Order properties of extended non-negative reals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ≤ filter.limsup u f
theorem
ennreal.limsup_eq_zero_iff
{α : Type u_1}
{f : filter α}
[countable_Inter_filter 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 (λ (x : α), a * u x) f = a * filter.limsup u f
theorem
ennreal.limsup_const_mul
{α : Type u_1}
{f : filter α}
[countable_Inter_filter f]
{u : α → ennreal}
{a : ennreal} :
filter.limsup (λ (x : α), a * u x) f = a * filter.limsup u f
theorem
ennreal.limsup_mul_le
{α : Type u_1}
{f : filter α}
[countable_Inter_filter f]
(u v : α → ennreal) :
filter.limsup (u * v) f ≤ filter.limsup u f * filter.limsup v f
theorem
ennreal.limsup_add_le
{α : Type u_1}
{f : filter α}
[countable_Inter_filter 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 α}
[countable_Inter_filter f]
{g : filter β}
(u : α → β → ennreal) :
filter.limsup (λ (a : α), filter.liminf (λ (b : β), u a b) g) f ≤ filter.liminf (λ (b : β), filter.limsup (λ (a : α), u a b) f) g