feat: Lipschitz function criterion for weak convergence of probability measures (#30742)

Weak convergence of probability measures is equivalent to the property that the integrals of every bounded Lipschitz function converge to the integral of the function against the limit measure.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

@@ -104,7 +104,7 @@ theorem measure_of_cont_bdd_of_tendsto_indicator
 
 /-- The integrals of thickened indicators of a closed set against a finite measure tend to the
 measure of the closed set if the thickening radii tend to zero. -/
-theorem tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type*} [MeasurableSpace Ω]
+theorem tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type*} {mΩ : MeasurableSpace Ω}
     [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] {F : Set Ω}
     (F_closed : IsClosed F) {δs : ℕ → ℝ} (δs_pos : ∀ n, 0 < δs n)
     (δs_lim : Tendsto δs atTop (𝓝 0)) :
@@ -115,6 +115,36 @@ theorem tendsto_lintegral_thickenedIndicator_of_isClosed {Ω : Type*} [Measurabl
   have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F
   rwa [F_closed.closure_eq] at key
 
+/-- A thickened indicator is integrable. -/
+lemma integrable_thickenedIndicator {Ω : Type*} {mΩ : MeasurableSpace Ω}
+    [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] (F : Set Ω)
+    {δ : ℝ} (δ_pos : 0 < δ) :
+    Integrable (fun ω ↦ (thickenedIndicator δ_pos F ω : ℝ)) μ := by
+  refine .of_bound (by fun_prop) 1 (ae_of_all _ fun x ↦ ?_)
+  simpa using thickenedIndicator_le_one δ_pos F x
+
+/-- The integrals of thickened indicators of a closed set against a finite measure tend to the
+measure of the closed set if the thickening radii tend to zero. -/
+lemma tendsto_integral_thickenedIndicator_of_isClosed {Ω : Type*} {mΩ : MeasurableSpace Ω}
+    [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] {F : Set Ω}
+    (F_closed : IsClosed F) {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n)
+    (δs_lim : Tendsto δs atTop (𝓝 0)) :
+    Tendsto (fun n : ℕ ↦ ∫ ω, (thickenedIndicator (δs_pos n) F ω : ℝ) ∂μ) atTop (𝓝 (μ.real F)) := by
+  -- we switch to the `lintegral` formulation and apply the corresponding lemma there
+  let fs : ℕ → Ω → ℝ := fun n ω ↦ thickenedIndicator (δs_pos n) F ω
+  have h := tendsto_lintegral_thickenedIndicator_of_isClosed μ F_closed δs_pos δs_lim
+  have h_eq (n : ℕ) : ∫⁻ ω, thickenedIndicator (δs_pos n) F ω ∂μ
+      = ENNReal.ofReal (∫ ω, fs n ω ∂μ) := by
+    rw [lintegral_coe_eq_integral]
+    exact integrable_thickenedIndicator F (δs_pos _)
+  simp_rw [h_eq] at h
+  rw [Measure.real_def]
+  have h_eq' : (fun n ↦ ∫ ω, fs n ω ∂μ) = fun n ↦ (ENNReal.ofReal (∫ ω, fs n ω ∂μ)).toReal := by
+    ext n
+    rw [ENNReal.toReal_ofReal]
+    exact integral_nonneg fun x ↦ by simp [fs]
+  rwa [h_eq', ENNReal.tendsto_toReal_iff (by simp) (by finiteness)]
+
 end MeasureTheory -- namespace
 
 end auxiliary -- section

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -640,8 +640,80 @@ theorem tendsto_of_forall_isClosed_limsup_le
   exact (limsup_comp (fun i ↦ μs i F) u _).trans_le
     (limsup_le_limsup_of_le hu (by isBoundedDefault) ⟨1, by simp⟩)
 
+lemma tendsto_of_forall_isClosed_limsup_real_le' {L : Filter ι} [L.IsCountablyGenerated]
+    (h : ∀ F : Set Ω, IsClosed F →
+      limsup (fun i ↦ (μs i : Measure Ω).real F) L ≤ (μ : Measure Ω).real F) :
+    Tendsto μs L (𝓝 μ) := by
+  refine tendsto_of_forall_isClosed_limsup_le' fun F hF ↦ ?_
+  rcases L.eq_or_neBot with rfl | hne
+  · simp
+  specialize h F hF
+  simp only [Measure.real_def] at h
+  rwa [ENNReal.limsup_toReal_eq (b := 1) (by simp) (.of_forall fun i ↦ prob_le_one),
+    ENNReal.toReal_le_toReal _ (by finiteness)] at h
+  refine ne_top_of_le_ne_top (b := 1) (by simp) ?_
+  refine limsup_le_of_le ?_ (.of_forall fun i ↦ prob_le_one)
+  exact isCoboundedUnder_le_of_le L (x := 0) (by simp)
+
 end Closed
 
+section Lipschitz
+
+/-- Weak convergence of probability measures is equivalent to the property that the integrals of
+every bounded Lipschitz function converge to the integral of the function against
+the limit measure. -/
+theorem tendsto_iff_forall_lipschitz_integral_tendsto {γ Ω : Type*} {mΩ : MeasurableSpace Ω}
+    [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {F : Filter γ} [F.IsCountablyGenerated]
+    {μs : γ → ProbabilityMeasure Ω} {μ : ProbabilityMeasure Ω} :
+    Tendsto μs F (𝓝 μ) ↔
+      ∀ f : Ω → ℝ, (∃ (C : ℝ), ∀ x y, dist (f x) (f y) ≤ C) → (∃ L, LipschitzWith L f) →
+        Tendsto (fun i ↦ ∫ ω, f ω ∂(μs i)) F (𝓝 (∫ ω, f ω ∂μ)) := by
+  constructor
+  · -- A bounded Lipschitz function is in particular a bounded continuous function, and we already
+    -- know that weak convergence implies convergence of their integrals
+    intro h f hf_bounded hf_lip
+    simp_rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto] at h
+    let f' : BoundedContinuousFunction Ω ℝ :=
+    { toFun := f
+      continuous_toFun := hf_lip.choose_spec.continuous
+      map_bounded' := hf_bounded }
+    simpa using h f'
+  -- To prove the other direction, we prove convergence of the measure of closed sets.
+  -- We approximate the indicator function of a closed set by bounded Lipschitz functions.
+  rcases F.eq_or_neBot with rfl | hne
+  · simp
+  refine fun h ↦ tendsto_of_forall_isClosed_limsup_real_le' fun s hs ↦ ?_
+  refine le_of_forall_pos_le_add fun ε ε_pos ↦ ?_
+  let fs : ℕ → Ω → ℝ := fun n ω ↦ thickenedIndicator (δ := (1 : ℝ) / (n + 1)) (by positivity) s ω
+  have key₁ : Tendsto (fun n ↦ ∫ ω, fs n ω ∂μ) atTop (𝓝 ((μ : Measure Ω).real s)) :=
+    tendsto_integral_thickenedIndicator_of_isClosed μ hs (δs := fun n ↦ (1 : ℝ) / (n + 1))
+      (fun _ ↦ by positivity) tendsto_one_div_add_atTop_nhds_zero_nat
+  have room₁ : (μ : Measure Ω).real s < (μ : Measure Ω).real s + ε / 2 := by simp [ε_pos]
+  obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁
+  have key₂ : Tendsto (fun i ↦ ∫ ω, fs M ω ∂(μs i)) F (𝓝 (∫ ω, fs M ω ∂μ)) :=
+    h (fs M) ⟨1, fun x y ↦ ?_⟩
+      ⟨_, lipschitzWith_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s⟩
+  swap
+  · simp only [Real.dist_eq, abs_le]
+    have h1 x : fs M x ≤ 1 := thickenedIndicator_le_one _ _ _
+    have h2 x : 0 ≤ fs M x := by simp [fs]
+    grind
+  have room₂ : ∫ a, fs M a ∂μ < ∫ a, fs M a ∂μ + ε / 2 := by simp [ε_pos]
+  have ev_near : ∀ᶠ x in F, (μs x : Measure Ω).real s ≤ ∫ a, fs M a ∂μ + ε / 2 := by
+    refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx
+    rw [← integral_indicator_one hs.measurableSet]
+    refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
+    · exact (integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn
+    · have h : _ ≤ fs M :=
+        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
+      simpa using h
+  apply (Filter.limsup_le_of_le ?_ ev_near).trans
+  · apply (add_le_add (hM M rfl.le).le (le_refl (ε / 2))).trans_eq
+    ring
+  · exact isCoboundedUnder_le_of_le F (x := 0) (by simp)
+
+end Lipschitz
+
 section convergenceCriterion
 
 open scoped Finset