le_measure_liminf_of_limsup_measure_compl_le

English

For a measurable E, if the limsup of the complements Eᶜ is below μ(Eᶜ), then μ(E) is below the limsup of the complements, i.e., μ(E) ≤ limsup μ_s(i,Eᶜ).

Русский

Пусть E измеримо. Если limsup по Eᶜ ниже μ(Eᶜ), то μ(E) не превосходит limsup по Eᶜ, то есть μ(E) ≤ limsup μ_s(i,Eᶜ).

LaTeX

$$$\text{Measurable}(E) \Rightarrow \Bigl( \mu(E^c) \le \liminf_i \mu_i(E^c) \Bigr) \Rightarrow \mu(E) \le \limsup_i \mu_i(E^c)$$$

Lean4

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

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