Skip to content

[Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions #39768

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
mathlib-splicebot wants to merge 1 commit into from
Closed

[Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions #39768

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
18 changes: 14 additions & 4 deletions Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,10 +76,11 @@ theorem tendsto_lintegral_of_dominated_convergence' {F : ℕ → α → ℝ≥0
filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'
rwa [H'] at H

/-- **Dominated convergence theorem** for filters with a countable basis. -/
theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
/-- **Dominated convergence theorem** for filters with a countable basis and
AEMeasurable functions. -/
theorem tendsto_lintegral_filter_of_dominated_convergence' {ι} {l : Filter ι}
[l.IsCountablyGenerated] {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
(hF_meas : ∀ᶠ n in l, Measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
(hF_meas : ∀ᶠ n in l, AEMeasurable (F n) μ) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
(h_fin : ∫⁻ a, bound a ∂μ ≠ ∞) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
Tendsto (fun n => ∫⁻ a, F n a ∂μ) l (𝓝 <| ∫⁻ a, f a ∂μ) := by
rw [tendsto_iff_seq_tendsto]
Expand All @@ -91,7 +92,7 @@ theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
replace h := hxl _ h
rcases h with ⟨k, h⟩
rw [← tendsto_add_atTop_iff_nat k]
refine tendsto_lintegral_of_dominated_convergence ?_ ?_ ?_ ?_ ?_
refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_
· exact bound
· intro
refine (h _ ?_).1
Expand All @@ -106,6 +107,15 @@ theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
rw [tendsto_add_atTop_iff_nat]
assumption

/-- **Dominated convergence theorem** for filters with a countable basis. -/
theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
[l.IsCountablyGenerated] {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
(hF_meas : ∀ᶠ n in l, Measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
(h_fin : ∫⁻ a, bound a ∂μ ≠ ∞) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
Tendsto (fun n => ∫⁻ a, F n a ∂μ) l (𝓝 <| ∫⁻ a, f a ∂μ) := by
refine tendsto_lintegral_filter_of_dominated_convergence' bound ?_ h_bound h_fin h_lim
filter_upwards [hF_meas] using by fun_prop

/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. Auxiliary version assuming moreover that the
Expand Down
Loading