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 α} [countable_Inter_filter f] (u : α → ennreal) :

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

theorem ennreal.limsup_eq_zero_iff {α : Type u_1} {f : filter α} [countable_Inter_filter f] {u : α → ennreal} :

theorem ennreal.limsup_const_mul_of_ne_top {α : Type u_1} {f : filter α} {u : α → ennreal} {a : ennreal} (ha_top : a ≠ ⊤) :

f.limsup (λ (x : α), a * u x) = a * f.limsup u

theorem ennreal.limsup_const_mul {α : Type u_1} {f : filter α} [countable_Inter_filter f] {u : α → ennreal} {a : ennreal} :

f.limsup (λ (x : α), a * u x) = a * f.limsup u

theorem ennreal.limsup_add_le {α : Type u_1} {f : filter α} [countable_Inter_filter f] (u v : α → ennreal) :

theorem ennreal.limsup_liminf_le_liminf_limsup {α : Type u_1} {β : Type u_2} [countable β] {f : filter α} [countable_Inter_filter f] {g : filter β} (u : α → β → ennreal) :

f.limsup (λ (a : α), g.liminf (λ (b : β), u a b)) ≤ g.liminf (λ (b : β), f.limsup (λ (a : α), u a b))