English
If for all open sets G we have μ(G) ≤ L.liminf μ_s(i,G) and frontier(E) carries zero mass under μ, then μ_s(i,E) → μ(E).
Русский
Если для всех открытых множеств G верно μ(G) ≤ L.liminf μ_s(i,G) и фронтир E имеет нулевую массу μ, тогда μ_s(i,E) сходится к μ(E).
LaTeX
$$$\forall G\, (\text{IsOpen}(G) \Rightarrow μ(G) \le L.liminf_i μ_s(i,G)) \land μ(\text{frontier}(E)) = 0 \Rightarrow \ Tendsto_i μ_s(i,E) \to μ(E)$$$
Lean4
/-- One implication of the portmanteau theorem:
For a sequence of Borel probability measures, if the liminf of the measures of any open set is at
least the measure of the open set under a candidate limit measure, then for any set whose
boundary carries no probability mass under the candidate limit measure, then its measures under the
sequence converge to its measure under the candidate limit measure.
-/
theorem tendsto_measure_of_null_frontier {ι : Type*} {L : Filter ι} {μ : Measure Ω} {μs : ι → Measure Ω}
[IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)]
(h_opens : ∀ G, IsOpen G → μ G ≤ L.liminf fun i ↦ μs i G) {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) :
L.Tendsto (fun i ↦ μs i E) (𝓝 (μ E)) :=
haveI h_closeds : ∀ F, IsClosed F → (L.limsup fun i ↦ μs i F) ≤ μ F :=
limsup_measure_closed_le_iff_liminf_measure_open_ge.mpr h_opens
tendsto_measure_of_le_liminf_measure_of_limsup_measure_le interior_subset subset_closure E_nullbdry
(h_opens _ isOpen_interior) (h_closeds _ isClosed_closure)
