feat: add last implication of portmanteau characterizations of weak c…

…onvergence (#8097)

This PR adds the last missing implication of the general case of portmanteau equivalent characterizations of convergence in distribution: a sufficient condition for convergence in distribution of a sequence of probability measures is that for all open sets the candidate limit measure is at most the liminf of the measures.



Co-authored-by: Kalle <kalle.kytola@aalto.fi>
Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

Mathlib.lean

@@ -3545,6 +3545,7 @@ import Mathlib.Topology.NoetherianSpace
 import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.Order.Bounded
 import Mathlib.Topology.Order.Category.AlexDisc
 import Mathlib.Topology.Order.Category.FrameAdjunction
 import Mathlib.Topology.Order.Hom.Basic

Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

@@ -22,8 +22,17 @@ namespace BoundedContinuousFunction
 
 section NNRealValued
 
+lemma apply_le_nndist_zero {X : Type*} [TopologicalSpace X] (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] [OpensMeasurableSpace X]
 
+lemma lintegral_le_edist_mul (f : X →ᵇ ℝ≥0) (μ : Measure X) :
+    (∫⁻ x, f x ∂μ) ≤ edist 0 f * (μ Set.univ) :=
+  le_trans (lintegral_mono (fun x ↦ ENNReal.coe_le_coe.mpr (f.apply_le_nndist_zero x))) (by simp)
+
 theorem measurable_coe_ennreal_comp (f : X →ᵇ ℝ≥0) :
     Measurable fun x ↦ (f x : ℝ≥0∞) :=
   measurable_coe_nnreal_ennreal.comp f.continuous.measurable

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -5,6 +5,9 @@ Authors: Kalle Kytölä
 -/
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
+import Mathlib.MeasureTheory.Integral.Layercake
+import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
+import Mathlib.Topology.Order.Bounded
 
 #align_import measure_theory.measure.portmanteau from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -39,9 +42,8 @@ The separate implications are:
  * `MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge` is the equivalence (C) ↔ (O).
  * `MeasureTheory.tendsto_measure_of_null_frontier` is the implication (O) → (B).
  * `MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure` is the implication (B) → (C).
-
-TODO:
- * Prove the remaining implication (O) → (T) to complete the proof of equivalence of the conditions.
+ * `MeasureTheory.tendsto_of_forall_isOpen_le_liminf` gives the implication (O) → (T) for
+    any sequence of Borel probability measures.
 
 ## Implementation notes
 
@@ -77,14 +79,7 @@ probability measure
 
 noncomputable section
 
-open MeasureTheory
-
-open Set
-
-open Filter
-
-open BoundedContinuousFunction
-
+open MeasureTheory Set Filter BoundedContinuousFunction
 open scoped Topology ENNReal NNReal BoundedContinuousFunction
 
 namespace MeasureTheory
@@ -539,4 +534,128 @@ lemma le_liminf_measure_open_of_forall_tendsto_measure
 
 end LimitBorelImpliesLimsupClosedLE --section
 
+section le_liminf_open_implies_convergence
+
+/-! ### Portmanteau implication: liminf condition for open sets implies weak convergence
+
+
+In this section we prove for a sequence (μsₙ)ₙ Borel probability measures that
+
+  (O) For any open set G, the liminf of the measures of G under μsₙ is at least
+      the measure of G under μ, i.e., μ(G) ≤ liminfₙ μsₙ(G).
+
+implies
+
+  (T) The measures μsₙ converge weakly to the measure μ.
+
+-/
+
+variable {Ω : Type} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω]
+
+lemma lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
+    {μ : Measure Ω} {μs : ℕ → Measure Ω} {f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f)
+    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
+    ∫⁻ x, ENNReal.ofReal (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫⁻ x, ENNReal.ofReal (f x) ∂ (μs i)) := by
+  simp_rw [lintegral_eq_lintegral_meas_lt _ (eventually_of_forall f_nn) f_cont.aemeasurable]
+  calc  ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
+      ≤ ∫⁻ (t : ℝ) in Set.Ioi 0, atTop.liminf (fun i ↦ (μs i) {a | t < f a}) := ?_ -- (i)
+    _ ≤ atTop.liminf (fun i ↦ ∫⁻ (t : ℝ) in Set.Ioi 0, (μs i) {a | t < f a}) := ?_ -- (ii)
+  · -- (i)
+    exact (lintegral_mono (fun t ↦ h_opens _ (continuous_def.mp f_cont _ isOpen_Ioi))).trans
+            (le_refl _)
+  · -- (ii)
+    exact lintegral_liminf_le (fun n ↦ Antitone.measurable (fun s t hst ↦
+            measure_mono (fun ω hω ↦ lt_of_le_of_lt hst hω)))
+
+lemma integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure
+    {μ : Measure Ω} [IsProbabilityMeasure μ] {μs : ℕ → Measure Ω} [∀ i, IsProbabilityMeasure (μs i)]
+    {f : Ω →ᵇ ℝ} (f_nn : 0 ≤ f)
+    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
+    ∫ x, (f x) ∂μ ≤ atTop.liminf (fun i ↦ ∫ x, (f x) ∂ (μs i)) := by
+  have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
+                  f.continuous f_nn h_opens
+  rw [@integral_eq_lintegral_of_nonneg_ae Ω _ μ f (eventually_of_forall f_nn)
+        f.continuous.measurable.aestronglyMeasurable]
+  convert (ENNReal.toReal_le_toReal ?_ ?_).mpr same
+  · simp only [fun i ↦ @integral_eq_lintegral_of_nonneg_ae Ω _ (μs i) f (eventually_of_forall f_nn)
+                        f.continuous.measurable.aestronglyMeasurable]
+    let g := BoundedContinuousFunction.comp _ Real.lipschitzWith_toNNReal f
+    have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
+      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using
+            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g
+    apply ENNReal.liminf_toReal_eq ENNReal.coe_ne_top (eventually_of_forall bound)
+  · exact (f.lintegral_of_real_lt_top μ).ne
+  · apply ne_of_lt
+    have obs := fun (i : ℕ) ↦ @BoundedContinuousFunction.lintegral_nnnorm_le Ω _ _ (μs i) ℝ _ f
+    simp only [measure_univ, mul_one] at obs
+    apply lt_of_le_of_lt _ (show (‖f‖₊ : ℝ≥0∞) < ∞ from ENNReal.coe_lt_top)
+    apply liminf_le_of_le
+    · refine ⟨0, eventually_of_forall (by simp only [ge_iff_le, zero_le, forall_const])⟩
+    · intro x hx
+      obtain ⟨i, hi⟩ := hx.exists
+      apply le_trans hi
+      convert obs i with x
+      have aux := ENNReal.ofReal_eq_coe_nnreal (f_nn x)
+      simp only [ContinuousMap.toFun_eq_coe, BoundedContinuousFunction.coe_to_continuous_fun] at aux
+      rw [aux]
+      congr
+      exact (Real.norm_of_nonneg (f_nn x)).symm
+
+lemma tendsto_integral_of_forall_integral_le_liminf_integral {ι : Type*} {L : Filter ι}
+    {μ : Measure Ω} [IsProbabilityMeasure μ] {μs : ι → Measure Ω} [∀ i, IsProbabilityMeasure (μs i)]
+    (h : ∀ f : Ω →ᵇ ℝ, 0 ≤ f → ∫ x, (f x) ∂μ ≤ L.liminf (fun i ↦ ∫ x, (f x) ∂ (μs i)))
+    (f : Ω →ᵇ ℝ) :
+    Tendsto (fun i ↦ ∫ x, (f x) ∂ (μs i)) L (𝓝 (∫ x, (f x) ∂μ)) := by
+  rcases eq_or_neBot L with rfl|hL
+  · simp only [tendsto_bot]
+  have obs := BoundedContinuousFunction.isBounded_range_integral μs f
+  have bdd_above : IsBoundedUnder (· ≤ ·) L (fun i ↦ ∫ (x : Ω), f x ∂μs i) :=
+    isBounded_le_map_of_bounded_range _ obs
+  have bdd_below : IsBoundedUnder (· ≥ ·) L (fun i ↦ ∫ (x : Ω), f x ∂μs i) :=
+    isBounded_ge_map_of_bounded_range _ obs
+  apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, (f x) ∂ (μs i)) (∫ x, (f x) ∂μ)
+  · have key := h _ (f.add_norm_nonneg)
+    simp_rw [f.integral_add_const ‖f‖] at key
+    simp only [measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul] at key
+    have := liminf_add_const L (fun i ↦ ∫ x, (f x) ∂ (μs i)) ‖f‖ bdd_above bdd_below
+    rwa [this, add_le_add_iff_right] at key
+  · have key := h _ (f.norm_sub_nonneg)
+    simp_rw [f.integral_const_sub ‖f‖] at key
+    simp only [measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul] at key
+    have := liminf_const_sub L (fun i ↦ ∫ x, (f x) ∂ (μs i)) ‖f‖ bdd_above bdd_below
+    rwa [this, sub_le_sub_iff_left] at key
+  · exact bdd_above
+  · exact bdd_below
+
+/-- One implication of the portmanteau theorem:
+If for all open sets G we have the liminf condition `μ(G) ≤ liminf μsₙ(G)`, then the measures
+μsₙ converge weakly to the measure μ. -/
+theorem tendsto_of_forall_isOpen_le_liminf {μ : ProbabilityMeasure Ω}
+    {μs : ℕ → ProbabilityMeasure Ω}
+    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
+    atTop.Tendsto (fun i ↦ μs i) (𝓝 μ) := by
+  refine ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr ?_
+  apply tendsto_integral_of_forall_integral_le_liminf_integral
+  intro f f_nn
+  apply integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure (f := f) f_nn
+  intro G G_open
+  specialize h_opens G G_open
+  simp only at h_opens
+  have aux : ENNReal.ofNNReal (liminf (fun i ↦ ENNReal.toNNReal ((μs i : Measure Ω) G)) atTop) =
+          liminf (ENNReal.ofNNReal ∘ fun i ↦ (ENNReal.toNNReal ((μs i : Measure Ω) G))) atTop := by
+    refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
+    · apply ENNReal.continuous_coe.continuousAt
+    · use 1
+      simp only [eventually_map, ProbabilityMeasure.apply_le_one, eventually_atTop, ge_iff_le,
+        implies_true, forall_const, exists_const]
+    · use 0
+      simp only [zero_le, eventually_map, eventually_atTop, ge_iff_le, implies_true, forall_const,
+        exists_const]
+  have obs := ENNReal.coe_mono h_opens
+  simp only [ne_eq, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs
+  convert obs
+  simp only [Function.comp_apply, ne_eq, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
+
+end le_liminf_open_implies_convergence
+
 end MeasureTheory --namespace

Mathlib/Topology/Instances/ENNReal.lean

@@ -136,6 +136,9 @@ theorem tendsto_toReal {a : ℝ≥0∞} (ha : a ≠ ⊤) : Tendsto ENNReal.toRea
   NNReal.tendsto_coe.2 <| tendsto_toNNReal ha
 #align ennreal.tendsto_to_real ENNReal.tendsto_toReal
 
+lemma continuousOn_toReal : ContinuousOn ENNReal.toReal { a | a ≠ ∞ } :=
+  NNReal.continuous_coe.comp_continuousOn continuousOn_toNNReal
+
 /-- The set of finite `ℝ≥0∞` numbers is homeomorphic to `ℝ≥0`. -/
 def neTopHomeomorphNNReal : { a | a ≠ ∞ } ≃ₜ ℝ≥0 where
   toEquiv := neTopEquivNNReal
@@ -1603,9 +1606,47 @@ theorem edist_le_tsum_of_edist_le_of_tendsto₀ {f : ℕ → α} (d : ℕ → 
 
 end
 
+namespace ENNReal
+
+section truncateToReal
+
+/-- With truncation level `t`, the truncated cast `ℝ≥0∞ → ℝ` is given by `x ↦ (min t x).toReal`.
+Unlike `ENNReal.toReal`, this cast is continuous and monotone when `t ≠ ∞`. -/
+noncomputable def truncateToReal (t x : ℝ≥0∞) : ℝ := (min t x).toReal
+
+lemma truncateToReal_eq_toReal {t x : ℝ≥0∞} (t_ne_top : t ≠ ∞) (x_le : x ≤ t) :
+    truncateToReal t x = x.toReal := by
+  have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top
+  have obs : min t x ≠ ∞ := by
+    simp_all only [ne_eq, ge_iff_le, min_eq_top, false_and, not_false_eq_true]
+  exact (ENNReal.toReal_eq_toReal obs x_lt_top.ne).mpr (min_eq_right x_le)
+
+lemma truncateToReal_le {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) {x : ℝ≥0∞} :
+    truncateToReal t x ≤ t.toReal := by
+  rw [truncateToReal]
+  apply (toReal_le_toReal _ t_ne_top).mpr (min_le_left t x)
+  simp_all only [ne_eq, ge_iff_le, min_eq_top, false_and, not_false_eq_true]
+
+lemma truncateToReal_nonneg {t x : ℝ≥0∞} : 0 ≤ truncateToReal t x := toReal_nonneg
+
+/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is monotone when `t ≠ ∞`. -/
+lemma monotone_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Monotone (truncateToReal t) := by
+  intro x y x_le_y
+  have obs_x : min t x ≠ ∞ := by
+    simp_all only [ne_eq, ge_iff_le, min_eq_top, false_and, not_false_eq_true]
+  have obs_y : min t y ≠ ∞ := by
+    simp_all only [ne_eq, ge_iff_le, min_eq_top, false_and, not_false_eq_true]
+  exact (ENNReal.toReal_le_toReal obs_x obs_y).mpr (min_le_min_left t x_le_y)
+
+/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is continuous when `t ≠ ∞`. -/
+lemma continuous_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Continuous (truncateToReal t) := by
+  apply continuousOn_toReal.comp_continuous (continuous_min.comp (Continuous.Prod.mk t))
+  simp [t_ne_top]
+
+end truncateToReal
+
 section LimsupLiminf
 
-namespace ENNReal
 set_option autoImplicit true
 
 lemma limsup_sub_const (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
@@ -1630,6 +1671,43 @@ lemma liminf_const_sub (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞)
   (Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
     (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm
 
-end ENNReal -- namespace
+/-- If `xs : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ xs) = toReal (liminf xs)`. -/
+lemma liminf_toReal_eq {ι : Type*} {F : Filter ι} [NeBot F] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞)
+    {xs : ι → ℝ≥0∞} (le_b : ∀ᶠ i in F, xs i ≤ b) :
+    F.liminf (fun i ↦ (xs i).toReal) = (F.liminf xs).toReal := by
+  have liminf_le : F.liminf xs ≤ b := by
+    apply liminf_le_of_le ⟨0, by simp⟩
+    intro y h
+    obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
+    exact hi.1.trans hi.2
+  have aux : ∀ᶠ i in F, (xs i).toReal = ENNReal.truncateToReal b (xs i) := by
+    filter_upwards [le_b] with i i_le_b
+    simp only [truncateToReal_eq_toReal b_ne_top i_le_b, implies_true]
+  have aux' : (F.liminf xs).toReal = ENNReal.truncateToReal b (F.liminf xs) := by
+    rw [truncateToReal_eq_toReal b_ne_top liminf_le]
+  simp_rw [liminf_congr aux, aux']
+  have key := Monotone.map_liminf_of_continuousAt (F := F) (monotone_truncateToReal b_ne_top) xs
+          (continuous_truncateToReal b_ne_top).continuousAt
+          ⟨b, by simpa only [eventually_map] using le_b⟩ ⟨0, eventually_of_forall (by simp)⟩
+  rw [key]
+  rfl
+
+/-- If `xs : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ xs) = toReal (liminf xs)`. -/
+lemma limsup_toReal_eq {ι : Type*} {F : Filter ι} [NeBot F] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞)
+    {xs : ι → ℝ≥0∞} (le_b : ∀ᶠ i in F, xs i ≤ b) :
+    F.limsup (fun i ↦ (xs i).toReal) = (F.limsup xs).toReal := by
+  have aux : ∀ᶠ i in F, (xs i).toReal = ENNReal.truncateToReal b (xs i) := by
+    filter_upwards [le_b] with i i_le_b
+    simp only [truncateToReal_eq_toReal b_ne_top i_le_b, implies_true]
+  have aux' : (F.limsup xs).toReal = ENNReal.truncateToReal b (F.limsup xs) := by
+    rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]
+  simp_rw [limsup_congr aux, aux']
+  have key := Monotone.map_limsup_of_continuousAt (F := F) (monotone_truncateToReal b_ne_top) xs
+          (continuous_truncateToReal b_ne_top).continuousAt
+          ⟨b, by simpa only [eventually_map] using le_b⟩ ⟨0, eventually_of_forall (by simp)⟩
+  rw [key]
+  rfl
 
 end LimsupLiminf
+
+end ENNReal -- namespace

Mathlib/Topology/MetricSpace/Lipschitz.lean

@@ -190,6 +190,11 @@ theorem _root_.lipschitzWith_min : LipschitzWith 1 fun p : ℝ × ℝ => min p.1
     (le_abs_self _).trans (abs_min_sub_min_le_max _ _ _ _)
 #align lipschitz_with_min lipschitzWith_min
 
+lemma _root_.Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal := by
+  refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)
+  simpa only [ge_iff_le, NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using
+    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)
+
 end Metric
 
 section EMetric

Mathlib/Topology/Order/Bounded.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä
+-/
+import Mathlib.Topology.Bornology.Basic
+import Mathlib.Topology.Instances.Real
+import Mathlib.Order.LiminfLimsup
+
+/-!
+# Relating order and metric boundedness
+
+In spaces equipped with both an order and a metric, there are separate notions of boundedness
+associated with each of the two structures. In specific cases such as ℝ, there are results which
+relate the two notions.
+
+## Tags
+
+bounded, bornology, order, metric
+-/
+
+open Set Filter
+
+section Real
+
+lemma Filter.isBounded_le_map_of_bounded_range {ι : Type*} (F : Filter ι) {f : ι → ℝ}
+    (h : Bornology.IsBounded (Set.range f)) :
+    (F.map f).IsBounded (· ≤ ·) := by
+  rw [Real.isBounded_iff_bddBelow_bddAbove] at h
+  obtain ⟨c, hc⟩ := h.2
+  refine isBoundedUnder_of ⟨c, by simpa [mem_upperBounds] using hc⟩
+
+lemma Filter.isBounded_ge_map_of_bounded_range {ι : Type*} (F : Filter ι) {f : ι → ℝ}
+    (h : Bornology.IsBounded (Set.range f)) :
+    (F.map f).IsBounded (· ≥ ·) := by
+  rw [Real.isBounded_iff_bddBelow_bddAbove] at h
+  obtain ⟨c, hc⟩ := h.1
+  apply isBoundedUnder_of ⟨c, by simpa [mem_lowerBounds] using hc⟩
+
+end Real