English
If μ(G) ≤ liminf μ_s(i,G) for all open G, then μ is the limit of μ_s along the open sets, i.e., convergence on opens.
Русский
Если для всех открытых G верно μ(G) ≤ liminf μ_s(i,G), то сходимость μ_s к μ holds on open sets.
LaTeX
$$$\forall G\text{ open},\; μ(G) \le \liminf_i μ_s(i,G)$$$
Lean4
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that the liminf of the measures of any open set
is at least the measure of the open set under the limit probability measure.
-/
theorem le_liminf_measure_open_of_tendsto {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω]
[OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω}
(μs_lim : Tendsto μs L (𝓝 μ)) {G : Set Ω} (G_open : IsOpen G) :
(μ : Measure Ω) G ≤ L.liminf fun i ↦ (μs i : Measure Ω) G :=
haveI h_closeds : ∀ F, IsClosed F → (L.limsup fun i ↦ (μs i : Measure Ω) F) ≤ (μ : Measure Ω) F := fun _ F_closed ↦
limsup_measure_closed_le_of_tendsto μs_lim F_closed
le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet (h_closeds _ (isClosed_compl_iff.mpr G_open))
