norm_setToL1S_le — Mathlib

English

There is a linear map setToL1SCLM' from L1-simple functions to F that extends T via a dominated finite-measure additive property.

Русский

Существует линейное отображение setToL1SCLM' от L1-подобразующих к F, расширяющее T при доминированном условии конечной меры.

LaTeX

$$$$setToL1SCLM'(T) : (α \to₁ₛ[μ] E) \to F, \; f \mapsto setToL1S T f.$$$$

Lean4

theorem norm_setToL1S_le (T : Set α → E →L[ℝ] F) {C : ℝ}
    (hT_norm : ∀ s, MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s) (f : α →₁ₛ[μ] E) : ‖setToL1S T f‖ ≤ C * ‖f‖ :=
  by
  rw [setToL1S, norm_eq_sum_mul f]
  exact SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm _ (SimpleFunc.integrable f)

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