English
If two σ-finite vector-valued functions have equal integrals over all measurable sets, they are equal almost everywhere.
Русский
Если две векторнозначные функции σ-сконечны по мере, имеют одинаковые интегралы на всех измеримых множествах, то они равны почти повсюду.
LaTeX
$$$f = g\ a.e.\ μ$ given $\int_s f = \int_s g$ for all measurable s.$$
Lean4
theorem ae_eq_of_forall_setIntegral_eq {f g : α → E}
(hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
(hg_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn g s μ)
(hfg_eq : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
(hf : AEFinStronglyMeasurable f μ) (hg : AEFinStronglyMeasurable g μ) : f =ᵐ[μ] g :=
by
rw [← sub_ae_eq_zero]
have hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 :=
by
intro s hs hμs
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs), sub_eq_zero.mpr (hfg_eq s hs hμs)]
have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
(hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
exact (hf.sub hg).ae_eq_zero_of_forall_setIntegral_eq_zero hfg_int hfg
