English
If E is clopen, the measures of E converge to the limit measure along the given filter.
Русский
Если E — клип (одновременно открытое и замкнутое), то мера E сходится к пределу по заданному фильтру.
LaTeX
$$$\forall E\; (\text{Clopen}(E)) \Rightarrow \text{Tendsto} (i\mapsto μ_s(i,E)) L (\mathcal{N}(μ(E)))$$$
Lean4
/-- 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 μ.
Superseded by `tendsto_of_forall_isOpen_le_liminf` which works for all countably
generated filters. -/
theorem tendsto_of_forall_isOpen_le_liminf_nat {μ : 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
have aux : ENNReal.ofNNReal (liminf (fun i ↦ μs i G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i ↦ μs i G) atTop :=
by
refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
· exact ENNReal.continuous_coe.continuousAt
· exact IsBoundedUnder.isCoboundedUnder_ge ⟨1, by simp⟩
· exact ⟨0, by simp⟩
have obs := ENNReal.coe_mono h_opens
simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure, aux] at obs
convert obs
simp only [Function.comp_apply, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]
