English
If μ is finite and T satisfies the zero-condition, then for indicator of the whole space, setToL1S T equals T univ on inputs.
Русский
Если мера μ конечна и T удовлетворяет нулевому условию, то indicator_const на всю пространство даёт равенство.
LaTeX
$$$$setToL1S T(\\mathrm{indicatorConst}(1)_{\\mathrm{univ}}) = T(\\mathrm{univ}).$$$$
Lean4
theorem setToL1S_indicatorConst {T : Set α → E →L[ℝ] F} {s : Set α} (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
(h_add : FinMeasAdditive μ T) (hs : MeasurableSet s) (hμs : μ s < ∞) (x : E) :
setToL1S T (simpleFunc.indicatorConst 1 hs hμs.ne x) = T s x :=
by
have h_empty : T ∅ = 0 := h_zero _ MeasurableSet.empty measure_empty
rw [setToL1S_eq_setToSimpleFunc]
refine Eq.trans ?_ (SimpleFunc.setToSimpleFunc_indicator T h_empty hs x)
refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
exact toSimpleFunc_indicatorConst hs hμs.ne x
