mathlib documentation

data.real.ennreal

Extended non-negative reals #

We define ennreal = ℝ≥0∞ := with_top ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a measure_theory.measure, and of the extended distance edist in a emetric_space. In this file we define some algebraic operations and a linear order on ℝ≥0∞ and prove basic properties of these operations, order, and conversions to/from , ℝ≥0, and .

Main definitions #

Implementation notes #

We define a can_lift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

Notations #

@[protected, instance]
def ennreal  :
Type

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations
@[protected, instance]
noncomputable def ennreal.has_sub  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem ennreal.some_eq_coe (a : ℝ≥0) :
@[protected]

to_nnreal x returns x if it is real, otherwise 0.

Equations
@[protected]

to_real x returns x if it is real, 0 otherwise.

Equations
@[protected]
noncomputable def ennreal.of_real (r : ) :

of_real x returns x if it is nonnegative, 0 otherwise.

Equations
@[simp, norm_cast]
@[simp]
theorem ennreal.coe_to_nnreal {a : ℝ≥0∞} :
a (a.to_nnreal) = a
@[simp]
@[simp]
theorem ennreal.to_real_of_real {r : } (h : 0 r) :
theorem ennreal.of_real_eq_coe_nnreal {x : } (h : 0 x) :
@[simp, norm_cast]
theorem ennreal.coe_zero  :
0 = 0
@[simp, norm_cast]
theorem ennreal.coe_one  :
1 = 1
@[simp]
@[simp]
@[simp]
@[simp]
theorem ennreal.one_to_real  :
@[simp]
@[simp]
@[simp]
@[simp]
theorem ennreal.zero_to_real  :
@[simp]
@[simp]
theorem ennreal.forall_ennreal {p : ℝ≥0∞ → Prop} :
(∀ (a : ℝ≥0∞), p a) (∀ (r : ℝ≥0), p r) p
theorem ennreal.forall_ne_top {p : ℝ≥0∞ → Prop} :
(∀ (a : ℝ≥0∞), a p a) ∀ (r : ℝ≥0), p r
theorem ennreal.exists_ne_top {p : ℝ≥0∞ → Prop} :
(∃ (a : ℝ≥0∞) (H : a ), p a) ∃ (r : ℝ≥0), p r
@[simp]
theorem ennreal.coe_ne_top {r : ℝ≥0} :
@[simp]
theorem ennreal.top_ne_coe {r : ℝ≥0} :
@[simp]
@[simp]
theorem ennreal.zero_ne_top  :
@[simp]
theorem ennreal.top_ne_zero  :
@[simp]
theorem ennreal.one_ne_top  :
@[simp]
theorem ennreal.top_ne_one  :
@[simp, norm_cast]
theorem ennreal.coe_eq_coe {r q : ℝ≥0} :
r = q r = q
@[simp, norm_cast]
theorem ennreal.coe_le_coe {r q : ℝ≥0} :
r q r q
@[simp, norm_cast]
theorem ennreal.coe_lt_coe {r q : ℝ≥0} :
r < q r < q
@[simp, norm_cast]
theorem ennreal.coe_eq_zero {r : ℝ≥0} :
r = 0 r = 0
@[simp, norm_cast]
theorem ennreal.zero_eq_coe {r : ℝ≥0} :
0 = r 0 = r
@[simp, norm_cast]
theorem ennreal.coe_eq_one {r : ℝ≥0} :
r = 1 r = 1
@[simp, norm_cast]
theorem ennreal.one_eq_coe {r : ℝ≥0} :
1 = r 1 = r
@[simp, norm_cast]
theorem ennreal.coe_nonneg {r : ℝ≥0} :
0 r 0 r
@[simp, norm_cast]
theorem ennreal.coe_pos {r : ℝ≥0} :
0 < r 0 < r
theorem ennreal.coe_ne_zero {r : ℝ≥0} :
r 0 r 0
@[simp, norm_cast]
theorem ennreal.coe_add {r p : ℝ≥0} :
(r + p) = r + p
@[simp, norm_cast]
theorem ennreal.coe_mul {r p : ℝ≥0} :
r * p = (r) * p
@[simp, norm_cast]
theorem ennreal.coe_bit0 {r : ℝ≥0} :
@[simp, norm_cast]
theorem ennreal.coe_bit1 {r : ℝ≥0} :
theorem ennreal.coe_two  :
2 = 2
@[protected]
theorem ennreal.zero_lt_one  :
0 < 1
@[simp]
theorem ennreal.one_lt_two  :
1 < 2
@[simp]
theorem ennreal.zero_lt_two  :
0 < 2
theorem ennreal.two_ne_zero  :
2 0
@[protected, instance]

(1 : ℝ≥0∞) ≤ 1, recorded as a fact for use with Lp spaces.

@[protected, instance]

(1 : ℝ≥0∞) ≤ 2, recorded as a fact for use with Lp spaces.

@[protected, instance]

(1 : ℝ≥0∞) ≤ ∞, recorded as a fact for use with Lp spaces.

The set of numbers in ℝ≥0∞ that are not equal to is equivalent to ℝ≥0.

