English
A comprehensive AE-equivalence on restriction: if the restriction to s of m equals the restriction to s of m2 in the sense described, then μ[f|m] = a.e. μ[f|m2] on s.
Русский
Обобщённое эквивалентность по мере на ограничении: если ограничения по s совпадают, то μ[f|m] = a.e. μ[f|m2] на s.
LaTeX
$$$$ μ[f|m] =_{a.e. μ|s} μ[f|m_2] $$$$
Lean4
theorem ae_eq_zero_of_forall_setIntegral_eq_zero (hm : m ≤ m0) (f : lpMeas E' 𝕜 m p μ) (hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ∞) (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (f : Lp E' p μ) s μ)
(hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, (f : Lp E' p μ) x ∂μ = 0) : f =ᵐ[μ] (0 : α → E') :=
by
obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top
refine hfg.trans ?_
refine ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim hm ?_ ?_ hg_sm
· intro s hs hμs
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
rw [IntegrableOn, integrable_congr hfg_restrict.symm]
exact hf_int_finite s hs hμs
· intro s hs hμs
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
rw [integral_congr_ae hfg_restrict.symm]
exact hf_zero s hs hμs
