setToL1SCLM — Mathlib

English

Under the hypothesis hT_norm, for f ∈ α →₁ₛ[μ] E, the norm of setToL1S T f is bounded by C times the norm of f.

Русский

При гипотезе hT_norm нормa setToL1S T f не превышает C умножить на норму f.

LaTeX

$$$$ \|setToL1S T f\| \le C \|f\|. $$$$

Lean4

/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[ℝ] F`. -/
def setToL1SCLM {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : (α →₁ₛ[μ] E) →L[ℝ] F :=
  LinearMap.mkContinuous
    ⟨⟨setToL1S T, setToL1S_add T (fun _ => hT.eq_zero_of_measure_zero) hT.1⟩,
      setToL1S_smul_real T (fun _ => hT.eq_zero_of_measure_zero) hT.1⟩
    C fun f => norm_setToL1S_le T hT.2 f

Похожие утверждения