English
For a sequence of probability measures, the open-set liminf inequality is equivalent to the closed-set limsup inequality.
Русский
Для последовательности вероятностных мер открытое неравенство liminf эквивалентно замкнутому неравенству limsup.
LaTeX
$$$\forall \mathcal{F}\text{ IsClosed},\; \forall \mathcal{G}\text{ IsOpen},\; (\text{Closed-Limsup} \iff \text{Open-Liminf})$$$
Lean4
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that if a set is clopen, then the limit of the
measures of the set equals the measure of the set under the limit probability measure.
-/
theorem tendsto_measure_of_isClopen_of_tendsto {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω]
[OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω}
(μs_lim : Tendsto μs L (𝓝 μ)) {E : Set Ω} (hE : IsClopen E) : Tendsto (fun i ↦ μs i E) L (𝓝 (μ E)) :=
ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto μs_lim (by simp [hE])
