mathlib3 documentation

data.real.ennreal

Extended non-negative reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def ennreal.has_sub  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[protected]

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

Equations
@[protected]
def ennreal.to_real (a : ennreal) :

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]
@[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]
theorem ennreal.to_real_nonneg {a : ennreal} :
@[simp]
@[simp]
@[simp]
theorem ennreal.one_to_real  :
@[simp]
@[simp]
theorem ennreal.coe_to_real (r : nnreal) :
@[simp]
@[simp]
theorem ennreal.zero_to_real  :
@[simp]
@[simp]
theorem ennreal.forall_ennreal {p : ennreal Prop} :
( (a : ennreal), p a) ( (r : nnreal), p r) p
theorem ennreal.forall_ne_top {p : ennreal Prop} :
( (a : ennreal), a p a) (r : nnreal), p r
theorem ennreal.exists_ne_top {p : ennreal Prop} :
( (a : ennreal) (H : a ), p a) (r : nnreal), p r
@[simp]
theorem ennreal.coe_ne_top {r : nnreal} :
@[simp]
theorem ennreal.top_ne_coe {r : nnreal} :
@[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 : nnreal} :
r = q r = q
@[simp, norm_cast]
theorem ennreal.coe_le_coe {r q : nnreal} :
r q r q
@[simp, norm_cast]
theorem ennreal.coe_lt_coe {r q : nnreal} :
r < q r < q
@[simp, norm_cast]
theorem ennreal.coe_eq_zero {r : nnreal} :
r = 0 r = 0
@[simp, norm_cast]
theorem ennreal.zero_eq_coe {r : nnreal} :
0 = r 0 = r
@[simp, norm_cast]
theorem ennreal.coe_eq_one {r : nnreal} :
r = 1 r = 1
@[simp, norm_cast]
theorem ennreal.one_eq_coe {r : nnreal} :
1 = r 1 = r
@[simp, norm_cast]
theorem ennreal.coe_pos {r : nnreal} :
0 < r 0 < r
theorem ennreal.coe_ne_zero {r : nnreal} :
r 0 r 0
@[simp, norm_cast]
theorem ennreal.coe_add {r p : nnreal} :
(r + p) = r + p
@[simp, norm_cast]
theorem ennreal.coe_mul {r p : nnreal} :
(r * p) = r * p
@[simp, norm_cast]
theorem ennreal.coe_bit0 {r : nnreal} :
@[simp, norm_cast]
theorem ennreal.coe_bit1 {r : nnreal} :
theorem ennreal.coe_two  :
2 = 2
theorem ennreal.to_real_eq_to_real_iff (x y : ennreal) :
x.to_real = y.to_real x = y x = 0 y = x = y = 0
theorem ennreal.to_nnreal_eq_to_nnreal_iff' {x y : ennreal} (hx : x ) (hy : y ) :
theorem ennreal.to_real_eq_to_real_iff' {x y : ennreal} (hx : x ) (hy : y ) :
@[simp]
theorem ennreal.one_lt_two  :
1 < 2
@[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 : ennreal α) :
( (x : {x // x }), f x) = (x : nnreal), f x
theorem ennreal.infi_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal α) :
( (x : ennreal) (H : x ), f x) = (x : nnreal), f x
theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ennreal α) :
( (x : {x // x }), f x) = (x : nnreal), f x
theorem ennreal.supr_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal α) :
( (x : ennreal) (H : x ), f x) = (x : nnreal), f x
theorem ennreal.infi_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal α} :
( (n : ennreal), f n) = ( (n : nnreal), f n) f
theorem ennreal.supr_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal α} :
( (n : ennreal), f n) = ( (n : nnreal), f n) f

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

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

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

Equations
theorem ennreal.smul_def {M : Type u_1} [mul_action ennreal M] (c : nnreal) (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 ennreal 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 ennreal 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 : α nnreal) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a
@[simp, norm_cast]
theorem ennreal.coe_pow {r : nnreal} (n : ) :
(r ^ n) = r ^ n
@[simp]
theorem ennreal.add_eq_top {a b : ennreal} :
a + b = a = b =
@[simp]
theorem ennreal.add_lt_top {a b : ennreal} :
a + b < a < b <
theorem ennreal.to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ ) (h₂ : r₂ ) :
(r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal
theorem ennreal.not_lt_top {x : ennreal} :
theorem ennreal.add_ne_top {a b : ennreal} :
theorem ennreal.mul_top {a : ennreal} :
a * = ite (a = 0) 0
theorem ennreal.top_mul {a : ennreal} :
* a = ite (a = 0) 0
@[simp]
theorem ennreal.top_pow {n : } (h : 0 < n) :
theorem ennreal.mul_eq_top {a b : ennreal} :
a * b = a 0 b = a = b 0
theorem ennreal.mul_lt_top {a b : ennreal} :
a b a * b <
theorem ennreal.mul_ne_top {a b : ennreal} :
theorem ennreal.lt_top_of_mul_ne_top_left {a b : ennreal} (h : a * b ) (hb : b 0) :
a <
theorem ennreal.lt_top_of_mul_ne_top_right {a b : ennreal} (h : a * b ) (ha : a 0) :
b <
theorem ennreal.mul_lt_top_iff {a b : ennreal} :
a * b < a < b < a = 0 b = 0
theorem ennreal.mul_pos_iff {a b : ennreal} :
0 < a * b 0 < a 0 < b
theorem ennreal.mul_pos {a b : ennreal} (ha : a 0) (hb : b 0) :
0 < a * b
@[simp]
theorem ennreal.pow_eq_top_iff {a : ennreal} {n : } :
a ^ n = a = n 0
theorem ennreal.pow_eq_top {a : ennreal} (n : ) (h : a ^ n = ) :
a =
theorem ennreal.pow_ne_top {a : ennreal} (h : a ) {n : } :
a ^ n
theorem ennreal.pow_lt_top {a : ennreal} :
a < (n : ), a ^ n <
@[simp, norm_cast]
theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), (f a))
@[simp, norm_cast]
theorem ennreal.coe_finset_prod {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), (f a))
@[simp]
theorem ennreal.bot_eq_zero  :
= 0
@[simp]
theorem ennreal.coe_lt_top {r : nnreal} :
@[simp]
@[simp, norm_cast]
theorem ennreal.one_le_coe_iff {r : nnreal} :
1 r 1 r
@[simp, norm_cast]
theorem ennreal.coe_le_one_iff {r : nnreal} :
r 1 r 1
@[simp, norm_cast]
theorem ennreal.coe_lt_one_iff {p : nnreal} :
p < 1 p < 1
@[simp, norm_cast]
theorem ennreal.one_lt_coe_iff {p : nnreal} :
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 : ennreal} {r : nnreal} :
a r (p : nnreal), a = p p r
theorem ennreal.coe_le_iff {a : ennreal} {r : nnreal} :
r a (p : nnreal), a = p r p
theorem ennreal.lt_iff_exists_coe {a b : ennreal} :
a < b (p : nnreal), a = p p < b
@[simp, norm_cast]
theorem ennreal.coe_finset_sup {α : Type u_1} {s : finset α} {f : α nnreal} :
(s.sup f) = s.sup (λ (x : α), (f x))
@[simp]
theorem ennreal.max_eq_zero_iff {a b : ennreal} :
linear_order.max a b = 0 a = 0 b = 0
@[simp]
@[simp]
@[simp]
theorem ennreal.sup_eq_max {a b : ennreal} :
@[protected]
theorem ennreal.pow_pos {a : ennreal} :
0 < a (n : ), 0 < a ^ n
@[protected]
theorem ennreal.pow_ne_zero {a : ennreal} :
a 0 (n : ), a ^ n 0
@[simp]
theorem ennreal.not_lt_zero {a : ennreal} :
¬a < 0
@[protected]
theorem ennreal.le_of_add_le_add_left {a b c : ennreal} :
a a + b a + c b c
@[protected]
theorem ennreal.le_of_add_le_add_right {a b c : ennreal} :
a b + a c + a b c
@[protected]
theorem ennreal.add_lt_add_left {a b c : ennreal} :
a b < c a + b < a + c
@[protected]
theorem ennreal.add_lt_add_right {a b c : ennreal} :
a b < c b + a < c + a
@[protected]
theorem ennreal.add_le_add_iff_left {a b c : ennreal} :
a (a + b a + c b c)
@[protected]
theorem ennreal.add_le_add_iff_right {a b c : ennreal} :
a (b + a c + a b c)
@[protected]
theorem ennreal.add_lt_add_iff_left {a b c : ennreal} :
a (a + b < a + c b < c)
@[protected]
theorem ennreal.add_lt_add_iff_right {a b c : ennreal} :
a (b + a < c + a b < c)
@[protected]
theorem ennreal.add_lt_add_of_le_of_lt {a b c d : ennreal} :
a a b c < d a + c < b + d
@[protected]
theorem ennreal.add_lt_add_of_lt_of_le {a b c d : ennreal} :
c a < b c d a + c < b + d
theorem ennreal.lt_add_right {a b : ennreal} (ha : a ) (hb : b 0) :
a < a + b
theorem ennreal.le_of_forall_pos_le_add {a b : ennreal} :
( (ε : nnreal), 0 < ε b < a b + ε) a b
theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ennreal} :
a < b (r : nnreal), a < r r < b
theorem ennreal.lt_iff_exists_add_pos_lt {a b : ennreal} :
a < b (r : nnreal), 0 < r a + r < b
@[simp, norm_cast]
theorem ennreal.coe_nat_lt_coe {r : nnreal} {n : } :
n < r n < r
@[simp, norm_cast]
theorem ennreal.coe_lt_coe_nat {r : nnreal} {n : } :
r < n r < n
@[protected]
theorem ennreal.exists_nat_gt {r : ennreal} (h : r ) :
(n : ), r < n
@[simp]
@[simp]
@[simp]
theorem ennreal.Union_Ioc_coe_nat {a : ennreal} :
( (n : ), set.Ioc a n) = set.Ioi a \ {}
@[simp]
theorem ennreal.Union_Ioo_coe_nat {a : ennreal} :
( (n : ), set.Ioo a n) = set.Ioi a \ {}
@[simp]
theorem ennreal.Union_Icc_coe_nat {a : ennreal} :
( (n : ), set.Icc a n) = set.Ici a \ {}
@[simp]
theorem ennreal.Union_Ico_coe_nat {a : ennreal} :
( (n : ), set.Ico a n) = set.Ici a \ {}
@[simp]
theorem ennreal.Inter_Ici_coe_nat  :
( (n : ), set.Ici n) = {}
@[simp]
theorem ennreal.Inter_Ioi_coe_nat  :
( (n : ), set.Ioi n) = {}
theorem ennreal.add_lt_add {a b c d : ennreal} (ac : a < c) (bd : b < d) :
a + b < c + d
@[norm_cast]
@[norm_cast]
theorem ennreal.le_of_top_imp_top_of_to_nnreal_le {a b : ennreal} (h : a = b = ) (h_nnreal : a b a.to_nnreal b.to_nnreal) :
a b
theorem ennreal.coe_Sup {s : set nnreal} :
bdd_above s ((has_Sup.Sup s) = (a : nnreal) (H : a s), a)
theorem ennreal.coe_Inf {s : set nnreal} :
s.nonempty ((has_Inf.Inf s) = (a : nnreal) (H : a s), a)
theorem ennreal.coe_supr {ι : Sort u_1} {f : ι nnreal} (hf : bdd_above (set.range f)) :
(supr f) = (a : ι), (f a)
@[norm_cast]
theorem ennreal.coe_infi {ι : Sort u_1} [nonempty ι] (f : ι nnreal) :
(infi f) = (a : ι), (f a)
theorem ennreal.mul_lt_mul {a b c d : ennreal} (ac : a < c) (bd : b < d) :
a * b < c * d
theorem ennreal.mul_right_mono {a : ennreal} :
monotone (λ (x : ennreal), x * a)
theorem ennreal.pow_strict_mono {n : } (hn : n 0) :
strict_mono (λ (x : ennreal), x ^ n)
theorem ennreal.max_mul {a b c : ennreal} :
theorem ennreal.mul_max {a b c : ennreal} :
theorem ennreal.mul_left_strictMono {a : ennreal} (h0 : a 0) (hinf : a ) :
theorem ennreal.mul_eq_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b = a * c b = c
theorem ennreal.mul_eq_mul_right {a b c : ennreal} :
c 0 c (a * c = b * c a = b)
theorem ennreal.mul_le_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b a * c b c
theorem ennreal.mul_le_mul_right {a b c : ennreal} :
c 0 c (a * c b * c a b)
theorem ennreal.mul_lt_mul_left {a b c : ennreal} (h₀ : a 0) (hinf : a ) :
a * b < a * c b < c
theorem ennreal.mul_lt_mul_right {a b c : ennreal} :
c 0 c (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.

theorem ennreal.cancel_of_lt {a : ennreal} (h : a < ) :

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

theorem ennreal.cancel_of_lt' {a b : ennreal} (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 : ennreal} (h : a ) :
a + b = a + c b = c
theorem ennreal.add_left_inj {a b c : ennreal} (h : a ) :
b + a = c + a b = c
theorem ennreal.sub_eq_Inf {a b : ennreal} :
a - b = has_Inf.Inf {d : ennreal | a d + b}
theorem ennreal.coe_sub {r p : nnreal} :
(r - p) = r - p

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

theorem ennreal.top_sub_coe {r : nnreal} :

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

theorem ennreal.sub_top {a : ennreal} :
a - = 0

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

theorem ennreal.sub_eq_top_iff {a b : ennreal} :
a - b = a = b
theorem ennreal.sub_ne_top {a b : ennreal} (ha : a ) :
a - b
@[simp, norm_cast]
theorem ennreal.nat_cast_sub (m n : ) :
(m - n) = m - n
@[protected]
theorem ennreal.sub_eq_of_eq_add {a b c : ennreal} (hb : b ) :
a = c + b a - b = c
@[protected]
theorem ennreal.eq_sub_of_add_eq {a b c : ennreal} (hc : c ) :
a + c = b a = b - c
@[protected]
theorem ennreal.sub_eq_of_eq_add_rev {a b c : ennreal} (hb : b ) :
a = b + c a - b = c
theorem ennreal.sub_eq_of_add_eq {a b c : ennreal} (hb : b ) (hc : a + b = c) :
c - b = a
@[protected, simp]
theorem ennreal.add_sub_cancel_left {a b : ennreal} (ha : a ) :
a + b - a = b
@[protected, simp]
theorem ennreal.add_sub_cancel_right {a b : ennreal} (hb : b ) :
a + b - b = a
@[protected]
theorem ennreal.lt_add_of_sub_lt_left {a b c : ennreal} (h : a b ) :
a - b < c a < b + c
@[protected]
theorem ennreal.lt_add_of_sub_lt_right {a b c : ennreal} (h : a c ) :
a - c < b a < b + c
theorem ennreal.le_sub_of_add_le_left {a b c : ennreal} (ha : a ) :
a + b c b c - a
theorem ennreal.le_sub_of_add_le_right {a b c : ennreal} (hb : b ) :
a + b c a c - b
@[protected]
theorem ennreal.sub_lt_of_lt_add {a b c : ennreal} (hac : c a) (h : a < b + c) :
a - c < b
@[protected]
theorem ennreal.sub_lt_iff_lt_right {a b c : ennreal} (hb : b ) (hab : b a) :
a - b < c a < c + b
@[protected]
theorem ennreal.sub_lt_self {a b : ennreal} (ha : a ) (ha₀ : a 0) (hb : b 0) :
a - b < a
@[protected]
theorem ennreal.sub_lt_self_iff {a b : ennreal} (ha : a ) :
a - b < a 0 < a 0 < b
theorem ennreal.sub_lt_of_sub_lt {a b c : ennreal} (h₂ : c a) (h₃ : a b ) (h₁ : a - b < c) :
a - c < b
theorem ennreal.sub_sub_cancel {a b : ennreal} (h : a ) (h2 : b a) :
a - (a - b) = b
theorem ennreal.sub_right_inj {a b c : ennreal} (ha : a ) (hb : b a) (hc : c a) :
a - b = a - c b = c
theorem ennreal.sub_mul {a b c : ennreal} (h : 0 < b b < a c ) :
(a - b) * c = a * c - b * c
theorem ennreal.mul_sub {a b c : ennreal} (h : 0 < c c < b a ) :
a * (b - c) = a * b - a * c
theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α ennreal} (h : (a : α), a s f a ) :
s.prod (λ (a : α), f a) <