Equations
theorem ennreal.cinfi_ne_top {α : Type u_1} [has_Inf α] (f : ℝ≥0∞ → α) :
(⨅ (x : {x // x }), f x) = ⨅ (x : ℝ≥0), f x
theorem ennreal.infi_ne_top {α : Type u_1} [complete_lattice α] (f : ℝ≥0∞ → α) :
(⨅ (x : ℝ≥0∞) (H : x ), f x) = ⨅ (x : ℝ≥0), f x
theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ℝ≥0∞ → α) :
(⨆ (x : {x // x }), f x) = ⨆ (x : ℝ≥0), f x
theorem ennreal.supr_ne_top {α : Type u_1} [complete_lattice α] (f : ℝ≥0∞ → α) :
(⨆ (x : ℝ≥0∞) (H : x ), f x) = ⨆ (x : ℝ≥0), f x
theorem ennreal.infi_ennreal {α : Type u_1} [complete_lattice α] {f : ℝ≥0∞ → α} :
(⨅ (n : ℝ≥0∞), f n) = (⨅ (n : ℝ≥0), f n) f
theorem ennreal.supr_ennreal {α : Type u_1} [complete_lattice α] {f : ℝ≥0∞ → α} :
(⨆ (n : ℝ≥0∞), f n) = (⨆ (n : ℝ≥0), f n) f
@[simp]
theorem ennreal.add_top {a : ℝ≥0∞} :
@[simp]
theorem ennreal.top_add {a : ℝ≥0∞} :

Coercion ℝ≥0 → ℝ≥0∞ as a ring_hom.

Equations
@[protected, instance]
noncomputable def ennreal.mul_action {M : Type u_1} [mul_action ℝ≥0∞ M] :

A mul_action over ℝ≥0∞ restricts to a mul_action over ℝ≥0.

Equations
theorem ennreal.smul_def {M : Type u_1} [mul_action ℝ≥0∞ M] (c : ℝ≥0) (x : M) :
c x = c x
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def ennreal.module {M : Type u_1} [add_comm_monoid M] [module ℝ≥0∞ M] :

A module over ℝ≥0∞ restricts to a module over ℝ≥0.

Equations
@[protected, instance]
noncomputable def ennreal.algebra {A : Type u_1} [semiring A] [algebra ℝ≥0∞ A] :

An algebra over ℝ≥0∞ restricts to an algebra over ℝ≥0.

Equations
@[simp, norm_cast]
theorem ennreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a
@[simp, norm_cast]
theorem ennreal.coe_pow {r : ℝ≥0} (n : ) :
(r ^ n) = r ^ n
@[simp]
theorem ennreal.add_eq_top {a b : ℝ≥0∞} :
a + b = a = b =
@[simp]
theorem ennreal.add_lt_top {a b : ℝ≥0∞} :
a + b < a < b <
theorem ennreal.to_nnreal_add {r₁ r₂ : ℝ≥0∞} (h₁ : r₁ ) (h₂ : r₂ ) :
(r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal
theorem ennreal.add_ne_top {a b : ℝ≥0∞} :
theorem ennreal.mul_top {a : ℝ≥0∞} :
a * = ite (a = 0) 0
theorem ennreal.top_mul {a : ℝ≥0∞} :
* a = ite (a = 0) 0
@[simp]
theorem ennreal.top_pow {n : } (h : 0 < n) :
theorem ennreal.mul_eq_top {a b : ℝ≥0∞} :
a * b = a 0 b = a = b 0
theorem ennreal.mul_lt_top {a b : ℝ≥0∞} :
a b a * b <
theorem ennreal.mul_ne_top {a b : ℝ≥0∞} :
a b a * b
theorem ennreal.lt_top_of_mul_ne_top_left {a b : ℝ≥0∞} (h : a * b ) (hb : b 0) :
a <
theorem ennreal.lt_top_of_mul_ne_top_right {a b : ℝ≥0∞} (h : a * b ) (ha : a 0) :
b <
theorem ennreal.mul_lt_top_iff {a b : ℝ≥0∞} :
a * b < a < b < a = 0 b = 0
theorem ennreal.mul_pos_iff {a b : ℝ≥0∞} :
0 < a * b 0 < a 0 < b
theorem ennreal.mul_pos {a b : ℝ≥0∞} (ha : a 0) (hb : b 0) :
0 < a * b
@[simp]
theorem ennreal.pow_eq_top_iff {a : ℝ≥0∞} {n : } :
a ^ n = a = n 0
theorem ennreal.pow_eq_top {a : ℝ≥0∞} (n : ) (h : a ^ n = ) :
a =
theorem ennreal.pow_ne_top {a : ℝ≥0∞} (h : a ) {n : } :
a ^ n
theorem ennreal.pow_lt_top {a : ℝ≥0∞} :
a < ∀ (n : ), a ^ n <
@[simp, norm_cast]
theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
∑ (a : α) in s, f a = ∑ (a : α) in s, (f a)
@[simp, norm_cast]
theorem ennreal.coe_finset_prod {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
∏ (a : α) in s, f a = ∏ (a : α) in s, (f a)
@[simp]
theorem ennreal.bot_eq_zero  :
= 0
@[simp]
theorem ennreal.coe_lt_top {r : ℝ≥0} :
@[simp]
@[simp, norm_cast]
theorem ennreal.one_le_coe_iff {r : ℝ≥0} :
1 r 1 r
@[simp, norm_cast]
theorem ennreal.coe_le_one_iff {r : ℝ≥0} :
r 1 r 1
@[simp, norm_cast]
theorem ennreal.coe_lt_one_iff {p : ℝ≥0} :
p < 1 p < 1
@[simp, norm_cast]
theorem ennreal.one_lt_coe_iff {p : ℝ≥0} :
1 < p 1 < p
@[simp, norm_cast]
theorem ennreal.coe_nat (n : ) :
@[simp]
theorem ennreal.nat_ne_top (n : ) :
@[simp]
theorem ennreal.top_ne_nat (n : ) :
@[simp]
theorem ennreal.one_lt_top  :
1 <
@[simp, norm_cast]
@[simp, norm_cast]
theorem ennreal.to_real_nat (n : ) :
theorem ennreal.le_coe_iff {a : ℝ≥0∞} {r : ℝ≥0} :
a r ∃ (p : ℝ≥0), a = p p r
theorem ennreal.coe_le_iff {a : ℝ≥0∞} {r : ℝ≥0} :
r a ∀ (p : ℝ≥0), a = pr p
theorem ennreal.lt_iff_exists_coe {a b : ℝ≥0∞} :
a < b ∃ (p : ℝ≥0), a = p p < b
@[simp, norm_cast]
theorem ennreal.coe_finset_sup {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
(s.sup f) = s.sup (λ (x : α), (f x))
theorem ennreal.pow_le_pow {a : ℝ≥0∞} {n m : } (ha : 1 a) (h : n m) :
a ^ n a ^ m
theorem ennreal.one_le_pow_of_one_le {a : ℝ≥0∞} (ha : 1 a) (n : ) :
1 a ^ n
@[simp]
theorem ennreal.max_eq_zero_iff {a b : ℝ≥0∞} :
max a b = 0 a = 0 b = 0
@[simp]
theorem ennreal.max_zero_left {a : ℝ≥0∞} :
max 0 a = a
@[simp]
theorem ennreal.max_zero_right {a : ℝ≥0∞} :
max a 0 = a
@[simp]
theorem ennreal.sup_eq_max {a b : ℝ≥0∞} :
a b = max a b
@[protected]
theorem ennreal.pow_pos {a : ℝ≥0∞} :
0 < a∀ (n : ), 0 < a ^ n
@[protected]
theorem ennreal.pow_ne_zero {a : ℝ≥0∞} :
a 0∀ (n : ), a ^ n 0
@[simp]
theorem ennreal.not_lt_zero {a : ℝ≥0∞} :
¬a < 0
@[protected]
theorem ennreal.le_of_add_le_add_left {a b c : ℝ≥0∞} :
a a + b a + cb c
@[protected]
theorem ennreal.le_of_add_le_add_right {a b c : ℝ≥0∞} :
a b + a c + ab c
@[protected]
theorem ennreal.add_lt_add_left {a b c : ℝ≥0∞} :
a b < ca + b < a + c
@[protected]
theorem ennreal.add_lt_add_right {a b c : ℝ≥0∞} :
a b < cb + a < c + a
@[protected]
theorem ennreal.add_le_add_iff_left {a b c : ℝ≥0∞} :
a (a + b a + c b c)
@[protected]
theorem ennreal.add_le_add_iff_right {a b c : ℝ≥0∞} :
a (b + a c + a b c)
@[protected]
theorem ennreal.add_lt_add_iff_left {a b c : ℝ≥0∞} :
a (a + b < a + c b < c)
@[protected]
theorem ennreal.add_lt_add_iff_right {a b c : ℝ≥0∞} :
a (b + a < c + a b < c)
@[protected]
theorem ennreal.add_lt_add_of_le_of_lt {a b c d : ℝ≥0∞} :
a a bc < da + c < b + d
@[protected]
theorem ennreal.add_lt_add_of_lt_of_le {a b c d : ℝ≥0∞} :
c a < bc da + c < b + d
theorem ennreal.lt_add_right {a b : ℝ≥0∞} (ha : a ) (hb : b 0) :
a < a + b
theorem ennreal.le_of_forall_pos_le_add {a b : ℝ≥0∞} :
(∀ (ε : ℝ≥0), 0 < εb < a b + ε)a b
theorem ennreal.lt_iff_exists_rat_btwn {a b : ℝ≥0∞} :
a < b ∃ (q : ), 0 q a < (q.to_nnreal) (q.to_nnreal) < b
theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ℝ≥0∞} :
a < b ∃ (r : ℝ≥0), a < r r < b
theorem ennreal.lt_iff_exists_add_pos_lt {a b : ℝ≥0∞} :
a < b ∃ (r : ℝ≥0), 0 < r a + r < b
theorem ennreal.coe_nat_lt_coe {r : ℝ≥0} {n : } :
n < r n < r
theorem ennreal.coe_lt_coe_nat {r : ℝ≥0} {n : } :
r < n r < n
@[simp, norm_cast]
theorem ennreal.coe_nat_lt_coe_nat {m n : } :
m < n m < n
@[simp, norm_cast]
theorem ennreal.coe_nat_le_coe_nat {m n : } :
m n m n
@[protected, instance]
@[protected]
theorem ennreal.exists_nat_gt {r : ℝ≥0∞} (h : r ) :
∃ (n : ), r < n
theorem ennreal.add_lt_add {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) :
a + b < c + d
@[norm_cast]
theorem ennreal.coe_min {r p : ℝ≥0} :
(min r p) = min r p
@[norm_cast]
theorem ennreal.coe_max {r p : ℝ≥0} :
(max r p) = max r p
theorem ennreal.le_of_top_imp_top_of_to_nnreal_le {a b : ℝ≥0∞} (h : a = b = ) (h_nnreal : a b a.to_nnreal b.to_nnreal) :
a b
theorem ennreal.coe_Sup {s : set ℝ≥0} :
bdd_above s((Sup s) = ⨆ (a : ℝ≥0) (H : a s), a)
theorem ennreal.coe_Inf {s : set ℝ≥0} :
s.nonempty((Inf s) = ⨅ (a : ℝ≥0) (H : a s), a)
theorem ennreal.mul_le_mul {a b c d : ℝ≥0∞} :
a bc da * c b * d
theorem ennreal.mul_lt_mul {a b c d : ℝ≥0∞} (ac : a < c) (bd : b < d) :
a * b < c * d
theorem ennreal.mul_right_mono {a : ℝ≥0∞} :
monotone (λ (x : ℝ≥0∞), x * a)
theorem ennreal.pow_strict_mono {n : } (hn : n 0) :
strict_mono (λ (x : ℝ≥0∞), x ^ n)
theorem ennreal.max_mul {a b c : ℝ≥0∞} :
(max a b) * c = max (a * c) (b * c)
theorem ennreal.mul_max {a b c : ℝ≥0∞} :
a * max b c = max (a * b) (a * c)
theorem ennreal.mul_eq_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b = a * c b = c)
theorem ennreal.mul_eq_mul_right {a b c : ℝ≥0∞} :
c 0c (a * c = b * c a = b)
theorem ennreal.mul_le_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b a * c b c)
theorem ennreal.mul_le_mul_right {a b c : ℝ≥0∞} :
c 0c (a * c b * c a b)
theorem ennreal.mul_lt_mul_left {a b c : ℝ≥0∞} :
a 0a (a * b < a * c b < c)
theorem ennreal.mul_lt_mul_right {a b c : ℝ≥0∞} :
c 0c (a * c < b * c a < b)

An element a is add_le_cancellable if a + b ≤ a + c implies b ≤ c for all b and c. This is true in ℝ≥0∞ for all elements except .

This lemma has an abbreviated name because it is used frequently.

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.cancel_of_lt' {a b : ℝ≥0∞} (h : a < b) :

This lemma has an abbreviated name because it is used frequently.

This lemma has an abbreviated name because it is used frequently.

theorem ennreal.add_right_inj {a b c : ℝ≥0∞} (h : a ) :
a + b = a + c b = c
theorem ennreal.add_left_inj {a b c : ℝ≥0∞} (h : a ) :
b + a = c + a b = c
theorem ennreal.sub_eq_Inf {a b : ℝ≥0∞} :
a - b = Inf {d : ℝ≥0∞ | a d + b}
theorem ennreal.coe_sub {r p : ℝ≥0} :
(r - p) = r - p

This is a special case of with_top.coe_sub in the ennreal namespace

theorem ennreal.top_sub_coe {r : ℝ≥0} :

This is a special case of with_top.top_sub_coe in the ennreal namespace

theorem ennreal.sub_top {a : ℝ≥0∞} :
a - = 0

This is a special case of with_top.sub_top in the ennreal namespace

theorem ennreal.sub_eq_top_iff {a b : ℝ≥0∞} :
a - b = a = b
theorem ennreal.sub_ne_top {a b : ℝ≥0∞} (ha : a ) :
a - b
@[protected]
theorem ennreal.sub_lt_of_lt_add {a b c : ℝ≥0∞} (hac : c a) (h : a < b + c) :
a - c < b
@[simp]
theorem ennreal.add_sub_self {a b : ℝ≥0∞} (hb : b ) :
a + b - b = a
@[simp]
theorem ennreal.add_sub_self' {a b : ℝ≥0∞} (ha : a ) :
a + b - a = b
theorem ennreal.sub_eq_of_add_eq {a b c : ℝ≥0∞} (hb : b ) (hc : a + b = c) :
c - b = a
@[protected]
theorem ennreal.lt_add_of_sub_lt {a b c : ℝ≥0∞} (ht : a b ) (h : a - b < c) :
a < c + b
@[protected]
theorem ennreal.sub_lt_iff_lt_add {a b c : ℝ≥0∞} (hb : b ) (hab : b a) :
a - b < c a < c + b
@[protected]
theorem ennreal.sub_lt_self {a b : ℝ≥0∞} (hat : a ) (ha0 : a 0) (hb : b 0) :
a - b < a
theorem ennreal.sub_lt_of_sub_lt {a b c : ℝ≥0∞} (h₂ : c a) (h₃ : a b ) (h₁ : a - b < c) :
a - c < b
theorem ennreal.sub_sub_cancel {a b : ℝ≥0∞} (h : a ) (h2 : b a) :
a - (a - b) = b
theorem ennreal.sub_right_inj {a b c : ℝ≥0∞} (ha : a ) (hb : b a) (hc : c a) :
a - b = a - c b = c
theorem ennreal.sub_mul {a b c : ℝ≥0∞} (h : 0 < bb < ac ) :
(a - b) * c = a * c - b * c
theorem ennreal.mul_sub {a b c : ℝ≥0∞} (h : 0 < cc < ba ) :
a * (b - c) = a * b - a * c
theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∀ (a : α), a sf a ) :
∏ (a : α) in s, f a <

A product of finite numbers is still finite

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∀ (a : α), a sf a ) :
∑ (a : α) in s, f a <

A sum of finite numbers is still finite

theorem ennreal.sum_lt_top_iff {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} :
∑ (a : α) in s, f a < ∀ (a : α), a sf a <

A sum of finite numbers is still finite

theorem ennreal.sum_eq_top_iff {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} :
∑ (x : α) in s, f x = ∃ (a : α) (H : a s), f a =

A sum of numbers is infinite iff one of them is infinite

theorem ennreal.lt_top_of_sum_ne_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∑ (x : α) in s, f x ) {a : α} (ha : a s) :
f a <
theorem ennreal.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (hf : ∀ (a : α), a sf a ) :
(∑ (a : α) in s, f a).to_nnreal = ∑ (a : α) in s, (f a).to_nnreal

seeing ℝ≥0∞ as ℝ≥0 does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ennreal.to_real_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (hf : ∀ (a : α), a sf a ) :
(∑ (a : α) in s, f a).to_real = ∑ (a : α) in s, (f a).to_real

seeing ℝ≥0∞ as real does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ennreal.of_real_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (i : α), i s0 f i) :
ennreal.of_real (∑ (i : α) in s, f i) = ∑ (i : α) in s, ennreal.of_real (f i)
theorem ennreal.sum_lt_sum_of_nonempty {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α → ℝ≥0∞} (Hlt : ∀ (i : α), i sf i < g i) :
∑ (i : α) in s, f i < ∑ (i : α) in s, g i
theorem ennreal.exists_le_of_sum_le {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α → ℝ≥0∞} (Hle : ∑ (i : α) in s, f i ∑ (i : α) in s, g i) :
∃ (i : α) (H : i s), f i g i
@[protected]
theorem ennreal.Ico_eq_Iio {y : ℝ≥0∞} :
theorem ennreal.mem_Iio_self_add {x ε : ℝ≥0∞} :
x ε 0x set.Iio (x + ε)
theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ℝ≥0∞} :
x x 0ε₁ 0ε₂ 0x set.Ioo (x - ε₁) (x + ε₂)
@[simp]
theorem ennreal.bit0_inj {a b : ℝ≥0∞} :
bit0 a = bit0 b a = b
@[simp]
theorem ennreal.bit0_eq_zero_iff {a : ℝ≥0∞} :
bit0 a = 0 a = 0
@[simp]
@[simp]
theorem ennreal.bit1_inj {a b : ℝ≥0∞} :
bit1 a = bit1 b a = b
@[simp]
theorem ennreal.bit1_ne_zero {a : ℝ≥0∞} :
bit1 a 0
@[simp]
theorem ennreal.bit1_eq_one_iff {a : ℝ≥0∞} :
bit1 a = 1 a = 0
@[simp]
@[protected, instance]
noncomputable def ennreal.has_inv  :
Equations
@[protected, instance]
Equations
@[simp]
theorem ennreal.inv_zero  :
@[simp]
theorem ennreal.inv_top  :
@[simp, norm_cast]
theorem ennreal.coe_inv {r : ℝ≥0} (hr : r 0) :
@[norm_cast]
@[simp, norm_cast]
theorem ennreal.coe_div {r p : ℝ≥0} (hr : r 0) :
(p / r) = p / r
theorem ennreal.div_zero {a : ℝ≥0∞} (h : a 0) :
a / 0 =
@[simp]
theorem ennreal.inv_one  :
1⁻¹ = 1
@[simp]
theorem ennreal.div_one {a : ℝ≥0∞} :
a / 1 = a
@[protected]
theorem ennreal.inv_pow {a : ℝ≥0∞} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
@[protected, instance]
Equations
@[simp]
theorem ennreal.inv_eq_top {a : ℝ≥0∞} :
a⁻¹ = a = 0
@[simp]
theorem ennreal.inv_lt_top {x : ℝ≥0∞} :
x⁻¹ < 0 < x
theorem ennreal.div_lt_top {x y : ℝ≥0∞} (h1 : x ) (h2 : y 0) :
x / y <
@[simp]
theorem ennreal.inv_eq_zero {a : ℝ≥0∞} :
a⁻¹ = 0 a =
theorem ennreal.mul_inv {a b : ℝ≥0∞} (ha : a 0 b ) (hb : a b 0) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
@[simp]
theorem ennreal.inv_pos {a : ℝ≥0∞} :
@[simp]
theorem ennreal.inv_lt_inv {a b : ℝ≥0∞} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem ennreal.inv_le_inv {a b : ℝ≥0∞} :
@[simp]
theorem ennreal.inv_le_one {a : ℝ≥0∞} :
a⁻¹ 1 1 a
theorem ennreal.one_le_inv {a : ℝ≥0∞} :
1 a⁻¹ a 1
@[simp]
theorem ennreal.inv_lt_one {a : ℝ≥0∞} :
a⁻¹ < 1 1 < a

