setToL1S_const — Mathlib

English

For measurable s with finite measure, the indicator-constant simple function yields the correct T(s) application.

Русский

Для измеримого s с конечной мерой индикаторная константа дает корректное применение T(s).

LaTeX

$$$$setToL1S T(\mathrm{indicatorConst}(1)_{s} \; x) = T(s) x.$$$$

Lean4

theorem setToL1S_const [IsFiniteMeasure μ] {T : Set α → E →L[ℝ] F} (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (x : E) :
    setToL1S T (simpleFunc.indicatorConst 1 MeasurableSet.univ (measure_ne_top μ _) x) = T univ x :=
  setToL1S_indicatorConst h_zero h_add MeasurableSet.univ (measure_lt_top _ _) x

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