English
A collection of equivalent statements of Portmanteau: the limsup of closed sets is bounded by the limit measure if open-set convergence holds, and vice versa.
Русский
Сводка эквивалентных формул Портманто: лимсуп по замкнутым множествам ограничен пределом меры, если выполняется сходимость по открытым множествам, и наоборот.
LaTeX
$$$\text{Portmanteau equivalence: }(\forall F,\ F\text{ closed} \Rightarrow \limsup_i μ_s(i,F) ≤ μ(F)) \iff (\forall G,\ G\text{ open} \Rightarrow μ(G) ≤ \liminf_i μ_s(i,G))$$$
Lean4
/-- Consider a set of sets `S` containing arbitrarily small neighborhoods of any point, and a
probability measure. Then any open set can be approximated arbitrarily well in measure from inside
by a finite union of elements of `S`.
This is a technical lemma for `IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem`, which is
why it is formulated for a `ProbabilityMeasure`. If needed, this could be generalized to finite
measures or to general measures.
-/
theorem exists_lt_measure_biUnion_of_isOpen [TopologicalSpace Ω] [SecondCountableTopology Ω] {S : Set (Set Ω)}
(ν : ProbabilityMeasure Ω) (h : ∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u) {G : Set Ω}
(hG : IsOpen G) {r : ℝ≥0} (hr : r < ν G) :
∃ T : Finset (Set Ω), (∀ t ∈ T, t ∈ S) ∧ (r < ν (⋃ t ∈ T, t)) ∧ (⋃ t ∈ T, t) ⊆ G := by
classical
obtain ⟨T, TS, T_count, hT⟩ : ∃ T : Set (Set Ω), T ⊆ S ∧ T.Countable ∧ ⋃ t ∈ T, t = G :=
by
have : ∀ (x : G), ∃ s ∈ S, s ∈ 𝓝 (x : Ω) ∧ s ⊆ G := fun x ↦ h G hG x x.2
choose! s hsS hs_nhds hsG using this
rcases TopologicalSpace.isOpen_iUnion_countable (fun i ↦ interior (s i)) (fun i ↦ isOpen_interior) with
⟨T₀, T₀_count, hT₀⟩
refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
refine Subset.antisymm (by simp; grind) ?_
have : G ⊆ ⋃ i, interior (s i) := by
intro y hy
simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
apply this.trans
rw [← hT₀, biUnion_image]
exact iUnion₂_mono fun i j ↦ interior_subset
have : T.Nonempty := by
contrapose! hr
simp [← hT, hr]
rcases T_count.exists_eq_range this with ⟨f, hf⟩
have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
have : Tendsto (fun i ↦ ν (Accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
(ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
rw [← G_eq] at this
rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
· convert hn
simp [accumulate_def]
grind
· simpa [G_eq] using fun i _ ↦ subset_iUnion f i
