English
A symmetric version: for certain convergence contexts, limsup of closed sets is bounded by the limit measure.
Русский
Симметричная версия: в некоторых случаях сходимости лимсуп по замкнутым множествам ограничен пределом меры.
LaTeX
$$$\text{limsup of closed sets} \le \text{limit measure}$$$
Lean4
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that the limsup of the measures of any closed
set is at most the measure of the closed set under the limit probability measure.
-/
theorem limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω]
[OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω}
(μs_lim : Tendsto μs L (𝓝 μ)) {F : Set Ω} (F_closed : IsClosed F) :
(L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F := by
apply
FiniteMeasure.limsup_measure_closed_le_of_tendsto ((tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds L).mp μs_lim)
F_closed
