Order properties of extended non-negative reals

This file compiles filter-related results about ℝ≥0∞ (see Data/Real/ENNReal.lean).

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_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_le {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : α → ENNReal) (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 : α → ENNReal) (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