English
If μ is sigma-finite and f is integrable on all sets, and integrals over all measurable sets agree with zero, then f = 0 almost everywhere.
Русский
При сигма-конечности μ и интегрируемости на всех множествах, если интегралы совпадают с нулём на всех измеримых множествах, то f = 0 a.e.
LaTeX
$$$f = 0\ a.e.\ μ$ under sigma-finite hypotheses and integrable conditions.$$
Lean4
theorem ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite [SigmaFinite μ] {f : α → E}
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hf_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
by
let S := spanningSets μ
rw [← @Measure.restrict_univ _ _ μ, ← iUnion_spanningSets μ, EventuallyEq, ae_iff,
Measure.restrict_apply' (MeasurableSet.iUnion (measurableSet_spanningSets μ))]
rw [Set.inter_iUnion, measure_iUnion_null_iff]
intro n
have h_meas_n : MeasurableSet (S n) := measurableSet_spanningSets μ n
have hμn : μ (S n) < ∞ := measure_spanningSets_lt_top μ n
rw [← Measure.restrict_apply' h_meas_n]
exact ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hf_int_finite hf_zero h_meas_n hμn.ne
