English
If for all E with frontier E measure zero the convergence μ_s(i,E) → μ(E) holds, then for all open G, μ(G) ≤ liminf μ_s(i,G).
Русский
Если для всех E с μ(frontier E)=0 верна сходимость μ_s(i,E) → μ(E), тогда для всех открытых G верно μ(G) ≤ liminf μ_s(i,G).
LaTeX
$$$\bigl( \forall E,\; \text{Measurable}(E) \land μ(\text{frontier}(E)) = 0 \Rightarrow Tendsto (i\mapsto μ_s(i,E)) L (\mathcal{N}(μ(E))) \bigr) \Rightarrow \forall G,\; G\text{ open} \Rightarrow μ(G) \le L.liminf (i\mapsto μ_s(i,G))$$$
Lean4
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all open sets G we have the limsup condition μ(G) ≤ liminf μsᵢ(G). -/
theorem le_liminf_measure_open_of_forall_tendsto_measure {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω]
[TopologicalSpace Ω] [PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{μs : ι → Measure Ω} [∀ i, IsProbabilityMeasure (μs i)]
(h : ∀ {E}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ μs i E) L (𝓝 (μ E))) (G : Set Ω)
(G_open : IsOpen G) : μ G ≤ L.liminf (fun i ↦ μs i G) :=
by
apply le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet
exact limsup_measure_closed_le_of_forall_tendsto_measure h _ (isClosed_compl_iff.mpr G_open)
