case pos
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : L = ⊥
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L

case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
by_cases L_bot : L = ⊥
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
have : L.NeBot := { ne' := L_bot }
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
have meas_Ec : μ (Eᶜ) = 1 - μ E := by
  simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
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
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ 1 - ↑↑μ E ≤ liminf (fun i => 1 - ↑↑(μs i) E) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
simp_rw [meas_Ec, meas_i_Ec]
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf (fun i => 1 - ↑↑(μs i) E) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ 1 - ↑↑μ E ≤ liminf (fun i => 1 - ↑↑(μs i) E) L
have obs :
  (L.liminf fun i : ι => 1 - μs i E) = L.liminf ((fun x => 1 - x) ∘ fun i : ι => μs i E) := by rfl
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf (fun i => 1 - ↑↑(μs i) E) L
rw [obs]
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - limsup (fun i => ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
have := antitone_const_tsub.map_limsup_of_continuousAt (F := L)
  (fun i => μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - limsup (fun i => ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ 1 - limsup (fun i => ↑↑(μs i) E) L
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - limsup (fun i => ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
simp_rw [← this]
no goals
case neg
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - limsup (fun i => ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - ↑↑μ E ≤ 1 - limsup (fun i => ↑↑(μs i) E) L
exact antitone_const_tsub h
no goals
case pos
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : L = ⊥
⊢ ↑↑μ (Eᶜ) ≤ liminf (fun i => ↑↑(μs i) (Eᶜ)) L
simp only [L_bot, le_top,
  show liminf (fun i => μs i (Eᶜ)) ⊥ = ⊤ by simp only [liminf, Filter.map_bot, limsInf_bot]]
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : L = ⊥
⊢ liminf (fun i => ↑↑(μs i) (Eᶜ)) ⊥ = ⊤
simp only [liminf, Filter.map_bot, limsInf_bot]
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
⊢ ↑↑μ (Eᶜ) = 1 - ↑↑μ E
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
i : ι
⊢ ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
⊢ ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
intro i
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
i : ι
⊢ ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ liminf (fun i => 1 - ↑↑(μs i) E) L = liminf ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
rfl