case hinf
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L

case hsup
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E

case h
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ↑↑(μs i) E) _auto✝

case h'
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ↑↑(μs i) E) _auto✝
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ Tendsto (fun i => ↑↑(μs i) E) L (𝓝 (↑↑μ E))
apply tendsto_of_le_liminf_of_limsup_le
case hinf
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
E₀_ae_eq_E : E₀ =ᵐ[μ] E
⊢ ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
case hinf
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
have E₀_ae_eq_E : E₀ =ᵐ[μ] E :=
  EventuallyLE.antisymm E₀_subset.eventuallyLE
    (subset_E₁.eventuallyLE.trans (ae_le_set.mpr nulldiff))
no goals
case hinf
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
E₀_ae_eq_E : E₀ =ᵐ[μ] E
⊢ ↑↑μ E ≤ liminf (fun i => ↑↑(μs i) E) L
calc
  μ E = μ E₀ := measure_congr E₀_ae_eq_E.symm
  _ ≤ L.liminf fun i => μs i E₀ := h_E₀
  _ ≤ L.liminf fun i => μs i E :=
    liminf_le_liminf (eventually_of_forall fun _ => measure_mono E₀_subset)
case hsup
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
E_ae_eq_E₁ : E =ᵐ[μ] E₁
⊢ limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
case hsup
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
have E_ae_eq_E₁ : E =ᵐ[μ] E₁ :=
  EventuallyLE.antisymm subset_E₁.eventuallyLE
    ((ae_le_set.mpr nulldiff).trans E₀_subset.eventuallyLE)
no goals
case hsup
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
E_ae_eq_E₁ : E =ᵐ[μ] E₁
⊢ limsup (fun i => ↑↑(μs i) E) L ≤ ↑↑μ E
calc
  (L.limsup fun i => μs i E) ≤ L.limsup fun i => μs i E₁ :=
    limsup_le_limsup (eventually_of_forall fun _ => measure_mono subset_E₁)
  _ ≤ μ E₁ := h_E₁
  _ = μ E := measure_congr E_ae_eq_E₁.symm
no goals
case h
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ↑↑(μs i) E) _auto✝
infer_param
no goals
case h'
Ω : Type u_2
inst✝ : MeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : ↑↑μ (E₁ \ E₀) = 0
h_E₀ : ↑↑μ E₀ ≤ liminf (fun i => ↑↑(μs i) E₀) L
h_E₁ : limsup (fun i => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁
⊢ autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ↑↑(μs i) E) _auto✝
infer_param