English
For a family of probability measures, the following are equivalent: (a) for every closed F, limsup μ_s(i,F) ≤ μ(F); (b) for every open G, μ(G) ≤ liminf μ_s(i,G).
Русский
Для семейства распределений вероятность эквивалентна: (a) для каждого замкнутого F выполняется limsup μ_s(i,F) ≤ μ(F); (b) для каждого открытого G выполняется μ(G) ≤ liminf μ_s(i,G).
LaTeX
$$$\forall F\text{ IsClosed}(F)\; (\limsup_i μ_s(i,F) \le μ(F)) \iff \forall G\; (IsOpen(G) \Rightarrow μ(G) \le \liminf_i μ_s(i,G))$$$
Lean4
/-- One pair of implications of the portmanteau theorem:
For a sequence of Borel probability measures, the following two are equivalent:
(C) The limsup of the measures of any closed set is at most the measure of the closed set
under a candidate limit measure.
(O) The liminf of the measures of any open set is at least the measure of the open set
under a candidate limit measure.
-/
theorem limsup_measure_closed_le_iff_liminf_measure_open_ge {ι : Type*} {L : Filter ι} {μ : Measure Ω}
{μs : ι → Measure Ω} [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] :
(∀ F, IsClosed F → (L.limsup fun i ↦ μs i F) ≤ μ F) ↔ ∀ G, IsOpen G → μ G ≤ L.liminf fun i ↦ μs i G :=
by
constructor
· intro h G G_open
exact le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet (h Gᶜ (isClosed_compl_iff.mpr G_open))
· intro h F F_closed
exact limsup_measure_le_of_le_liminf_measure_compl F_closed.measurableSet (h Fᶜ (isOpen_compl_iff.mpr F_closed))
