limsup_measure_le_of_le_liminf_measure_compl

English

If a sequence of measures μ_s(i) converges to μ on a topological space, then for any closed set F, limsup_i μ_s(i,F) ≤ μ(F).

Русский

Если последовательность мер μ_s(i) сходится к μ, то для любого замкнутого множества F выполняется limsup_i μ_s(i,F) ≤ μ(F).

LaTeX

$$$\forall F\text{ closed},\; \limsup_i (\mu_i(F)) \le \mu(F)$$$

Lean4

theorem limsup_measure_le_of_le_liminf_measure_compl {ι : Type*} {L : Filter ι} {μ : Measure Ω} {μs : ι → Measure Ω}
    [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E)
    (h : μ Eᶜ ≤ L.liminf fun i ↦ μs i Eᶜ) : (L.limsup fun i ↦ μs i E) ≤ μ E :=
  compl_compl E ▸ limsup_measure_compl_le_of_le_liminf_measure (MeasurableSet.compl E_mble) h

Похожие утверждения