Documentation

Mathlib.Order.Filter.ENNReal

Limsup and liminf of reals #

This file compiles filter-related results about ℝ, ℝ≥0 and ℝ≥0∞.

source
@[simp]
theorem Real.limsSup_of_not_isCobounded {f : Filter ℝ} (hf : ¬Filter.IsCobounded (fun (x1 x2 : ℝ) => x1 ≤ x2) f) :
f.limsSup = 0
source
@[simp]
theorem Real.limsSup_of_not_isBounded {f : Filter ℝ} (hf : ¬Filter.IsBounded (fun (x1 x2 : ℝ) => x1 ≤ x2) f) :
f.limsSup = 0
source
@[simp]
theorem Real.limsInf_of_not_isCobounded {f : Filter ℝ} (hf : ¬Filter.IsCobounded (fun (x1 x2 : ℝ) => x1 ≥ x2) f) :
f.limsInf = 0
source
@[simp]
theorem Real.limsInf_of_not_isBounded {f : Filter ℝ} (hf : ¬Filter.IsBounded (fun (x1 x2 : ℝ) => x1 ≥ x2) f) :
f.limsInf = 0
source
@[simp]
theorem Real.limsup_of_not_isCoboundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) :
Filter.limsup u f = 0
source
@[simp]
theorem Real.limsup_of_not_isBoundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) :
Filter.limsup u f = 0
source
@[simp]
theorem Real.liminf_of_not_isCoboundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f u) :
Filter.liminf u f = 0
source
@[simp]
theorem Real.liminf_of_not_isBoundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f u) :
Filter.liminf u f = 0
source
@[simp]
theorem NNReal.isBoundedUnder_le_toReal {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :
(Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f fun (i : ι) => ↑(u i)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) f u
source
@[simp]
theorem NNReal.isBoundedUnder_ge_toReal {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :
(Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f fun (i : ι) => ↑(u i)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≥ x2) f u
source
@[simp]
theorem NNReal.isCoboundedUnder_le_toReal {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} [f.NeBot] :
(Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f fun (i : ι) => ↑(u i)) ↔ Filter.IsCoboundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) f u
source
@[simp]
theorem NNReal.isCoboundedUnder_ge_toReal {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :
(Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f fun (i : ι) => ↑(u i)) ↔ Filter.IsCoboundedUnder (fun (x1 x2 : NNReal) => x1 ≥ x2) f u
source
@[simp]
theorem NNReal.limsSup_of_not_isBounded {f : Filter NNReal} (hf : ¬Filter.IsBounded (fun (x1 x2 : NNReal) => x1 ≤ x2) f) :
f.limsSup = 0
source
@[simp]
theorem NNReal.limsInf_of_not_isCobounded {f : Filter NNReal} (hf : ¬Filter.IsCobounded (fun (x1 x2 : NNReal) => x1 ≥ x2) f) :
f.limsInf = 0
source
@[simp]
theorem NNReal.limsup_of_not_isBoundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} (hf : ¬Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) f u) :
Filter.limsup u f = 0
source
@[simp]
theorem NNReal.liminf_of_not_isCoboundedUnder {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} (hf : ¬Filter.IsCoboundedUnder (fun (x1 x2 : NNReal) => x1 ≥ x2) f u) :
Filter.liminf u f = 0
source
@[simp]
theorem NNReal.toReal_liminf {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :
Filter.liminf (fun (i : ι) => ↑(u i)) f = ↑(Filter.liminf u f)
source
@[simp]
theorem NNReal.toReal_limsup {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :
Filter.limsup (fun (i : ι) => ↑(u i)) f = ↑(Filter.limsup u f)
source
theorem ENNReal.eventually_le_limsup {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : α → ENNReal) :
∀ᶠ (y : α) in f, u y ≤ Filter.limsup u f
source
theorem ENNReal.limsup_eq_zero_iff {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} :
Filter.limsup u f = 0 ↔ u =ᶠ[f] 0
source
theorem ENNReal.limsup_const_mul_of_ne_top {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) :
Filter.limsup (fun (x : α) => a * u x) f = a * Filter.limsup u f
source
theorem ENNReal.limsup_const_mul {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal} :
Filter.limsup (fun (x : α) => a * u x) f = a * Filter.limsup u f
source
theorem ENNReal.limsup_mul_le {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal) :
Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f

See also limsup_mul_le'

source
theorem ENNReal.limsup_add_le {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal) :
Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
source
theorem ENNReal.limsup_liminf_le_liminf_limsup {α : Type u_1} {β : Type u_2} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β} (u : α → β → ENNReal) :
Filter.limsup (fun (a : α) => Filter.liminf (fun (b : β) => u a b) g) f ≤ Filter.liminf (fun (b : β) => Filter.limsup (fun (a : α) => u a b) f) g