English
If for every open G and every measurable E with frontier E mass zero, μ_s(i,E) → μ(E), then the limsup over closed F is controlled by μ(F).
Русский
Если для каждого открытого G и каждого измеримого E с нулевой массой по фронтиру μ_s(i,E) сходится к μ(E), то на замкнутых F лимсуп ограничен μ(F).
LaTeX
$$$\forall E\, (\text{Measurable}(E) \land μ(\text{frontier}(E)) = 0 \Rightarrow Tendsto (i\mapsto μ_s(i,E)) L (\mathcal{N}(μ(E)))) \Rightarrow \forall F,\; F\text{ closed} \Rightarrow L.limsup (i\mapsto μ_s(i,F)) ≤ μ(F)$$$
Lean4
/-- Given a π-system, if a sequence of probability measures converges along all elements of
the π-system, then it also converges along finite unions of elements of the π-system. -/
theorem _root_.IsPiSystem.tendsto_probabilityMeasure_biUnion {S : Set (Set Ω)} (hS : IsPiSystem S)
{μ : ι → ProbabilityMeasure Ω} {ν : ProbabilityMeasure Ω} {l : Filter ι} {t : Finset (Set Ω)} (ht : ∀ s ∈ t, s ∈ S)
(hmeas : ∀ s ∈ S, MeasurableSet s) (h : ∀ s ∈ S, Tendsto (fun i ↦ μ i s) l (𝓝 (ν s))) :
Tendsto (fun i ↦ μ i (⋃ s ∈ t, s)) l (𝓝 (ν (⋃ s ∈ t, s))) :=
by
have : Tendsto (fun i ↦ (μ i : Measure Ω).real (⋃ s ∈ t, s)) l (𝓝 ((ν : Measure Ω).real (⋃ s ∈ t, s))) :=
by
apply hS.tendsto_measureReal_biUnion ht hmeas
simpa using h
simpa using this
