feat(MeasureTheory/Function): ae convergence implies convergence in distribution (leanprover-community#39517)

This PR introduces a theorem which concludes convergence in distribution from almost everywhere convergence. 

Previously, this could be done by chaining [`tendstoInMeasure_of_tendsto_ae`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/ConvergenceInMeasure.html#MeasureTheory.tendstoInMeasure_of_tendsto_ae) and [`TendstoInMeasure.tendstoInDistribution`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.html#MeasureTheory.TendstoInMeasure.tendstoInDistribution).
However, this is not a good way to to it since the second lemma requires a `SeminormedAddCommGroup E` instance (which is not needed for the statement to hold). Thus, we instead give a direct short proof which relies on dominated convergence.

As a consequence, we also obtain a new proof of `TendstoInMeasure.tendstoInDistribution` which does not pass through `tendstoInDistribution_of_tendstoInMeasure_sub` and therefore does not require `SeminormedAddCommGroup` and `SecondCountableTopology` anymore. I expect this will enable significant golfing (or maybe even removal) of `tendstoInDistribution_of_tendstoInMeasure_sub` in the future.

In order to allow for ae measurability as an assumption, it was necessary to add `tendsto_lintegral_filter_of_dominated_convergence'`, which gives dominated convergence along a countable filter for `AEMeasurable` functions.

Sidenote: I believe [`TendstoInMeasure.tendstoInDistribution`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.html#MeasureTheory.TendstoInMeasure.tendstoInDistribution) should be rewritten at some point to require only a metric space (or maybe only uniform space) structure. However, even if this was done, the theorem of this PR provides the value of relying only on `TopologicalSpace E`.

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author: 2 people

Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

@@ -129,8 +129,41 @@ theorem TendstoInDistribution.continuous_comp {F : Type*} [OpensMeasurableSpace
       congr
       rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable h.aemeasurable_limit]
 
+/-- Almost sure convergence implies convergence in distribution. -/
+theorem tendstoInDistribution_of_ae_tendsto [l.IsCountablyGenerated]
+    [OpensMeasurableSpace E] {X : ι → Ω' → E}
+    (hX₁ : ∀ i, AEMeasurable (X i) μ') (hZ : AEMeasurable Z μ')
+    (hX₂ : ∀ᵐ ω ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))) :
+    TendstoInDistribution X l Z (fun _ ↦ μ') μ' where
+  forall_aemeasurable := hX₁
+  aemeasurable_limit := hZ
+  tendsto := by
+    simp_rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, ProbabilityMeasure.coe_mk]
+    intro f
+    rw [lintegral_map' (by fun_prop) hZ]
+    conv in ∫⁻ _, _ ∂_ => rw [lintegral_map' (by fun_prop) (hX₁ i)]
+    apply tendsto_lintegral_filter_of_dominated_convergence' (bound := fun _ ↦ edist 0 f)
+    · exact .of_forall (by fun_prop)
+    · simp [f.apply_le_edist_zero]
+    · simp
+    filter_upwards [hX₂] with ω hω
+    simpa using f.continuous.tendsto (Z ω) |>.comp hω
+
 end TendstoInDistribution
 
+/-- Convergence in probability (`TendstoInMeasure`) implies convergence in distribution
+(`TendstoInDistribution`). -/
+theorem TendstoInMeasure.tendstoInDistribution [PseudoEMetricSpace E] [BorelSpace E]
+    [l.IsCountablyGenerated] [l.NeBot] {X : ι → Ω' → E}
+    (h : TendstoInMeasure μ' X l Z) (hX : ∀ i, AEMeasurable (X i) μ') :
+    TendstoInDistribution X l Z (fun _ ↦ μ') μ' := by
+  have hZ := h.aemeasurable hX
+  refine ⟨hX, hZ, ?_⟩
+  refine Filter.tendsto_of_subseq_tendsto (fun ns hns ↦ ?_)
+  obtain ⟨ms, hms1, hms2⟩ := h.comp hns |>.exists_seq_tendsto_ae'
+  refine ⟨ms, TendstoInDistribution.tendsto ?_⟩
+  exact tendstoInDistribution_of_ae_tendsto (by fun_prop) hZ hms2
+
 variable [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E]
 
 /-- Let `X, Y` be two sequences of measurable functions such that `X n` converges in distribution
@@ -257,13 +290,6 @@ lemma TendstoInMeasure.tendstoInDistribution_of_aemeasurable [l.IsCountablyGener
   tendstoInDistribution_of_tendstoInMeasure_sub X Z (tendstoInDistribution_const hZ)
     (by simpa [tendstoInMeasure_iff_norm] using h) hX
 
-/-- Convergence in probability (`TendstoInMeasure`) implies convergence in distribution
-(`TendstoInDistribution`). -/
-lemma TendstoInMeasure.tendstoInDistribution [l.NeBot] [l.IsCountablyGenerated]
-    {X : ι → Ω' → E} (h : TendstoInMeasure μ' X l Z) (hX : ∀ i, AEMeasurable (X i) μ') :
-    TendstoInDistribution X l Z (fun _ ↦ μ') μ' :=
-    h.tendstoInDistribution_of_aemeasurable hX (h.aemeasurable hX)
-
 /-- **Slutsky's theorem**: if `X n` converges in distribution to `Z`, and `Y n` converges in
 probability to a constant `c`, then the pair `(X n, Y n)` converges in distribution to `(Z, c)`. -/
 theorem TendstoInDistribution.prodMk_of_tendstoInMeasure_const

Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

@@ -27,12 +27,18 @@ namespace BoundedContinuousFunction
 
 section NNRealValued
 
-lemma apply_le_nndist_zero {X : Type*} [TopologicalSpace X] (f : X →ᵇ ℝ≥0) (x : X) :
+variable {X : Type*} [TopologicalSpace X]
+
+lemma apply_le_nndist_zero (f : X →ᵇ ℝ≥0) (x : X) :
     f x ≤ nndist 0 f := by
   convert! nndist_coe_le_nndist x
   simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]
 
-variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X]
+lemma apply_le_edist_zero (f : X →ᵇ ℝ≥0) (x : X) :
+    f x ≤ edist 0 f := by
+  simpa [← ENNReal.coe_le_coe] using f.apply_le_nndist_zero x
+
+variable [MeasurableSpace X]
 
 lemma lintegral_le_edist_mul (f : X →ᵇ ℝ≥0) (μ : Measure X) :
     (∫⁻ x, f x ∂μ) ≤ edist 0 f * (μ Set.univ) :=

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -314,7 +314,7 @@ theorem edist_lt_top {α : Type*} [PseudoMetricSpace α] (x y : α) : edist x y
   (edist_dist x y).symm ▸ ENNReal.ofReal_lt_top
 
 /-- In a pseudometric space, the extended distance is always finite -/
-@[aesop (rule_sets := [finiteness]) safe apply]
+@[aesop (rule_sets := [finiteness]) safe apply, simp]
 theorem edist_ne_top (x y : α) : edist x y ≠ ⊤ :=
   (edist_lt_top x y).ne