English
If a function is FinStronglyMeasurable with respect to a trimmed measure μ.trim(hm), and it has zero finite-set integrals on measurable sets, then it is zero almost everywhere with respect to μ.
Русский
Если функция является FinStronglyMeasurable относительно усеченного мерами μ.trim(hm) измеримого пространства и интегралы по конечным измеримым множествам равны нулю, то она равна нулю почти повсеместно по μ.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} 0 $$$$
Lean4
theorem ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim (hm : m ≤ m0) {f : α → E}
(hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = 0)
(hf : FinStronglyMeasurable f (μ.trim hm)) : f =ᵐ[μ] 0 :=
by
obtain ⟨t, ht_meas, htf_zero, htμ⟩ := hf.exists_set_sigmaFinite
haveI : SigmaFinite ((μ.restrict t).trim hm) := by rwa [restrict_trim hm μ ht_meas] at htμ
have htf_zero : f =ᵐ[μ.restrict tᶜ] 0 :=
by
rw [EventuallyEq, ae_restrict_iff' (MeasurableSet.compl (hm _ ht_meas))]
exact Eventually.of_forall htf_zero
have hf_meas_m : StronglyMeasurable[m] f := hf.stronglyMeasurable
suffices f =ᵐ[μ.restrict t] 0 from ae_of_ae_restrict_of_ae_restrict_compl _ this htf_zero
refine measure_eq_zero_of_trim_eq_zero hm ?_
refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_
· intro s hs hμs
unfold IntegrableOn
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs, trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
refine Integrable.trim hm ?_ hf_meas_m
exact hf_int_finite _ (hs.inter ht_meas) hμs
· intro s hs hμs
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs, trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
rw [← integral_trim hm hf_meas_m]
exact hf_zero _ (hs.inter ht_meas) hμs
