English
If hT is a dominated additive property with scalar smul compatibility, then (c • T) yields the same scaled map on f.
Русский
Если есть совместимость умножения скаляра и доминированного аддитивного свойства, то (c • T) действует как масштабирование на f.
LaTeX
$$$$setToL1S (\lambda s. c \cdot T(s)) (f) = c \cdot setToL1S T f.$$$$
Lean4
theorem setToL1S_nonneg (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T)
(hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f : α →₁ₛ[μ] G''} (hf : 0 ≤ f) :
0 ≤ setToL1S T f := by
simp_rw [setToL1S]
obtain ⟨f', hf', hff'⟩ := exists_simpleFunc_nonneg_ae_eq hf
replace hff' : simpleFunc.toSimpleFunc f =ᵐ[μ] f' := (Lp.simpleFunc.toSimpleFunc_eq_toFun f).trans hff'
rw [SimpleFunc.setToSimpleFunc_congr _ h_zero h_add (SimpleFunc.integrable _) hff']
exact SimpleFunc.setToSimpleFunc_nonneg' T hT_nonneg _ hf' ((SimpleFunc.integrable f).congr hff')
