English
The linear map from continuous maps to AEEqFun preserves scalar multiplication and addition, forming a linear map between these objects.
Русский
Линейное отображение от непрерывных отображений к AEEqFun сохраняет умножение на скаляры и сложение.
LaTeX
$$$\text{toAEEqFunLinearMap}$ is a linear map: $L(f+g) = L(f) + L(g)$ and $L(c f) = c L(f)$.$$
Lean4
theorem ae_nonneg_of_forall_setIntegral_nonneg {f : α → ℝ} (hf : AEFinStronglyMeasurable f μ)
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f :=
by
let t := hf.sigmaFiniteSet
suffices 0 ≤ᵐ[μ.restrict t] f from ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl.symm.le
haveI : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict
refine ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite (fun s hs hμts => ?_) fun s hs hμts => ?_
· rw [IntegrableOn, Measure.restrict_restrict hs]
rw [Measure.restrict_apply hs] at hμts
exact hf_int_finite (s ∩ t) (hs.inter hf.measurableSet) hμts
· rw [Measure.restrict_restrict hs]
rw [Measure.restrict_apply hs] at hμts
exact hf_zero (s ∩ t) (hs.inter hf.measurableSet) hμts
