feat(MeasureTheory/Measure/Tight): portmanteau condition for compact sets (leanprover-community#39543)

One part of the portmanteau theorem states that a limsup condition for closed sets implies weak convergence of probability measures. In the situation where the measures are tight however, one only needs to check the limsup condition for compact sets. 

This PR thus introduces `tendsto_of_forall_isCompact_of_isTightMeasureSet`, which is a version of [tendsto_of_forall_isClosed_limsup_le](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Portmanteau.html#MeasureTheory.tendsto_of_forall_isClosed_limsup_le) but replaces `IsClosed` with `IsCompact`, under the additional hypothesis that the measures are tight.

I would have liked to put this lemma in MeasureTheory/Portmeanteau, but this created an import cycle. I am open to suggestions for where it could otherwise be moved.

Author: jvanwinden

Mathlib/MeasureTheory/Measure/LevyConvergence.lean

@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
+public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 public import Mathlib.MeasureTheory.Measure.Tight
 
 import Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -6,9 +6,9 @@ Authors: Kalle Kytölä
 module
 
 public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
-public import Mathlib.MeasureTheory.Integral.Layercake
-public import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
+public import Mathlib.MeasureTheory.Measure.Tight
+
+import Mathlib.MeasureTheory.Integral.Layercake
 
 /-!
 # Characterizations of weak convergence of finite measures and probability measures
@@ -52,6 +52,9 @@ converges to a limiting probability measure. Assume also that the π-system cont
 small neighborhoods of any point. Then the sequence of probability measures converges for the
 weak topology.
 
+In case the set of measures is tight, (C) implies (T) even when 'closed' is replaced by 'compact'.
+This is shown in `MeasureTheory.tendsto_of_forall_isCompact_of_isTightMeasureSet`.
+
 ## Implementation notes
 
 Many of the characterizations of weak convergence hold for finite measures and are proven in that
@@ -647,6 +650,34 @@ lemma tendsto_of_forall_isClosed_limsup_real_le' {L : Filter ι} [L.IsCountablyG
       limsup (fun i ↦ (μs i : Measure Ω).real F) L ≤ (μ : Measure Ω).real F) :
     Tendsto μs L (𝓝 μ) := tendsto_of_forall_isClosed_limsup_le (by simpa using h)
 
+/-- A different version of the (C) → (T) implication of the portmanteau theorem:
+If the set of measures is tight, a `limsup` inequality for compact sets implies weak convergence. -/
+theorem tendsto_of_forall_isCompact_of_isTightMeasureSet
+    (h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs)))
+    (h₂ : ∀ F, IsCompact F → limsup (μs · F) L ≤ μ F) :
+    Tendsto μs L (𝓝 μ) := by
+  obtain rfl | _ := L.eq_or_neBot
+  · simp
+  refine tendsto_of_forall_isClosed_limsup_le <| fun F hF_closed ↦ ?_
+  rw [← ENNReal.coe_le_coe, ENNReal.ofNNReal_limsup <|
+      isBoundedUnder_of_eventually_le (a := 1) (by simp)]
+  refine ENNReal.le_of_forall_pos_le_add <| fun ε hε _ ↦ ?_
+  obtain ⟨K, hKc, hK_le⟩ := isTightMeasureSet_iff_exists_isCompact_measure_compl_le.mp
+    h₁ ε (by positivity)
+  grw [limsup_le_limsup (v := fun i ↦ μs i (F ∩ K) + (ε : ENNReal))]
+  · rw [limsup_add_const _ _ _ (by isBoundedDefault) (by isBoundedDefault)]
+    apply add_le_add _ (by simp)
+    specialize h₂ (F ∩ K) <| hKc.inter_left hF_closed
+    rw [← ENNReal.coe_le_coe, ENNReal.ofNNReal_limsup <|
+      isBoundedUnder_of_eventually_le (a := 1) (by simp)] at h₂
+    grw [h₂]
+    simp [measure_mono]
+  · refine .of_forall (fun i ↦ ?_)
+    simp_rw [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
+    grw [measure_mono (t := (F ∩ K) ∪ F \ K) (by simp), measure_union_le]
+    gcongr
+    exact le_trans (measure_mono (by simp)) <| hK_le (μs i) <| by simp
+
 end Closed
 
 section Lipschitz

Mathlib/MeasureTheory/Measure/Prokhorov.lean

@@ -7,9 +7,10 @@ module
 
 public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 public import Mathlib.MeasureTheory.Measure.Tight
+
 import Mathlib.MeasureTheory.Integral.Regular
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
-import Mathlib.Topology.Separation.CompletelyRegular
+import Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
 
 /-!
 # Prokhorov theorem
@@ -26,6 +27,8 @@ notably several versions of Prokhorov theorem on tight sets of probability measu
   to the complement of `Kₙ` form a compact set.
 * `isCompact_closure_of_isTightMeasureSet`: Given a tight set of probability measures, its closure
   is compact.
+* `isTightMeasureSet_of_isCompact_closure`: In a second countable complete metric space, a set of
+  probability measures with compact closure is tight.
 
 Versions are also given for finite measures.
 
@@ -51,9 +54,13 @@ check the condition.
 
 public section
 
-open scoped ENNReal NNReal CompactlySupported
-open Filter Function Set Topology TopologicalSpace MeasureTheory BoundedContinuousFunction
-  MeasureTheory.FiniteMeasure
+open scoped CompactlySupported
+open Metric ENNReal NNReal Filter Set Topology TopologicalSpace MeasureTheory
+  BoundedContinuousFunction
+
+section Forward
+
+open FiniteMeasure
 
 variable {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [T2Space E] [BorelSpace E]
 
@@ -525,3 +532,151 @@ lemma isCompact_closure_of_isTightMeasureSet {S : Set (ProbabilityMeasure E)}
     apply subset_biUnion_of_mem
     exact le_rfl (a := n)
   _ ≤ u n := by grind
+
+end Forward
+
+section Backward
+
+open ProbabilityMeasure
+
+namespace MeasureTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} [PseudoMetricSpace 𝓧]
+  [OpensMeasurableSpace 𝓧] [SecondCountableTopology 𝓧] {S : Set (ProbabilityMeasure 𝓧)}
+
+lemma exists_measure_iUnion_gt_of_isCompact_closure
+    (U : ℕ → Set 𝓧) (O : ∀ i, IsOpen (U i)) (Cov : ⋃ i, U i = univ) (hcomp : IsCompact (closure S))
+    (ε : ℝ≥0∞) (hε : 0 < ε) (hεbound : ε ≤ 1) :
+    ∃ (k : ℕ), ∀ μ ∈ S, 1 - ε < μ (⋃ i ≤ k, U i) := by
+  have εfin : ε ≠ ∞ := ne_top_of_le_ne_top (by simp) hεbound
+  lift ε to ℝ≥0 using εfin
+  obtain ⟨ε, hε', rfl⟩ : ∃ (ε' : ℝ) (hε' : 0 ≤ ε'), ε = .mk ε' hε' := ⟨↑ε, ε.2, rfl⟩
+  simp only [ENNReal.coe_pos, ← NNReal.coe_lt_coe, NNReal.coe_zero, coe_mk, coe_le_one_iff,
+      ← NNReal.coe_le_coe, NNReal.coe_one] at hε hεbound
+  by_contra! nh
+  choose μ hμInS hcontradiction using nh
+  obtain ⟨μlim, _, sub, hsubmono, hμconverges⟩ :=
+      hcomp.isSeqCompact (fun n ↦ subset_closure <| hμInS n)
+  have Measurebound n : (μlim (⋃ (i ≤ n), U i) : ℝ) ≤ 1 - ε := calc
+    (μlim (⋃ (i ≤ n), U i) : ℝ)
+    _ ≤ liminf (fun k ↦ (μ (sub k) (⋃ (i ≤ n), U i) : ℝ)) atTop := by
+      have hopen : IsOpen (⋃ i ≤ n, U i) := isOpen_biUnion fun i a ↦ O i
+      have := ProbabilityMeasure.le_liminf_measure_open_of_tendsto hμconverges hopen
+      simp_rw [Function.comp_apply, ← ennreal_coeFn_eq_coeFn_toMeasure] at this
+      rw [← ofNNReal_liminf] at this
+      · exact mod_cast this
+      use 1
+      simpa [ge_iff_le, eventually_map, eventually_atTop, forall_exists_index] using fun _ x h ↦
+          (h x (by simp)).trans <| ProbabilityMeasure.apply_le_one (μ (sub x)) (⋃ i ≤ n, U i)
+    _ ≤ liminf (fun k ↦ (μ (sub k) (⋃ (i ≤ sub k), U i) : ℝ)) atTop := by
+      apply Filter.liminf_le_liminf
+      · simp only [NNReal.coe_le_coe, eventually_atTop, ge_iff_le]
+        use n + 1
+        intro b hypo
+        refine (μ (sub b)).apply_mono
+            <| Set.biUnion_mono (fun i (hi : i ≤ n) ↦ hi.trans ?_) fun _ _ ↦ le_rfl
+        exact le_trans (Nat.le_add_right n 1) (le_trans hypo (StrictMono.le_apply hsubmono))
+      · use 0; simp
+      · use 1
+        simpa [ge_iff_le, eventually_map, eventually_atTop, ge_iff_le, forall_exists_index] using
+            fun _ d hyp ↦ (hyp d (by simp)).trans (by simp)
+    _ ≤ 1 - ε := by
+      apply Filter.liminf_le_of_le
+      · use 0; simp
+      simp only [eventually_atTop, ge_iff_le, forall_exists_index]
+      intro b c h
+      apply le_trans (h c le_rfl)
+      refine (ofReal_le_ofReal_iff (by rw [sub_nonneg]; exact hεbound)).mp ?_
+      rw [ofReal_coe_nnreal]
+      apply le_trans (hcontradiction (sub c))
+      norm_cast
+  have accumulation : Tendsto (fun n ↦ μlim (⋃ i ≤ n, U i)) atTop (𝓝 (μlim (⋃ i, U i))) := by
+    simp_rw [← Set.accumulate_def, ProbabilityMeasure.tendsto_measure_iUnion_accumulate]
+  rw [Cov, coeFn_univ, ← NNReal.tendsto_coe] at accumulation
+  have exceeds_bound : ∀ᶠ n in atTop, (1 - ε / 2 : ℝ) ≤ μlim (⋃ i ≤ n, U i) :=
+      Tendsto.eventually_const_le (v := 1)
+        (by simp only [sub_lt_self_iff, Nat.ofNat_pos, div_pos_iff_of_pos_right]; positivity)
+        accumulation
+  suffices ∀ᶠ n : ℕ in atTop, False from this.exists.choose_spec
+  filter_upwards [exceeds_bound] with n hn
+  linarith [hn.trans <| Measurebound n]
+
+variable [CompleteSpace 𝓧]
+
+/-- In a second countable complete metric space, a set of probability measures with compact closure
+is tight. -/
+theorem isTightMeasureSet_of_isCompact_closure (hcomp : IsCompact (closure S)) :
+    IsTightMeasureSet {((μ : ProbabilityMeasure 𝓧) : Measure 𝓧) | μ ∈ S} := by
+  rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le]
+  rcases isEmpty_or_nonempty 𝓧 with hempty | hnonempty
+  · rw [← univ_eq_empty_iff] at hempty
+    exact fun ε εpos ↦ ⟨∅, isCompact_empty, by simp [hempty]⟩
+  obtain ⟨D, hD⟩ := exists_dense_seq 𝓧
+  obtain ⟨u, hu_anti, hu_pos, hu⟩ : ∃ u, StrictAnti u ∧ (∀ n, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
+    exists_seq_strictAnti_tendsto (0 : ℝ)
+  have hcov (m : ℕ) : ⋃ i, ball (D i) (u m) = univ := by
+    rw [denseRange_iff] at hD
+    ext p
+    exact ⟨fun a ↦ trivial, fun _ ↦ mem_iUnion.mpr <| hD p (u m) (hu_pos m)⟩
+  intro ε εpos
+  rcases lt_or_ge 1 ε with hεbound | hεbound
+  · refine ⟨∅, isCompact_empty, fun μ hμ ↦ ?_⟩
+    simp only [mem_setOf_eq] at hμ
+    obtain ⟨μ', hμ', rfl⟩ := hμ
+    rw [compl_empty, measure_univ]
+    exact le_of_lt hεbound
+  have byclaim (m : ℕ) : ∃ k, ∀ μ ∈ S, 1 - (ε * 2 ^ (-m : ℤ) : ℝ≥0∞) <
+      μ (⋃ i ≤ k, ball (D i) (u m)) := by
+    refine exists_measure_iUnion_gt_of_isCompact_closure
+      (fun i ↦ ball (D i) (u m)) (fun _ ↦ isOpen_ball) (hcov m) hcomp (ε * 2 ^ (-m : ℤ)) ?_ ?_
+    · simpa using ⟨εpos, (ENNReal.zpow_pos (by simp) (by simp) (-↑m))⟩
+    · exact Left.mul_le_one hεbound <| zpow_le_one_of_nonpos (by linarith) (by simp)
+  choose! km hbound using byclaim
+  -- This is a set we can construct to show tightness
+  let bigK := ⋂ m, ⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m))
+  have bigcalc (μ : ProbabilityMeasure 𝓧) (hs : μ ∈ S) : μ.toMeasure bigKᶜ ≤ ε := calc
+    μ.toMeasure bigKᶜ
+    _ = μ.toMeasure (⋃ m, (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))ᶜ) := by simp [bigK]
+    _ ≤ ∑' m, μ.toMeasure (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))ᶜ :=
+      measure_iUnion_le _
+    _ = ∑' m, (1 - μ.toMeasure (⋃ (i ≤ km (m + 1)), closure (ball (D i) (u m)))) := by
+      congr! with m; rw [measure_compl (by measurability) (by simp)]; simp
+    _ ≤ (∑' (m : ℕ), (ε : ℝ≥0∞) * 2 ^ (-(m + 1) : ℤ)) := by
+      refine ENNReal.tsum_le_tsum fun m ↦ tsub_le_iff_tsub_le.mp ?_
+      replace hbound := (hbound (m + 1) μ hs).le
+      simp_all only [neg_add_rev, Int.reduceNeg, tsub_le_iff_right, Nat.cast_add, Nat.cast_one,
+          ← coe_ofNat, ← ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
+      grw [hbound]
+      gcongr with i hi
+      grw [← subset_closure (s := ball (D i) (u m)), ball_subset_ball]
+      exact hu_anti.antitone (by grind)
+    _ = ε := by
+      rw [ENNReal.tsum_mul_left]
+      nth_rw 2 [← mul_one (a := ε)]
+      congr
+      ring_nf
+      exact tsum_two_zpow_neg_add_one
+  -- Final proof
+  refine ⟨bigK, ?_, by simpa⟩
+  -- Compactness first
+  refine TotallyBounded.isCompact_of_isClosed ?_ ?_
+  --Totally bounded
+  · refine Metric.totallyBounded_iff.mpr fun δ δpos ↦ ?_
+    have ⟨δ_inv, hδ_inv⟩ : ∃ x, u x < δ := (Tendsto.eventually_lt_const δpos hu).exists
+    refine ⟨D '' .Iic (km (δ_inv + 1)), (Set.finite_Iic _).image _, ?_⟩
+    -- t should be image under D of the set of numbers less than km of δ_inv
+    simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, bigK]
+    calc
+        ⋂ m, ⋃ i ≤ km (m + 1), closure (ball (D i) (u m))
+    _ ⊆ ⋃ i ≤ km (δ_inv + 1), closure (ball (D i) (u δ_inv)) := iInter_subset ..
+    _ ⊆ ⋃ i ≤ km (δ_inv + 1), ball (D i) δ := by
+        gcongr
+        exact closure_ball_subset_closedBall.trans <| closedBall_subset_ball <| hδ_inv
+  -- Closedness
+  · simp_rw [bigK, ← Set.mem_Iic]
+    exact isClosed_iInter fun n =>
+      Finite.isClosed_biUnion (finite_Iic _) (fun _ _ ↦ isClosed_closure)
+
+end MeasureTheory -- namespace
+
+end Backward