le_measure_compl_liminf_of_limsup_measure_le

English

If E is measurable and the limsup of the measures of E under the sequence is bounded above by μ(E), then the liminf of the measures of E's complement is bounded above by μ(Eᶜ).

Русский

Пусть E измеримо. Если верхняя граница по лимит-сукупностям мер E над последовательностью не превосходит μ(E), то верхняя граница по лимит-нижним мерам комплемента E не превосходит μ(Еᶜ).

LaTeX

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

Lean4

theorem le_measure_compl_liminf_of_limsup_measure_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ᶜ :=
  by
  rcases L.eq_or_neBot with rfl | hne
  · simp only [liminf_bot, le_top]
  have meas_Ec : μ Eᶜ = 1 - μ E := by simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
  have meas_i_Ec : ∀ i, μs i Eᶜ = 1 - μs i E := by
    intro i
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
  simp_rw [meas_Ec, meas_i_Ec]
  rw [show (L.liminf fun i : ι ↦ 1 - μs i E) = L.liminf ((fun x ↦ 1 - x) ∘ fun i : ι ↦ μs i E) from rfl]
  have key :=
    antitone_const_tsub.map_limsup_of_continuousAt (F := L) (fun i ↦ μs i E)
      (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
  simpa [← key] using antitone_const_tsub h

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