English
If two functions f, g have equal restricted integrals on all measurable sets, then they are equal almost everywhere on t, under the usual measurable assumptions.
Русский
Если интегралы f и g по ограничению на каждый измеримый набор совпадают, то они равны a.e. на t.
LaTeX
$$$f =_{a.e.\ μ|_t} g$ if $\int_s f = \int_s g$ for all measurable s ⊆ t.$$
Lean4
theorem ae_eq_restrict_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_zero : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) {t : Set α}
(ht : MeasurableSet t) (hμt : μ t ≠ ∞) : f =ᵐ[μ.restrict t] 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)]
exact sub_eq_zero.mpr (hfg_zero 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 ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hfg_int hfg' ht hμt