The inverse map λ x, x⁻¹ is an order isomorphism between ℝ≥0∞ and its order_dual

Equations
theorem ennreal.pow_le_pow_of_le_one {a : ℝ≥0∞} {n m : } (ha : a 1) (h : n m) :
a ^ m a ^ n
@[simp]
theorem ennreal.div_top {a : ℝ≥0∞} :
a / = 0
@[simp]
theorem ennreal.top_div_coe {p : ℝ≥0} :
theorem ennreal.top_div_of_ne_top {a : ℝ≥0∞} (h : a ) :
theorem ennreal.top_div_of_lt_top {a : ℝ≥0∞} (h : a < ) :
theorem ennreal.top_div {a : ℝ≥0∞} :
/ a = ite (a = ) 0
@[simp]
theorem ennreal.zero_div {a : ℝ≥0∞} :
0 / a = 0
theorem ennreal.div_eq_top {a b : ℝ≥0∞} :
a / b = a 0 b = 0 a = b
theorem ennreal.le_div_iff_mul_le {a b c : ℝ≥0∞} (h0 : b 0 c 0) (ht : b c ) :
a c / b a * b c
theorem ennreal.div_le_iff_le_mul {a b c : ℝ≥0∞} (hb0 : b 0 c ) (hbt : b c 0) :
a / b c a c * b
theorem ennreal.lt_div_iff_mul_lt {a b c : ℝ≥0∞} (hb0 : b 0 c ) (hbt : b c 0) :
c < a / b c * b < a
theorem ennreal.div_le_of_le_mul {a b c : ℝ≥0∞} (h : a b * c) :
a / c b
theorem ennreal.div_le_of_le_mul' {a b c : ℝ≥0∞} (h : a b * c) :
a / b c
theorem ennreal.mul_le_of_le_div {a b c : ℝ≥0∞} (h : a b / c) :
a * c b
theorem ennreal.mul_le_of_le_div' {a b c : ℝ≥0∞} (h : a b / c) :
c * a b
@[protected]
theorem ennreal.div_lt_iff {a b c : ℝ≥0∞} (h0 : b 0 c 0) (ht : b c ) :
c / b < a c < a * b
theorem ennreal.mul_lt_of_lt_div {a b c : ℝ≥0∞} (h : a < b / c) :
a * c < b
theorem ennreal.mul_lt_of_lt_div' {a b c : ℝ≥0∞} (h : a < b / c) :
c * a < b
theorem ennreal.inv_le_iff_le_mul {a b : ℝ≥0∞} :
(b = a 0)(a = b 0)(a⁻¹ b 1 a * b)
@[simp]
theorem ennreal.le_inv_iff_mul_le {a b : ℝ≥0∞} :
a b⁻¹ a * b 1
theorem ennreal.mul_inv_cancel {a : ℝ≥0∞} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
theorem ennreal.inv_mul_cancel {a : ℝ≥0∞} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
theorem ennreal.eq_inv_of_mul_eq_one {a b : ℝ≥0∞} (h : a * b = 1) :
a = b⁻¹
theorem ennreal.mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r 0) (hr₁ : r ) :
r * a b a r⁻¹ * b
theorem ennreal.le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ (r : ℝ≥0), r < xr y) :
x y
theorem ennreal.le_of_forall_pos_nnreal_lt {x y : ℝ≥0∞} (h : ∀ (r : ℝ≥0), 0 < rr < xr y) :
x y
theorem ennreal.eq_top_of_forall_nnreal_le {x : ℝ≥0∞} (h : ∀ (r : ℝ≥0), r x) :
x =
theorem ennreal.add_div {a b c : ℝ≥0∞} :
(a + b) / c = a / c + b / c
theorem ennreal.div_add_div_same {a b c : ℝ≥0∞} :
a / c + b / c = (a + b) / c
theorem ennreal.div_self {a : ℝ≥0∞} (h0 : a 0) (hI : a ) :
a / a = 1
theorem ennreal.mul_div_cancel {a b : ℝ≥0∞} (h0 : a 0) (hI : a ) :
(b / a) * a = b
theorem ennreal.mul_div_cancel' {a b : ℝ≥0∞} (h0 : a 0) (hI : a ) :
a * (b / a) = b
theorem ennreal.mul_div_le {a b : ℝ≥0∞} :
a * (b / a) b
@[simp]
theorem ennreal.add_halves (a : ℝ≥0∞) :
a / 2 + a / 2 = a
@[simp]
theorem ennreal.add_thirds (a : ℝ≥0∞) :
a / 3 + a / 3 + a / 3 = a
@[simp]
theorem ennreal.div_zero_iff {a b : ℝ≥0∞} :
a / b = 0 a = 0 b =
@[simp]
theorem ennreal.div_pos_iff {a b : ℝ≥0∞} :
0 < a / b a 0 b
theorem ennreal.half_pos {a : ℝ≥0∞} (h : a 0) :
0 < a / 2
theorem ennreal.half_lt_self {a : ℝ≥0∞} (hz : a 0) (ht : a ) :
a / 2 < a
theorem ennreal.half_le_self {a : ℝ≥0∞} :
a / 2 a
theorem ennreal.sub_half {a : ℝ≥0∞} (h : a ) :
a - a / 2 = a / 2
@[simp]
theorem ennreal.exists_inv_nat_lt {a : ℝ≥0∞} (h : a 0) :
∃ (n : ), (n)⁻¹ < a
theorem ennreal.exists_nat_pos_mul_gt {a b : ℝ≥0∞} (ha : a 0) (hb : b ) :
∃ (n : ) (H : n > 0), b < (n) * a
theorem ennreal.exists_nat_mul_gt {a b : ℝ≥0∞} (ha : a 0) (hb : b ) :
∃ (n : ), b < (n) * a
theorem ennreal.exists_nat_pos_inv_mul_lt {a b : ℝ≥0∞} (ha : a ) (hb : b 0) :
∃ (n : ) (H : n > 0), (n)⁻¹ * a < b
theorem ennreal.exists_nnreal_pos_mul_lt {a b : ℝ≥0∞} (ha : a ) (hb : b 0) :
∃ (n : ℝ≥0) (H : n > 0), (n) * a < b
theorem ennreal.exists_inv_two_pow_lt {a : ℝ≥0∞} (ha : a 0) :
∃ (n : ), 2⁻¹ ^ n < a
@[simp, norm_cast]
theorem ennreal.coe_zpow {r : ℝ≥0} (hr : r 0) (n : ) :
(r ^ n) = r ^ n
theorem ennreal.zpow_pos {a : ℝ≥0∞} (ha : a 0) (h'a : a ) (n : ) :
0 < a ^ n
theorem ennreal.zpow_lt_top {a : ℝ≥0∞} (ha : a 0) (h'a : a ) (n : ) :
a ^ n <
theorem ennreal.exists_mem_Ico_zpow {x y : ℝ≥0∞} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
∃ (n : ), x set.Ico (y ^ n) (y ^ (n + 1))
theorem ennreal.exists_mem_Ioc_zpow {x y : ℝ≥0∞} (hx : x 0) (h'x : x ) (hy : 1 < y) (h'y : y ) :
∃ (n : ), x set.Ioc (y ^ n) (y ^ (n + 1))
theorem ennreal.Ioo_zero_top_eq_Union_Ico_zpow {y : ℝ≥0∞} (hy : 1 < y) (h'y : y ) :
set.Ioo 0 = ⋃ (n : ), set.Ico (y ^ n) (y ^ (n + 1))
theorem ennreal.zpow_le_of_le {x : ℝ≥0∞} (hx : 1 x) {a b : } (h : a b) :
x ^ a x ^ b
theorem ennreal.monotone_zpow {x : ℝ≥0∞} (hx : 1 x) :
theorem ennreal.zpow_add {x : ℝ≥0∞} (hx : x 0) (h'x : x ) (m n : ) :
x ^ (m + n) = (x ^ m) * x ^ n
theorem ennreal.to_real_add {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_sub_of_le {a b : ℝ≥0∞} (h : b a) (ha : a ) :
theorem ennreal.le_to_real_sub {a b : ℝ≥0∞} (hb : b ) :
theorem ennreal.of_real_add {p q : } (hp : 0 p) (hq : 0 q) :
@[simp]
theorem ennreal.to_real_le_to_real {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_mono {a b : ℝ≥0∞} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_real_lt_to_real {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_strict_mono {a b : ℝ≥0∞} (hb : b ) (h : a < b) :
theorem ennreal.to_nnreal_mono {a b : ℝ≥0∞} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_nnreal_le_to_nnreal {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_nnreal_strict_mono {a b : ℝ≥0∞} (hb : b ) (h : a < b) :
@[simp]
theorem ennreal.to_nnreal_lt_to_nnreal {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_max {a b : ℝ≥0∞} (hr : a ) (hp : b ) :
theorem ennreal.to_nnreal_pos {a : ℝ≥0∞} (ha₀ : a 0) (ha_top : a ) :
theorem ennreal.to_real_pos {a : ℝ≥0∞} (ha₀ : a 0) (ha_top : a ) :
@[simp]
@[simp]
theorem ennreal.of_real_lt_of_real_iff {p q : } (h : 0 < q) :
@[simp]
theorem ennreal.of_real_pos {p : } :
@[simp]
theorem ennreal.of_real_eq_zero {p : } :
@[simp]
theorem ennreal.zero_eq_of_real {p : } :
theorem ennreal.of_real_lt_iff_lt_to_real {a : } {b : ℝ≥0∞} (ha : 0 a) (hb : b ) :
theorem ennreal.le_of_real_iff_to_real_le {a : ℝ≥0∞} {b : } (ha : a ) (hb : 0 b) :
theorem ennreal.to_real_le_of_le_of_real {a : ℝ≥0∞} {b : } (hb : 0 b) (h : a ennreal.of_real b) :
theorem ennreal.of_real_mul {p q : } (hp : 0 p) :
theorem ennreal.of_real_pow {p : } (hp : 0 p) (n : ) :
theorem ennreal.to_real_of_real_mul (c : ) (a : ℝ≥0∞) (h : 0 c) :
@[simp]
@[simp]
@[simp]
theorem ennreal.to_real_mul_top (a : ℝ≥0∞) :
(a * ).to_real = 0
@[simp]
theorem ennreal.to_real_top_mul (a : ℝ≥0∞) :
( * a).to_real = 0
theorem ennreal.to_real_eq_to_real {a b : ℝ≥0∞} (ha : a ) (hb : b ) :
theorem ennreal.to_real_smul (r : ℝ≥0) (s : ℝ≥0∞) :
(r s).to_real = r s.to_real
@[protected]
theorem ennreal.trichotomy (p : ℝ≥0∞) :
p = 0 p = 0 < p.to_real
@[protected]
theorem ennreal.trichotomy₂ {p q : ℝ≥0∞} (hpq : p q) :
p = 0 q = 0 p = 0 q = p = 0 0 < q.to_real p = q = 0 < p.to_real q = 0 < p.to_real 0 < q.to_real p.to_real q.to_real
@[protected]
theorem ennreal.dichotomy (p : ℝ≥0∞) [fact (1 p)] :

ennreal.to_nnreal as a monoid_hom.

Equations
theorem ennreal.to_nnreal_pow (a : ℝ≥0∞) (n : ) :
(a ^ n).to_nnreal = a.to_nnreal ^ n
theorem ennreal.to_nnreal_prod {ι : Type u_1} {s : finset ι} {f : ι → ℝ≥0∞} :
(∏ (i : ι) in s, f i).to_nnreal = ∏ (i : ι) in s, (f i).to_nnreal
theorem ennreal.to_real_mul {a b : ℝ≥0∞} :
(a * b).to_real = (a.to_real) * b.to_real
theorem ennreal.to_real_pow (a : ℝ≥0∞) (n : ) :
(a ^ n).to_real = a.to_real ^ n
theorem ennreal.to_real_prod {ι : Type u_1} {s : finset ι} {f : ι → ℝ≥0∞} :
(∏ (i : ι) in s, f i).to_real = ∏ (i : ι) in s, (f i).to_real
theorem ennreal.of_real_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → } (hf : ∀ (i : α), i s0 f i) :
ennreal.of_real (∏ (i : α) in s, f i) = ∏ (i : α) in s, ennreal.of_real (f i)
@[simp]
theorem ennreal.to_nnreal_bit1 {x : ℝ≥0∞} (hx_top : x ) :
@[simp]
@[simp]
theorem ennreal.to_real_bit1 {x : ℝ≥0∞} (hx_top : x ) :
@[simp]
theorem ennreal.of_real_bit0 {r : } (hr : 0 r) :
@[simp]
theorem ennreal.of_real_bit1 {r : } (hr : 0 r) :
theorem ennreal.infi_add {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
infi f + a = ⨅ (i : ι), f i + a
theorem ennreal.supr_sub {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a
theorem ennreal.sub_infi {a : ℝ≥0∞} {ι : Sort u_3} {f : ι → ℝ≥0∞} :
(a - ⨅ (i : ι), f i) = ⨆ (i : ι), a - f i
theorem ennreal.Inf_add {a : ℝ≥0∞} {s : set ℝ≥0∞} :
Inf s + a = ⨅ (b : ℝ≥0∞) (H : b s), b + a
theorem ennreal.add_infi {ι : Sort u_3} {f : ι → ℝ≥0∞} {a : ℝ≥0∞} :
a + infi f = ⨅ (b : ι), a + f b
theorem ennreal.infi_add_infi {ι : Sort u_3} {f g : ι → ℝ≥0∞} (h : ∀ (i j : ι), ∃ (k : ι), f k + g k f i + g j) :
infi f + infi g = ⨅ (a : ι), f a + g a
theorem ennreal.infi_sum {α : Type u_1} {ι : Sort u_3} {f : ι → α → ℝ≥0∞} {s : finset α} [nonempty ι] (h : ∀ (t : finset α) (i j : ι), ∃ (k : ι), ∀ (a : α), a tf k a f i a f k a f j a) :
(⨅ (i : ι), ∑ (a : α) in s, f i a) = ∑ (a : α) in s, ⨅ (i : ι), f i a
theorem ennreal.infi_mul_of_ne {ι : Sort u_1} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x 0) (h : x ) :
(infi f) * x = ⨅ (i : ι), (f i) * x

If x ≠ 0 and x ≠ ∞, then right multiplication by x maps infimum to infimum. See also ennreal.infi_mul that assumes [nonempty ι] but does not require x ≠ 0.

theorem ennreal.infi_mul {ι : Sort u_1} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ) :
(infi f) * x = ⨅ (i : ι), (f i) * x

If x ≠ ∞, then right multiplication by x maps infimum over a nonempty type to infimum. See also ennreal.infi_mul_of_ne that assumes x ≠ 0 but does not require [nonempty ι].

theorem ennreal.mul_infi {ι : Sort u_1} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ) :
x * infi f = ⨅ (i : ι), x * f i

If x ≠ ∞, then left multiplication by x maps infimum over a nonempty type to infimum. See also ennreal.mul_infi_of_ne that assumes x ≠ 0 but does not require [nonempty ι].

theorem ennreal.mul_infi_of_ne {ι : Sort u_1} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x 0) (h : x ) :
x * infi f = ⨅ (i : ι), x * f i

If x ≠ 0 and x ≠ ∞, then left multiplication by x maps infimum to infimum. See also ennreal.mul_infi that assumes [nonempty ι] but does not require x ≠ 0.

supr_mul, mul_supr and variants are in topology.instances.ennreal.

@[simp]
theorem ennreal.supr_eq_zero {ι : Sort u_1} {f : ι → ℝ≥0∞} :
(⨆ (i : ι), f i) = 0 ∀ (i : ι), f i = 0
@[simp]
theorem ennreal.supr_zero_eq_zero {ι : Sort u_1} :
(⨆ (i : ι), 0) = 0
theorem ennreal.sup_eq_zero {a b : ℝ≥0∞} :
a b = 0 a = 0 b = 0
theorem ennreal.supr_coe_nat  :
(⨆ (n : ), n) =