A product of finite numbers is still finite

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α ennreal} (h : (a : α), a s f a ) :
s.sum (λ (a : α), f a) <

A sum of finite numbers is still finite

theorem ennreal.sum_lt_top_iff {α : Type u_1} {s : finset α} {f : α ennreal} :
s.sum (λ (a : α), f a) < (a : α), a s f a <

A sum of finite numbers is still finite

theorem ennreal.sum_eq_top_iff {α : Type u_1} {s : finset α} {f : α ennreal} :
s.sum (λ (x : α), 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 : α ennreal} (h : s.sum (λ (x : α), f x) ) {a : α} (ha : a s) :
f a <
theorem ennreal.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α ennreal} (hf : (a : α), a s f a ) :
(s.sum (λ (a : α), f a)).to_nnreal = s.sum (λ (a : α), (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 : α ennreal} (hf : (a : α), a s f a ) :
(s.sum (λ (a : α), f a)).to_real = s.sum (λ (a : α), (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 s 0 f i) :
ennreal.of_real (s.sum (λ (i : α), f i)) = s.sum (λ (i : α), ennreal.of_real (f i))
theorem ennreal.sum_lt_sum_of_nonempty {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α ennreal} (Hlt : (i : α), i s f i < g i) :
s.sum (λ (i : α), f i) < s.sum (λ (i : α), g i)
theorem ennreal.exists_le_of_sum_le {α : Type u_1} {s : finset α} (hs : s.nonempty) {f g : α ennreal} (Hle : s.sum (λ (i : α), f i) s.sum (λ (i : α), g i)) :
(i : α) (H : i s), f i g i
@[protected]
theorem ennreal.Ico_eq_Iio {y : ennreal} :
theorem ennreal.mem_Iio_self_add {x ε : ennreal} :
x ε 0 x set.Iio (x + ε)
theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ennreal} :
x x 0 ε₁ 0 ε₂ 0 x set.Ioo (x - ε₁) (x + ε₂)
@[simp]
theorem ennreal.bit0_lt_bit0 {a b : ennreal} :
bit0 a < bit0 b a < b
@[simp]
theorem ennreal.bit0_le_bit0 {a b : ennreal} :
bit0 a bit0 b a b
@[simp]
theorem ennreal.bit0_inj {a b : ennreal} :
bit0 a = bit0 b a = b
@[simp]
theorem ennreal.bit0_eq_zero_iff {a : ennreal} :
bit0 a = 0 a = 0
@[simp]
theorem ennreal.bit0_top  :
@[simp]
theorem ennreal.bit0_eq_top_iff {a : ennreal} :
@[simp]
theorem ennreal.bit1_lt_bit1 {a b : ennreal} :
bit1 a < bit1 b a < b
@[simp]
theorem ennreal.bit1_le_bit1 {a b : ennreal} :
bit1 a bit1 b a b
@[simp]
theorem ennreal.bit1_inj {a b : ennreal} :
bit1 a = bit1 b a = b
@[simp]
theorem ennreal.bit1_ne_zero {a : ennreal} :
bit1 a 0
@[simp]
theorem ennreal.bit1_top  :
@[simp]
theorem ennreal.bit1_eq_top_iff {a : ennreal} :
@[simp]
theorem ennreal.bit1_eq_one_iff {a : ennreal} :
bit1 a = 1 a = 0
@[protected, instance]
noncomputable def ennreal.has_inv  :
Equations
@[protected, instance]
Equations
@[protected]
theorem ennreal.div_eq_inv_mul {a b : ennreal} :
a / b = b⁻¹ * a
@[simp]
theorem ennreal.inv_zero  :
@[simp]
theorem ennreal.inv_top  :
@[simp, norm_cast]
theorem ennreal.coe_inv {r : nnreal} (hr : r 0) :
@[norm_cast]
@[simp, norm_cast]
theorem ennreal.coe_div {r p : nnreal} (hr : r 0) :
(p / r) = p / r
theorem ennreal.div_zero {a : ennreal} (h : a 0) :
a / 0 =
@[protected]
theorem ennreal.inv_pow {a : ennreal} {n : } :
(a ^ n)⁻¹ = a⁻¹ ^ n
@[protected]
theorem ennreal.mul_inv_cancel {a : ennreal} (h0 : a 0) (ht : a ) :
a * a⁻¹ = 1
@[protected]
theorem ennreal.inv_mul_cancel {a : ennreal} (h0 : a 0) (ht : a ) :
a⁻¹ * a = 1
@[protected]
theorem ennreal.div_mul_cancel {a b : ennreal} (h0 : a 0) (hI : a ) :
b / a * a = b
@[protected]
theorem ennreal.mul_div_cancel' {a b : ennreal} (h0 : a 0) (hI : a ) :
a * (b / a) = b
@[protected]
theorem ennreal.mul_comm_div {a b c : ennreal} :
a / b * c = a * (c / b)
@[protected]
theorem ennreal.mul_div_right_comm {a b c : ennreal} :
a * b / c = a / c * b
@[protected, instance]
Equations
@[simp]
theorem ennreal.inv_eq_top {a : ennreal} :
a⁻¹ = a = 0
@[simp]
theorem ennreal.inv_lt_top {x : ennreal} :
x⁻¹ < 0 < x
theorem ennreal.div_lt_top {x y : ennreal} (h1 : x ) (h2 : y 0) :
x / y <
@[protected, simp]
theorem ennreal.inv_eq_zero {a : ennreal} :
a⁻¹ = 0 a =
@[protected]
theorem ennreal.inv_ne_zero {a : ennreal} :
@[protected]
theorem ennreal.div_pos {a b : ennreal} (ha : a 0) (hb : b ) :
0 < a / b
@[protected]
theorem ennreal.mul_inv {a b : ennreal} (ha : a 0 b ) (hb : a b 0) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
@[protected]
theorem ennreal.mul_div_mul_left {c : ennreal} (a b : ennreal) (hc : c 0) (hc' : c ) :
c * a / (c * b) = a / b
@[protected]
theorem ennreal.mul_div_mul_right {c : ennreal} (a b : ennreal) (hc : c 0) (hc' : c ) :
a * c / (b * c) = a / b
@[protected]
theorem ennreal.sub_div {a b c : ennreal} (h : 0 < b b < a c 0) :
(a - b) / c = a / c - b / c
@[protected, simp]
theorem ennreal.inv_pos {a : ennreal} :
@[protected, simp]
theorem ennreal.inv_lt_inv {a b : ennreal} :
a⁻¹ < b⁻¹ b < a
@[protected, simp]
theorem ennreal.inv_le_inv {a b : ennreal} :
@[protected, simp]
theorem ennreal.inv_le_one {a : ennreal} :
a⁻¹ 1 1 a
@[protected]
theorem ennreal.one_le_inv {a : ennreal} :
1 a⁻¹ a 1
@[protected, simp]
theorem ennreal.inv_lt_one {a : ennreal} :
a⁻¹ < 1 1 < a
@[protected, simp]
theorem ennreal.one_lt_inv {a : ennreal} :
1 < a⁻¹ a < 1

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

Equations
@[simp]
theorem ennreal.div_top {a : ennreal} :
a / = 0
@[simp]
theorem ennreal.top_div_coe {p : nnreal} :
theorem ennreal.top_div_of_ne_top {a : ennreal} (h : a ) :
theorem ennreal.top_div_of_lt_top {a : ennreal} (h : a < ) :
theorem ennreal.top_div {a : ennreal} :
/ a = ite (a = ) 0
@[protected, simp]
theorem ennreal.zero_div {a : ennreal} :
0 / a = 0
theorem ennreal.div_eq_top {a b : ennreal} :
a / b = a 0 b = 0 a = b
@[protected]
theorem ennreal.le_div_iff_mul_le {a b c : ennreal} (h0 : b 0 c 0) (ht : b c ) :
a c / b a * b c
@[protected]
theorem ennreal.div_le_iff_le_mul {a b c : ennreal} (hb0 : b 0 c ) (hbt : b c 0) :
a / b c a c * b
@[protected]
theorem ennreal.lt_div_iff_mul_lt {a b c : ennreal} (hb0 : b 0 c ) (hbt : b c 0) :
c < a / b c * b < a
theorem ennreal.div_le_of_le_mul {a b c : ennreal} (h : a b * c) :
a / c b
theorem ennreal.div_le_of_le_mul' {a b c : ennreal} (h : a b * c) :
a / b c
theorem ennreal.mul_le_of_le_div {a b c : ennreal} (h : a b / c) :
a * c b
theorem ennreal.mul_le_of_le_div' {a b c : ennreal} (h : a b / c) :
c * a b
@[protected]
theorem ennreal.div_lt_iff {a b c : ennreal} (h0 : b 0 c 0) (ht : b c ) :
c / b < a c < a * b
theorem ennreal.mul_lt_of_lt_div {a b c : ennreal} (h : a < b / c) :
a * c < b
theorem ennreal.mul_lt_of_lt_div' {a b c : ennreal} (h : a < b / c) :
c * a < b
theorem ennreal.inv_le_iff_le_mul {a b : ennreal} (h₁ : b = a 0) (h₂ : a = b 0) :
a⁻¹ b 1 a * b
@[simp]
theorem ennreal.le_inv_iff_mul_le {a b : ennreal} :
a b⁻¹ a * b 1
@[protected]
theorem ennreal.div_le_div {a b c d : ennreal} (hab : a b) (hdc : d c) :
a / c b / d
@[protected]
theorem ennreal.div_le_div_left {a b : ennreal} (h : a b) (c : ennreal) :
c / b c / a
@[protected]
theorem ennreal.div_le_div_right {a b : ennreal} (h : a b) (c : ennreal) :
a / c b / c
@[protected]
theorem ennreal.eq_inv_of_mul_eq_one_left {a b : ennreal} (h : a * b = 1) :
a = b⁻¹
theorem ennreal.mul_le_iff_le_inv {a b r : ennreal} (hr₀ : r 0) (hr₁ : r ) :
r * a b a r⁻¹ * b
@[protected]
theorem ennreal.le_inv_smul_iff {a b : ennreal} {r : nnreal} (hr₀ : r 0) :
a r⁻¹ b r a b

A variant of le_inv_smul_iff that holds for ennreal.

@[protected]
theorem ennreal.inv_smul_le_iff {a b : ennreal} {r : nnreal} (hr₀ : r 0) :
r⁻¹ a b a r b

A variant of inv_smul_le_iff that holds for ennreal.

theorem ennreal.le_of_forall_nnreal_lt {x y : ennreal} (h : (r : nnreal), r < x r y) :
x y
theorem ennreal.le_of_forall_pos_nnreal_lt {x y : ennreal} (h : (r : nnreal), 0 < r r < x r y) :
x y
theorem ennreal.eq_top_of_forall_nnreal_le {x : ennreal} (h : (r : nnreal), r x) :
x =
@[protected]
theorem ennreal.add_div {a b c : ennreal} :
(a + b) / c = a / c + b / c
@[protected]
theorem ennreal.div_add_div_same {a b c : ennreal} :
a / c + b / c = (a + b) / c
@[protected]
theorem ennreal.div_self {a : ennreal} (h0 : a 0) (hI : a ) :
a / a = 1
theorem ennreal.mul_div_le {a b : ennreal} :
a * (b / a) b
theorem ennreal.eq_div_iff {a b c : ennreal} (ha : a 0) (ha' : a ) :
b = c / a a * b = c
@[protected]
theorem ennreal.div_eq_div_iff {a b c d : ennreal} (ha : a 0) (ha' : a ) (hb : b 0) (hb' : b ) :
c / b = d / a a * c = b * d
theorem ennreal.div_eq_one_iff {a b : ennreal} (hb₀ : b 0) (hb₁ : b ) :
a / b = 1 a = b
@[protected, simp]
theorem ennreal.add_halves (a : ennreal) :
a / 2 + a / 2 = a
@[simp]
theorem ennreal.add_thirds (a : ennreal) :
a / 3 + a / 3 + a / 3 = a
@[simp]
theorem ennreal.div_zero_iff {a b : ennreal} :
a / b = 0 a = 0 b =
@[simp]
theorem ennreal.div_pos_iff {a b : ennreal} :
0 < a / b a 0 b
@[protected]
theorem ennreal.half_pos {a : ennreal} (h : a 0) :
0 < a / 2
@[protected]
@[protected]
theorem ennreal.half_lt_self {a : ennreal} (hz : a 0) (ht : a ) :
a / 2 < a
@[protected]
theorem ennreal.half_le_self {a : ennreal} :
a / 2 a
theorem ennreal.sub_half {a : ennreal} (h : a ) :
a - a / 2 = a / 2
@[simp]

The birational order isomorphism between ℝ≥0∞ and the unit interval set.Iic (1 : ℝ≥0∞).

Equations
noncomputable def ennreal.order_iso_Iic_coe (a : nnreal) :

Order isomorphism between an initial interval in ℝ≥0∞ and an initial interval in ℝ≥0.

Equations

An order isomorphism between the extended nonnegative real numbers and the unit interval.

Equations
theorem ennreal.exists_inv_nat_lt {a : ennreal} (h : a 0) :
(n : ), (n)⁻¹ < a
theorem ennreal.exists_nat_pos_mul_gt {a b : ennreal} (ha : a 0) (hb : b ) :
(n : ) (H : n > 0), b < n * a
theorem ennreal.exists_nat_mul_gt {a b : ennreal} (ha : a 0) (hb : b ) :
(n : ), b < n * a
theorem ennreal.exists_nat_pos_inv_mul_lt {a b : ennreal} (ha : a ) (hb : b 0) :
(n : ) (H : n > 0), (n)⁻¹ * a < b
theorem ennreal.exists_nnreal_pos_mul_lt {a b : ennreal} (ha : a ) (hb : b 0) :
(n : nnreal) (H : n > 0), n * a < b
theorem ennreal.exists_inv_two_pow_lt {a : ennreal} (ha : a 0) :
(n : ), 2⁻¹ ^ n < a
@[simp, norm_cast]
theorem ennreal.coe_zpow {r : nnreal} (hr : r 0) (n : ) :
(r ^ n) = r ^ n
theorem ennreal.zpow_pos {a : ennreal} (ha : a 0) (h'a : a ) (n : ) :
0 < a ^ n
theorem ennreal.zpow_lt_top {a : ennreal} (ha : a 0) (h'a : a ) (n : ) :
a ^ n <
theorem ennreal.exists_mem_Ico_zpow {x y : ennreal} (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 : ennreal} (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 : ennreal} (hy : 1 < y) (h'y : y ) :
set.Ioo 0 = (n : ), set.Ico (y ^ n) (y ^ (n + 1))
theorem ennreal.zpow_le_of_le {x : ennreal} (hx : 1 x) {a b : } (h : a b) :
x ^ a x ^ b
theorem ennreal.monotone_zpow {x : ennreal} (hx : 1 x) :
@[protected]
theorem ennreal.zpow_add {x : ennreal} (hx : x 0) (h'x : x ) (m n : ) :
x ^ (m + n) = x ^ m * x ^ n
theorem ennreal.to_real_add {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_sub_of_le {a b : ennreal} (h : b a) (ha : a ) :
theorem ennreal.le_to_real_sub {a b : ennreal} (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 : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_mono {a b : ennreal} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_real_lt_to_real {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_strict_mono {a b : ennreal} (hb : b ) (h : a < b) :
theorem ennreal.to_nnreal_mono {a b : ennreal} (hb : b ) (h : a b) :
@[simp]
theorem ennreal.to_nnreal_le_to_nnreal {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_nnreal_strict_mono {a b : ennreal} (hb : b ) (h : a < b) :
@[simp]
theorem ennreal.to_nnreal_lt_to_nnreal {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_nnreal_pos {a : ennreal} (ha₀ : a 0) (ha_top : a ) :
theorem ennreal.to_real_pos_iff {a : ennreal} :
0 < a.to_real 0 < a a <
theorem ennreal.to_real_pos {a : ennreal} (ha₀ : a 0) (ha_top : a ) :
@[simp]
@[simp]
theorem ennreal.of_real_eq_of_real_iff {p q : } (hp : 0 p) (hq : 0 q) :
@[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 : } :

Alias of the reverse direction of ennreal.of_real_eq_zero.

theorem ennreal.of_real_sub (p : ) {q : } (hq : 0 q) :
theorem ennreal.of_real_lt_iff_lt_to_real {a : } {b : ennreal} (ha : 0 a) (hb : b ) :
theorem ennreal.le_of_real_iff_to_real_le {a : ennreal} {b : } (ha : a ) (hb : 0 b) :
theorem ennreal.to_real_le_of_le_of_real {a : ennreal} {b : } (hb : 0 b) (h : a ennreal.of_real b) :
theorem ennreal.of_real_pow {p : } (hp : 0 p) (n : ) :
@[simp]
@[simp]
theorem ennreal.smul_to_nnreal (a : nnreal) (b : ennreal) :

ennreal.to_nnreal as a monoid_hom.

Equations
@[simp]
theorem ennreal.to_nnreal_pow (a : ennreal) (n : ) :
(a ^ n).to_nnreal = a.to_nnreal ^ n
@[simp]
theorem ennreal.to_nnreal_prod {ι : Type u_1} {s : finset ι} {f : ι ennreal} :
(s.prod (λ (i : ι), f i)).to_nnreal = s.prod (λ (i : ι), (f i).to_nnreal)
@[simp]
theorem ennreal.to_real_mul {a b : ennreal} :
@[simp]
theorem ennreal.to_real_pow (a : ennreal) (n : ) :
(a ^ n).to_real = a.to_real ^ n
@[simp]
theorem ennreal.to_real_prod {ι : Type u_1} {s : finset ι} {f : ι ennreal} :
(s.prod (λ (i : ι), f i)).to_real = s.prod (λ (i : ι), (f i).to_real)
theorem ennreal.to_real_of_real_mul (c : ) (a : ennreal) (h : 0 c) :
theorem ennreal.to_real_eq_to_real {a b : ennreal} (ha : a ) (hb : b ) :
theorem ennreal.to_real_smul (r : nnreal) (s : ennreal) :
(r s).to_real = r s.to_real
@[protected]
theorem ennreal.trichotomy (p : ennreal) :
p = 0 p = 0 < p.to_real
@[protected]
theorem ennreal.trichotomy₂ {p q : ennreal} (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 : ennreal) [fact (1 p)] :
theorem ennreal.to_real_div (a b : ennreal) :
theorem ennreal.of_real_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α } (hf : (i : α), i s 0 f i) :
ennreal.of_real (s.prod (λ (i : α), f i)) = s.prod (λ (i : α), ennreal.of_real (f i))
@[simp]
theorem ennreal.to_nnreal_bit1 {x : ennreal} (hx_top : x ) :
@[simp]
@[simp]
theorem ennreal.to_real_bit1 {x : ennreal} (hx_top : x ) :
@[simp]
theorem ennreal.of_real_bit1 {r : } (hr : 0 r) :
theorem ennreal.to_nnreal_infi {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(infi f).to_nnreal = (i : ι), (f i).to_nnreal
theorem ennreal.to_nnreal_supr {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(supr f).to_nnreal = (i : ι), (f i).to_nnreal
theorem ennreal.to_real_infi {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(infi f).to_real = (i : ι), (f i).to_real
theorem ennreal.to_real_supr {ι : Sort u_3} {f : ι ennreal} (hf : (i : ι), f i ) :
(supr f).to_real = (i : ι), (f i).to_real
theorem ennreal.infi_add {a : ennreal} {ι : Sort u_3} {f : ι ennreal} :
infi f + a = (i : ι), f i + a
theorem ennreal.supr_sub {a : ennreal} {ι : Sort u_3} {f : ι ennreal} :
( (i : ι), f i) - a = (i : ι), f i - a
theorem ennreal.sub_infi {a : ennreal} {ι : Sort u_3} {f : ι ennreal} :
(a - (i : ι), f i) = (i : ι), a - f i
theorem ennreal.Inf_add {a : ennreal} {s : set ennreal} :
has_Inf.Inf s + a = (b : ennreal) (H : b s), b + a
theorem ennreal.add_infi {ι : Sort u_3} {f : ι ennreal} {a : ennreal} :
a + infi f = (b : ι), a + f b
theorem ennreal.infi_add_infi {ι : Sort u_3} {f g : ι ennreal} (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 : ι α ennreal} {s : finset α} [nonempty ι] (h : (t : finset α) (i j : ι), (k : ι), (a : α), a t f k a f i a f k a f j a) :
( (i : ι), s.sum (λ (a : α), f i a)) = s.sum (λ (a : α), (i : ι), f i a)
theorem ennreal.infi_mul_of_ne {ι : Sort u_1} {f : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} {x : ennreal} (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 : ι ennreal} :
( (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 : ennreal} :
a b = 0 a = 0 b = 0
theorem ennreal.supr_coe_nat  :
( (n : ), n) =

Extension for the positivity tactic: cast from ℝ≥0 to ℝ≥0∞.

Extension for the positivity tactic: ennreal.of_real is positive if its input is.