Documentation

Mathlib.Order.Filter.ENNReal

Limsup and liminf of reals #

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

@[simp]

theorem Real.limsSup_of_not_isCobounded {f : Filter ℝ} (hf : ¬Filter.IsCobounded (fun (x1 x2 : ℝ) => x1 ≤ x2) f) :

@[simp]

theorem Real.limsSup_of_not_isBounded {f : Filter ℝ} (hf : ¬Filter.IsBounded (fun (x1 x2 : ℝ) => x1 ≤ x2) f) :

@[simp]

theorem Real.limsInf_of_not_isCobounded {f : Filter ℝ} (hf : ¬Filter.IsCobounded (fun (x1 x2 : ℝ) => x1 ≥ x2) f) :

@[simp]

theorem Real.limsInf_of_not_isBounded {f : Filter ℝ} (hf : ¬Filter.IsBounded (fun (x1 x2 : ℝ) => x1 ≥ x2) f) :

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[simp]

theorem NNReal.limsSup_of_not_isBounded {f : Filter NNReal} (hf : ¬Filter.IsBounded (fun (x1 x2 : NNReal) => x1 ≤ x2) f) :

@[simp]

theorem NNReal.limsInf_of_not_isCobounded {f : Filter NNReal} (hf : ¬Filter.IsCobounded (fun (x1 x2 : NNReal) => x1 ≥ x2) f) :

@[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

@[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

@[simp]

theorem NNReal.toReal_liminf {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :

Filter.liminf (fun (i : ι) => ↑(u i)) f = ↑(Filter.liminf u f)

@[simp]

theorem NNReal.toReal_limsup {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} :

Filter.limsup (fun (i : ι) => ↑(u i)) f = ↑(Filter.limsup u f)

theorem ENNReal.eventually_le_limsup {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : α → ENNReal) :

∀ᶠ (y : α) in f, u y ≤ Filter.limsup u f

theorem ENNReal.limsup_eq_zero_iff {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} :

Filter.limsup u f = 0 ↔ u =ᶠ[f] 0

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

theorem ENNReal.limsup_mul_const_of_ne_top {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) :

Filter.limsup (fun (x : α) => u x * a) f = a * Filter.limsup u f

theorem ENNReal.liminf_const_mul_of_ne_zero_of_ne_top {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

Filter.liminf (fun (x : α) => a * u x) f = a * Filter.liminf u f

theorem ENNReal.liminf_mul_const_of_ne_zero_of_ne_top {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

Filter.liminf (fun (x : α) => u x * a) f = a * Filter.liminf u f

theorem ENNReal.liminf_const_mul_of_ne_top {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) :

Filter.liminf (fun (x : α) => a * u x) f = a * Filter.liminf u f

theorem ENNReal.liminf_mul_const_of_ne_top {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) :

Filter.liminf (fun (x : α) => u x * a) f = a * Filter.liminf u f

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

theorem ENNReal.limsup_mul_const {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal} :

Filter.limsup (fun (x : α) => u x * a) f = a * Filter.limsup u f

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'

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

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

theorem ENNReal.ofReal_limsup {α : Type u_1} {f : Filter α} {u : α → ℝ} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u := by isBoundedDefault) :

ENNReal.ofReal (Filter.limsup u f) = Filter.limsup (fun (a : α) => ENNReal.ofReal (u a)) f

theorem ENNReal.ofReal_limsup_toReal {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {C : NNReal} (hf : ∀ᶠ (a : α) in f, u a ≤ ↑C) :

ENNReal.ofReal (Filter.limsup (fun (a : α) => (u a).toReal) f) = Filter.limsup u f

theorem ENNReal.toReal_limsup {α : Type u_1} {f : Filter α} {u : α → ENNReal} (h₁ : ∀ᶠ (a : α) in f, u a ≠ ⊤) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f fun (a : α) => (u a).toReal := by isBoundedDefault) :

(Filter.limsup u f).toReal = Filter.limsup (fun (a : α) => (u a).toReal) f