Skip to content

[Merged by Bors] - refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/AEEqOfIntegral #38350

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
yuanyi-350 wants to merge 1 commit into from
+6 −17
Closed

[Merged by Bors] - refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/AEEqOfIntegral #38350

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 6 additions & 17 deletions Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,27 +357,16 @@ theorem ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim (hm :
exact hf_zero _ (hs.inter ht_meas) hμs

theorem Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E} (hf : Integrable f μ)
(hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 := by
have hf_Lp : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
let f_Lp := hf_Lp.toLp f
have hf_f_Lp : f =ᵐ[μ] f_Lp := (MemLp.coeFn_toLp hf_Lp).symm
refine hf_f_Lp.trans ?_
refine Lp.ae_eq_zero_of_forall_setIntegral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top ?_ ?_
· exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _)
· intro s hs hμs
rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)]
exact hf_zero s hs hμs
(hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
hf.aefinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero
(fun _ _ _ => hf.integrableOn) hf_zero

theorem Integrable.ae_eq_of_forall_setIntegral_eq (f g : α → E) (hf : Integrable f μ)
(hg : Integrable g μ)
(hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) :
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.integrableOn hg.integrableOn]
exact sub_eq_zero.mpr (hfg s hs hμs)
exact Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero (hf.sub hg) hfg'
f =ᵐ[μ] g :=
AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq (fun _ _ _ => hf.integrableOn)
(fun _ _ _ => hg.integrableOn) hfg hf.aefinStronglyMeasurable hg.aefinStronglyMeasurable

variable {β : Type*} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]

Expand Down
Loading