[Merged by Bors] - feat(MeasureTheory/Measure/Tight): portmanteau condition for compact sets

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