English
For a measurable E, if the limsup of μ_s(i,E) is bounded by μ(E), then the limsup of μ_s(i,Eᶜ) is bounded by μ(Eᶜ).
Русский
Для измеримого E, если limsup μ_s(i,E) ≤ μ(E), то limsup μ_s(i,Eᶜ) ≤ μ(Eᶜ).
LaTeX
$$$\text{Measurable}(E) \land \Bigl( \limsup_i \mu_s(i,E) \le \mu(E) \Bigr) \Rightarrow \limsup_i \mu_s(i,E^c) \le \mu(E^c)$$$
Lean4
theorem limsup_measure_compl_le_of_le_liminf_measure {ι : 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ᶜ :=
by
rcases L.eq_or_neBot with rfl | hne
· simp only [limsup_bot, bot_le]
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.limsup fun i : ι ↦ 1 - μs i E) = L.limsup ((fun x ↦ 1 - x) ∘ fun i : ι ↦ μs i E) from rfl]
have key :=
antitone_const_tsub.map_liminf_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
