setToL1SCLM' — Mathlib

English

If for all s measurable and μ s finite, T s x ≤ T' s x, then setToL1S T f ≤ setToL1S T' f.

Русский

Если для всех измеримых s и μ s конечна T s x ≤ T' s x, то setToL1S T f ≤ setToL1S T' f.

LaTeX

$$$$\forall s, MeasurableSet(s) \to \mu(s) < \infty \to \forall x, T(s)x \le T'(s)x \Rightarrow setToL1S(T, f) \le setToL1S(T', f).$$$$

Lean4

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

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