From 5d32ec82454c28fcdf9642c6191e9e919b5722ff Mon Sep 17 00:00:00 2001
From: jvanwinden <6528059+jvanwinden@users.noreply.github.com>
Date: Sun, 24 May 2026 11:48:28 +0000
Subject: [PATCH] Automated addition of changes in
 Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean

---
 .../Lebesgue/DominatedConvergence.lean         | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean
index 1fc71d17528bcc..808e09449c5376 100644
--- a/Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean
+++ b/Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean
@@ -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]
@@ -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
@@ -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