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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : L = ⊥
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)

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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ limsup (fun i => 1 - ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup (fun i => 1 - ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ limsup (fun i => 1 - ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
have obs :
  (L.limsup fun i : ι => 1 - μs i E) = L.limsup ((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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup (fun i => 1 - ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - liminf (fun i => ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
have := antitone_const_tsub.map_liminf_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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - liminf (fun i => ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - liminf (fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - liminf (fun i => ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this✝ : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
obs : limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
this : 1 - liminf (fun i => ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
⊢ 1 - liminf (fun i => ↑↑(μs i) E) L ≤ 1 - ↑↑μ E
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : L = ⊥
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) L ≤ ↑↑μ (Eᶜ)
simp only [L_bot, bot_le,
  show limsup (fun i => μs i (Eᶜ)) ⊥ = ⊥ by simp only [limsup, Filter.map_bot, limsSup_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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : L = ⊥
⊢ limsup (fun i => ↑↑(μs i) (Eᶜ)) ⊥ = ⊥
simp only [limsup, Filter.map_bot, limsSup_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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
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 : ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
L_bot : ¬L = ⊥
this : NeBot L
meas_Ec : ↑↑μ (Eᶜ) = 1 - ↑↑μ E
meas_i_Ec : ∀ (i : ι), ↑↑(μs i) (Eᶜ) = 1 - ↑↑(μs i) E
⊢ limsup (fun i => 1 - ↑↑(μs i) E) L = limsup ((fun x => 1 - x) ∘ fun i => ↑↑(μs i) E) L
rfl