English
Let S be a π-system of subsets of Ω that generates the measurable sets and contains arbitrarily small neighborhoods of every point, and let μ_i be probability measures on Ω with limit ν. If μ_i(s) → ν(s) for every s ∈ S and the neighborhood condition holds, then μ_i converges to ν in the weak topology: μ_i ⇒ ν.
Русский
Пусть S — π-система подмножеств Ω, которая порождает измеримые множества и содержит произвольные маленькие окрестности любой точки; μ_i — последовательность распределений, сходящаяся к ν на каждом s ∈ S, и выполняются условия локализации. Тогда μ_i сходятся к ν в слабой топологии: μ_i ⇒ ν.
LaTeX
$$$IsPiSystem(S) \wedge \\bigl(\\forall s\\in S, MeasurableSet(s)\\bigr) \\wedge \\Bigl(\\forall u\\, IsOpen(u) \\rightarrow \\forall x\\in u, \\exists s\\in S, s \\in 𝓝 x \\wedge s \\subseteq u\\Bigr) \\wedge \\Bigl(\\forall s\\in S, Tendsto (\\lambda i. μ_i(s)) l (𝓝 (ν(s)))\\Bigr) \\rightarrow Tendsto μ l (𝓝 ν)$$$
Lean4
/-- Assume that, applied to all the elements of a π-system, a sequence of probability measures
converges to a limiting probability measure. Assume also that the π-system contains arbitrarily
small neighborhoods of any point. Then the sequence of probability measures converges for the
weak topology. -/
theorem _root_.IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem [TopologicalSpace Ω] [SecondCountableTopology Ω]
[OpensMeasurableSpace Ω] {S : Set (Set Ω)} (hS : IsPiSystem S) {μ : ι → ProbabilityMeasure Ω}
{ν : ProbabilityMeasure Ω} {l : Filter ι} [l.IsCountablyGenerated] (hmeas : ∀ s ∈ S, MeasurableSet s)
(h : ∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u)
(h' : ∀ s ∈ S, Tendsto (fun i ↦ μ i s) l (𝓝 (ν s))) : Tendsto μ l (𝓝 ν) := by
/- We apply the portmanteau theorem: it suffices to show that, given an open set `G`
and `r < ν G`, then for large `i` one has `r < μᵢ G`. For this, we approximate `G` from inside by
a finite union `G'` of elements of `S`, still with measure `> r`, by Lemma
`ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen`. If we have `μᵢ G' → ν G'`,
then we deduce `r < μᵢ G'` for large `i`, and therefore `r < μᵢ G`.
Our assumption does not give directly `μᵢ G' → ν G'`, as `G'` does not belong to the π-system `S`.
However, the inclusion-exclusion formula makes it possible to express `μᵢ G'` and `ν G'` in terms
of the measures of intersections of elements of `S`, for which we have the convergence. It follows
that `μᵢ G' → ν G'` holds, concluding the proof. This second step is already formalized in the
lemma `IsPiSystem.tendsto_probabilityMeasure_biUnion`. -/
rcases l.eq_or_neBot with rfl | hl
· simp
apply tendsto_of_forall_isOpen_le_liminf
intro G hG
refine (le_liminf_iff (isCoboundedUnder_ge_of_le (x := 1) l (by simp)) (by isBoundedDefault)).2 (fun r hr ↦ ?_)
obtain ⟨T, TS, T_meas, TG⟩ : ∃ T : Finset (Set Ω), (∀ t ∈ T, t ∈ S) ∧ (r < ν (⋃ t ∈ T, t)) ∧ (⋃ t ∈ T, t) ⊆ G :=
ν.exists_lt_measure_biUnion_of_isOpen h hG hr
have : Tendsto (fun i ↦ μ i (⋃ t ∈ T, t)) l (𝓝 (ν (⋃ t ∈ T, t))) := hS.tendsto_probabilityMeasure_biUnion TS hmeas h'
filter_upwards [(tendsto_order.1 this).1 r T_meas] with i hi
exact hi.trans_le <| ProbabilityMeasure.apply_mono _ TG
