update

Author: CoolRmal

Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

@@ -362,7 +362,7 @@ end ExistsSeqTendstoAe
 is bounded by some constant `C`, then the `eLpNorm` of its limit is also bounded by `C`. -/
 lemma eLpNorm_le_of_tendstoInMeasure {ι : Type*} [SeminormedAddGroup E]
     {u : Filter ι} [NeBot u] [IsCountablyGenerated u] {f : ι → α → E} {g : α → E} {C : ℝ≥0∞}
-    (p : ℝ≥0∞) (bound : ∀ᶠ i in u, eLpNorm (f i) p μ ≤ C) (h_tendsto : TendstoInMeasure μ f u g)
+    {p : ℝ≥0∞} (bound : ∀ᶠ i in u, eLpNorm (f i) p μ ≤ C) (h_tendsto : TendstoInMeasure μ f u g)
     (hf : ∀ i, AEStronglyMeasurable (f i) μ) : eLpNorm g p μ ≤ C := by
   obtain ⟨l, hl⟩ := h_tendsto.exists_seq_tendsto_ae'
   exact Lp.eLpNorm_le_of_ae_tendsto (hl.1.eventually bound) (fun n => hf (l n)) hl.2

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -674,32 +674,33 @@ theorem unifIntegrable_of (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → β
 
 /-- If `fn` is `UnifIntegrable`, then the family of limits in probability of sequences of `fn` is
 `UnifIntegrable`. -/
-lemma UnifIntegrable.unifIntegrable_of_tendstoInMeasure {fn : ι → α → β} (p : ℝ≥0∞)
+lemma UnifIntegrable.unifIntegrable_of_tendstoInMeasure {fn : ι → α → β}
     (hUI : UnifIntegrable fn p μ) (hfn : ∀ i, AEStronglyMeasurable (fn i) μ) :
     UnifIntegrable (fun (f : {g : α → β | ∃ ni : ℕ → ι,
       TendstoInMeasure μ (fn ∘ ni) atTop g}) ↦ f.1) p μ := by
   refine fun ε hε => ?_
   obtain ⟨δ, hδ, hδ'⟩ := hUI hε
   refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩
-  refine eLpNorm_le_of_tendstoInMeasure p
+  refine eLpNorm_le_of_tendstoInMeasure
     (Eventually.of_forall fun n => hδ' (s n) t ht ht') (hs.indicator t) ?_
   exact fun n => (hfn (s n)).indicator ht
 
 /-- If `fn` is `UnifIntegrable`, then the family of a.e. limits of sequences of `fn` is
 `UnifIntegrable`. -/
-lemma UnifIntegrable.unifIntegrable_of_tendsto_ae {fn : ι → α → β} (p : ℝ≥0∞)
-    (hUI : UnifIntegrable fn p μ) (hfn : ∀ i, AEStronglyMeasurable (fn i) μ) :
+lemma UnifIntegrable.unifIntegrable_of_tendsto_ae {fn : ι → α → β} (hUI : UnifIntegrable fn p μ)
+    (hfn : ∀ i, AEStronglyMeasurable (fn i) μ) :
     UnifIntegrable (fun (f : {g : α → β | ∃ ni : ℕ → ι,
       ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) atTop (nhds (g x))}) ↦ f.1) p μ := by
   refine fun ε hε => ?_
   obtain ⟨δ, hδ, hδ'⟩ := hUI hε
   refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩
-  refine seq_tendsto_ae_bounded p (fun n => hδ' (s n) t ht ht') ?_ ?_
+  refine Lp.eLpNorm_le_of_ae_tendsto
+    (Eventually.of_forall (f := atTop) fun n => hδ' (s n) t ht ht') ?_ ?_
+  · exact fun n => (hfn (s n)).indicator ht
   · filter_upwards [hs] with a ha
     by_cases memt : a ∈ t
     · simpa [memt]
     · simp [memt]
-  · exact fun n => (hfn (s n)).indicator ht
 
 end UnifIntegrable
 
@@ -919,16 +920,27 @@ theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} (
 
 /-- If `fn` is `UniformIntegrable`, then the family of limits in probability of sequences of `fn` is
 `UniformIntegrable`. -/
-lemma UniformIntegrable.uniformIntegrable_of_tendstoInMeasure
-    {α β ι : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β]
-    {fn : ι → α → β} (p : ℝ≥0∞) (hUI : UniformIntegrable fn p μ) :
+lemma UniformIntegrable.uniformIntegrable_of_tendstoInMeasure {fn : ι → α → β}
+    (hUI : UniformIntegrable fn p μ) :
     UniformIntegrable (fun (f : {g : α → β | ∃ ni : ℕ → ι,
       TendstoInMeasure μ (fn ∘ ni) atTop g}) ↦ f.1) p μ := by
-  refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure p (fun i => hUI.1 i), ?_⟩
+  refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendstoInMeasure (fun i => hUI.1 i), ?_⟩
   · exact hs.aestronglyMeasurable (fun n => hUI.1 (s n))
   · obtain ⟨C, hC⟩ := hUI.2.2
-    refine ⟨C, fun ⟨f, s, hs⟩ => ?_⟩
-    exact tendstoInMeasure_bounded p (fun n => hC (s n)) hs (fun n => hUI.1 (s n))
+    exact ⟨C, fun ⟨f, s, hs⟩ => eLpNorm_le_of_tendstoInMeasure
+      (Eventually.of_forall fun n => hC (s n)) hs (fun n => hUI.1 (s n))⟩
+
+/-- If `fn` is `UniformIntegrable`, then the family of a.e. limits of sequences of `fn` is
+`UniformIntegrable`. -/
+lemma UniformIntegrable.uniformIntegrable_of_tendsto_ae {fn : ι → α → β}
+    (hUI : UniformIntegrable fn p μ) :
+    UniformIntegrable (fun (f : {g : α → β | ∃ ni : ℕ → ι,
+      ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) atTop (nhds (g x))}) ↦ f.1) p μ := by
+  refine ⟨fun ⟨f, s, hs⟩ => ?_, hUI.2.1.unifIntegrable_of_tendsto_ae (fun i => hUI.1 i), ?_⟩
+  · exact aestronglyMeasurable_of_tendsto_ae atTop (fun n => hUI.1 (s n)) hs
+  · obtain ⟨C, hC⟩ := hUI.2.2
+    exact ⟨C, fun ⟨f, s, hs⟩ => Lp.eLpNorm_le_of_ae_tendsto
+      (Eventually.of_forall fun n => hC (s n)) (fun n => hUI.1 (s n)) hs⟩
 
 end UniformIntegrable