mathlib documentation

data.real.ennreal

Extended non-negative reals #

We define ennreal = ℝ≥0∞ := with_no ℝ≥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 #

ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as with_top ℝ≥0; it is equipped with the following structures:
- coercion from ℝ≥0 defined in the natural way;
- the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;
- a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;
- a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;
- a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;
- a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.
- a / b is defined as a * b⁻¹.
The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.
Coercions to/from other types:
- coercion ℝ≥0 → ℝ≥0∞ is defined as has_coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;
- ennreal.to_nnreal sends ↑p to p and ∞ to 0;
- ennreal.to_real := coe ∘ ennreal.to_nnreal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;
- ennreal.of_real := coe ∘ nnreal.of_real sends x : ℝ to ↑⟨max x 0, _⟩
- ennreal.ne_top_equiv_nnreal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

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 #

ℝ≥0∞: the type of the extended nonnegative real numbers;
ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in data.real.nnreal;
∞: a localized notation in ℝ≥0∞ for ⊤ : ℝ≥0∞.

def ennreal :

Type

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

Equations

ℝ≥0∞ = with_top ℝ≥0

@[instance]

def ennreal.nontrivial :

nontrivial ℝ≥0∞

@[instance]

def ennreal.densely_ordered :

densely_ordered ℝ≥0∞

@[instance]

def ennreal.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring ℝ≥0∞

@[instance]

def ennreal.complete_linear_order :

complete_linear_order ℝ≥0∞

@[instance]

def ennreal.inhabited :

inhabited ℝ≥0∞

Equations

ennreal.inhabited = {default := 0}

@[instance]

def ennreal.has_coe :

has_coe ℝ≥0 ℝ≥0∞

Equations

ennreal.has_coe = {coe := some ℝ≥0}

@[instance]

def ennreal.nnreal.can_lift :

can_lift ℝ≥0∞ ℝ≥0

Equations

ennreal.nnreal.can_lift = {coe := coe coe_to_lift, cond := λ (r : ℝ≥0∞), r ≠ ⊤, prf := ennreal.nnreal.can_lift._proof_1}

@[simp]

theorem ennreal.none_eq_top :

@[simp]

theorem ennreal.some_eq_coe (a : ℝ≥0) :

def ennreal.to_nnreal :

ℝ≥0∞ → ℝ≥0

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

Equations

ennreal.to_nnreal (some r) = r
ennreal.to_nnreal none = 0

def ennreal.to_real (a : ℝ≥0∞) :

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

Equations

a.to_real = ↑(a.to_nnreal)

def ennreal.of_real (r : ℝ) :

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

Equations

ennreal.of_real r = ↑(nnreal.of_real r)

@[simp]

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

↑r.to_nnreal = r

@[simp]

theorem ennreal.coe_to_nnreal {a : ℝ≥0∞} :

a ≠ ⊤ → ↑(a.to_nnreal) = a

@[simp]

theorem ennreal.of_real_to_real {a : ℝ≥0∞} (h : a ≠ ⊤) :

ennreal.of_real a.to_real = a

@[simp]

theorem ennreal.to_real_of_real {r : ℝ} (h : 0 ≤ r) :

(ennreal.of_real r).to_real = r

theorem ennreal.to_real_of_real' {r : ℝ} :

(ennreal.of_real r).to_real = max r 0

theorem ennreal.coe_to_nnreal_le_self {a : ℝ≥0∞} :

↑(a.to_nnreal) ≤ a

theorem ennreal.coe_nnreal_eq (r : ℝ≥0) :

↑r = ennreal.of_real ↑r

theorem ennreal.of_real_eq_coe_nnreal {x : ℝ} (h : 0 ≤ x) :

ennreal.of_real x = ↑⟨x, h⟩

@[simp]

theorem ennreal.of_real_coe_nnreal {p : ℝ≥0} :

ennreal.of_real ↑p = ↑p

@[simp]

theorem ennreal.coe_zero :

↑0 = 0

@[simp]

theorem ennreal.coe_one :

↑1 = 1

@[simp]

theorem ennreal.to_real_nonneg {a : ℝ≥0∞} :

0 ≤ a.to_real

@[simp]

theorem ennreal.top_to_nnreal :

⊤.to_nnreal = 0

@[simp]

theorem ennreal.top_to_real :

⊤.to_real = 0

@[simp]

theorem ennreal.one_to_real :

@[simp]

theorem ennreal.one_to_nnreal :

1.to_nnreal = 1

@[simp]

theorem ennreal.coe_to_real (r : ℝ≥0) :

↑r.to_real = ↑r

@[simp]

theorem ennreal.zero_to_nnreal :

0.to_nnreal = 0

@[simp]

theorem ennreal.zero_to_real :

@[simp]

theorem ennreal.of_real_zero :

ennreal.of_real 0 = 0

@[simp]

theorem ennreal.of_real_one :

ennreal.of_real 1 = 1

theorem ennreal.of_real_to_real_le {a : ℝ≥0∞} :

ennreal.of_real a.to_real ≤ a

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

theorem ennreal.to_nnreal_eq_zero_iff (x : ℝ≥0∞) :

x.to_nnreal = 0 ↔ x = 0 ∨ x = ⊤

theorem ennreal.to_real_eq_zero_iff (x : ℝ≥0∞) :

x.to_real = 0 ↔ x = 0 ∨ x = ⊤

@[simp]

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

@[simp]

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

@[simp]

theorem ennreal.of_real_ne_top {r : ℝ} :

ennreal.of_real r ≠ ⊤

@[simp]

theorem ennreal.of_real_lt_top {r : ℝ} :

ennreal.of_real r < ⊤

@[simp]

theorem ennreal.top_ne_of_real {r : ℝ} :

⊤ ≠ ennreal.of_real r

@[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]

theorem ennreal.coe_eq_coe {r q : ℝ≥0} :

↑r = ↑q ↔ r = q

@[simp]

theorem ennreal.coe_le_coe {r q : ℝ≥0} :

↑r ≤ ↑q ↔ r ≤ q

@[simp]

theorem ennreal.coe_lt_coe {r q : ℝ≥0} :

↑r < ↑q ↔ r < q

theorem ennreal.coe_mono :

@[simp]

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

↑r = 0 ↔ r = 0

@[simp]

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

0 = ↑r ↔ 0 = r

@[simp]

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

↑r = 1 ↔ r = 1

@[simp]

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

1 = ↑r ↔ 1 = r

@[simp]

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

0 ≤ ↑r ↔ 0 ≤ r

@[simp]

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

0 < ↑r ↔ 0 < r

@[simp]

theorem ennreal.coe_add {r p : ℝ≥0} :

↑(r + p) = ↑r + ↑p

@[simp]

theorem ennreal.coe_mul {r p : ℝ≥0} :

↑r * p = (↑r) * ↑p

@[simp]

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

↑(bit0 r) = bit0 ↑r

@[simp]

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

↑(bit1 r) = bit1 ↑r

theorem ennreal.coe_two :

↑2 = 2

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

theorem ennreal.two_ne_top :

def ennreal.ne_top_equiv_nnreal :

↥{a : ℝ≥0∞ | a ≠ ⊤} ≃ ℝ≥0

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

Equations

ennreal.ne_top_equiv_nnreal = {to_fun := λ (x : ↥{a : ℝ≥0∞ | a ≠ ⊤}), ↑x.to_nnreal, inv_fun := λ (x : ℝ≥0), ⟨↑x, _⟩, left_inv := ennreal.ne_top_equiv_nnreal._proof_1, right_inv := ennreal.ne_top_equiv_nnreal._proof_2}

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∞} :

def ennreal.of_nnreal_hom :

ℝ≥0 →+* ℝ≥0∞

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

Equations

ennreal.of_nnreal_hom = {to_fun := coe coe_to_lift, map_one' := ennreal.coe_one, map_mul' := ennreal.of_nnreal_hom._proof_1, map_zero' := ennreal.coe_zero, map_add' := ennreal.of_nnreal_hom._proof_2}

@[simp]

theorem ennreal.coe_of_nnreal_hom :

⇑ennreal.of_nnreal_hom = coe

@[simp]

theorem ennreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :

↑(s.indicator f a) = s.indicator (λ (x : α), ↑(f x)) a

@[simp]

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.lt_top_iff_ne_top {a : ℝ≥0∞} :

a < ⊤ ↔ a ≠ ⊤

theorem ennreal.bot_lt_iff_ne_bot {a : ℝ≥0∞} :

0 < a ↔ a ≠ 0

theorem ennreal.not_lt_top {x : ℝ≥0∞} :

¬x < ⊤ ↔ x = ⊤

theorem ennreal.add_ne_top {a b : ℝ≥0∞} :

a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

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_mul_top :

⊤ * ⊤ = ⊤

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.ne_top_of_mul_ne_top_left {a b : ℝ≥0∞} (h : a * b ≠ ⊤) (hb : b ≠ 0) :

theorem ennreal.ne_top_of_mul_ne_top_right {a b : ℝ≥0∞} (h : a * b ≠ ⊤) (ha : a ≠ 0) :

theorem ennreal.lt_top_of_mul_lt_top_left {a b : ℝ≥0∞} (h : a * b < ⊤) (hb : b ≠ 0) :

theorem ennreal.lt_top_of_mul_lt_top_right {a b : ℝ≥0∞} (h : a * b < ⊤) (ha : a ≠ 0) :

theorem ennreal.mul_lt_top_iff {a b : ℝ≥0∞} :

a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

theorem ennreal.mul_self_lt_top_iff {a : ℝ≥0∞} :

a * a < ⊤ ↔ a < ⊤

@[simp]

theorem ennreal.mul_pos {a b : ℝ≥0∞} :

0 < a * b ↔ 0 < a ∧ 0 < b

theorem ennreal.pow_eq_top {a : ℝ≥0∞} (n : ℕ) :

a ^ n = ⊤ → a = ⊤

theorem ennreal.pow_ne_top {a : ℝ≥0∞} (h : a ≠ ⊤) {n : ℕ} :

theorem ennreal.pow_lt_top {a : ℝ≥0∞} :

a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤

@[simp]

theorem ennreal.coe_finset_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :

↑∑ (a : α) in s, f a = ∑ (a : α) in s, ↑(f a)

@[simp]

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 :

@[simp]

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

@[simp]

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

theorem ennreal.zero_lt_coe_iff {p : ℝ≥0} :

0 < ↑p ↔ 0 < p

@[simp]

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

1 ≤ ↑r ↔ 1 ≤ r

@[simp]

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

↑r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ennreal.coe_lt_one_iff {p : ℝ≥0} :

↑p < 1 ↔ p < 1

@[simp]

theorem ennreal.one_lt_coe_iff {p : ℝ≥0} :

1 < ↑p ↔ 1 < p

@[simp]

theorem ennreal.coe_nat (n : ℕ) :

@[simp]

theorem ennreal.of_real_coe_nat (n : ℕ) :

ennreal.of_real ↑n = ↑n

@[simp]

theorem ennreal.nat_ne_top (n : ℕ) :

@[simp]

theorem ennreal.top_ne_nat (n : ℕ) :

@[simp]

theorem ennreal.one_lt_top :

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 = ↑p → r ≤ p

theorem ennreal.lt_iff_exists_coe {a b : ℝ≥0∞} :

a < b ↔ ∃ (p : ℝ≥0), a = ↑p ∧ ↑p < b

theorem ennreal.to_real_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ ↑b) :

a.to_real ≤ ↑b

@[simp]

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

@[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

theorem ennreal.pow_pos {a : ℝ≥0∞} :

0 < a → ∀ (n : ℕ), 0 < a ^ n

theorem ennreal.pow_ne_zero {a : ℝ≥0∞} :

a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

@[simp]

theorem ennreal.not_lt_zero {a : ℝ≥0∞} :

¬a < 0

theorem ennreal.add_lt_add_iff_left {a b c : ℝ≥0∞} :

a < ⊤ → (a + c < a + b ↔ c < b)

theorem ennreal.add_lt_add_iff_right {a b c : ℝ≥0∞} :

a < ⊤ → (c + a < b + a ↔ c < b)

theorem ennreal.lt_add_right {a b : ℝ≥0∞} (ha : a < ⊤) (hb : 0 < b) :

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 < ↑(nnreal.of_real ↑q) ∧ ↑(nnreal.of_real ↑q) < b

theorem ennreal.lt_iff_exists_real_btwn {a b : ℝ≥0∞} :

a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ennreal.of_real r ∧ ennreal.of_real r < 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]

theorem ennreal.coe_nat_lt_coe_nat {m n : ℕ} :

↑m < ↑n ↔ m < n

theorem ennreal.coe_nat_ne_top {n : ℕ} :

theorem ennreal.coe_nat_mono :

strict_mono coe

@[simp]

theorem ennreal.coe_nat_le_coe_nat {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

@[instance]

def ennreal.char_zero :

char_zero ℝ≥0∞

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

theorem ennreal.coe_min {r p : ℝ≥0} :

↑(min r p) = min ↑r ↑p

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)

@[simp]

theorem ennreal.top_mem_upper_bounds {s : set ℝ≥0∞} :

⊤ ∈ upper_bounds s

theorem ennreal.coe_mem_upper_bounds {r : ℝ≥0} {s : set ℝ≥0} :

↑r ∈ upper_bounds (coe '' s) ↔ r ∈ upper_bounds s

theorem ennreal.mul_le_mul {a b c d : ℝ≥0∞} :

a ≤ b → c ≤ d → a * 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_left_mono {a : ℝ≥0∞} :

monotone (has_mul.mul a)

theorem ennreal.mul_right_mono {a : ℝ≥0∞} :

monotone (λ (x : ℝ≥0∞), x * a)

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 ≠ 0 → a ≠ ⊤ → (a * b = a * c ↔ b = c)

theorem ennreal.mul_eq_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)

theorem ennreal.mul_le_mul_left {a b c : ℝ≥0∞} :

a ≠ 0 → a ≠ ⊤ → (a * b ≤ a * c ↔ b ≤ c)

theorem ennreal.mul_le_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c ≤ b * c ↔ a ≤ b)

theorem ennreal.mul_lt_mul_left {a b c : ℝ≥0∞} :

a ≠ 0 → a ≠ ⊤ → (a * b < a * c ↔ b < c)

theorem ennreal.mul_lt_mul_right {a b c : ℝ≥0∞} :

c ≠ 0 → c ≠ ⊤ → (a * c < b * c ↔ a < b)

@[instance]

def ennreal.has_sub :

has_sub ℝ≥0∞

Equations

ennreal.has_sub = {sub := λ (a b : ℝ≥0∞), Inf {d : ℝ≥0∞ | a ≤ d + b}}

theorem ennreal.coe_sub {r p : ℝ≥0} :

↑(p - r) = ↑p - ↑r

@[simp]

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

⊤ - ↑r = ⊤

@[simp]

theorem ennreal.sub_eq_zero_of_le {a b : ℝ≥0∞} (h : a ≤ b) :

a - b = 0

@[simp]

theorem ennreal.sub_self {a : ℝ≥0∞} :

a - a = 0

@[simp]

theorem ennreal.zero_sub {a : ℝ≥0∞} :

0 - a = 0

@[simp]

theorem ennreal.sub_infty {a : ℝ≥0∞} :

a - ⊤ = 0

theorem ennreal.sub_le_sub {a b c d : ℝ≥0∞} (h₁ : a ≤ b) (h₂ : d ≤ c) :

a - c ≤ b - d

@[simp]

theorem ennreal.add_sub_self {a b : ℝ≥0∞} :

b < ⊤ → a + b - b = a

@[simp]

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

a + b - a = b

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

@[simp]

theorem ennreal.sub_add_cancel_of_le {a b : ℝ≥0∞} :

b ≤ a → a - b + b = a

@[simp]

theorem ennreal.add_sub_cancel_of_le {a b : ℝ≥0∞} (h : b ≤ a) :

b + (a - b) = a

theorem ennreal.sub_add_self_eq_max {a b : ℝ≥0∞} :

a - b + b = max a b

theorem ennreal.le_sub_add_self {a b : ℝ≥0∞} :

a ≤ a - b + b

@[simp]

theorem ennreal.sub_le_iff_le_add {a b c : ℝ≥0∞} :

a - b ≤ c ↔ a ≤ c + b

theorem ennreal.sub_le_iff_le_add' {a b c : ℝ≥0∞} :

a - b ≤ c ↔ a ≤ b + c

theorem ennreal.sub_eq_of_add_eq {a b c : ℝ≥0∞} :

b ≠ ⊤ → a + b = c → c - b = a

theorem ennreal.sub_le_of_sub_le {a b c : ℝ≥0∞} (h : a - b ≤ c) :

a - c ≤ b

theorem ennreal.sub_lt_self {a b : ℝ≥0∞} :

a ≠ ⊤ → a ≠ 0 → 0 < b → a - b < a

@[simp]

theorem ennreal.sub_eq_zero_iff_le {a b : ℝ≥0∞} :

a - b = 0 ↔ a ≤ b

@[simp]

theorem ennreal.zero_lt_sub_iff_lt {a b : ℝ≥0∞} :

0 < a - b ↔ b < a

theorem ennreal.lt_sub_iff_add_lt {a b c : ℝ≥0∞} :

a < b - c ↔ a + c < b

theorem ennreal.sub_le_self (a b : ℝ≥0∞) :

a - b ≤ a

@[simp]

theorem ennreal.sub_zero {a : ℝ≥0∞} :

a - 0 = a

theorem ennreal.sub_le_sub_add_sub {a b c : ℝ≥0∞} :

a - c ≤ a - b + (b - c)

A version of triangle inequality for difference as a "distance".

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 < b → b < a → c ≠ ⊤) :

(a - b) * c = a * c - b * c

theorem ennreal.mul_sub {a b c : ℝ≥0∞} (h : 0 < c → c < b → a ≠ ⊤) :

a * (b - c) = a * b - a * c

theorem ennreal.sub_mul_ge {a b c : ℝ≥0∞} :

a * c - b * c ≤ (a - b) * c

theorem ennreal.prod_lt_top {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (h : ∀ (a : α), a ∈ s → f 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∞} :

(∀ (a : α), a ∈ s → f 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 ∈ s → f 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.to_nnreal_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0∞} (hf : ∀ (a : α), a ∈ s → f 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 ∈ s → f 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 ∈ s → 0 ≤ f i) :

ennreal.of_real (∑ (i : α) in s, f i) = ∑ (i : α) in s, ennreal.of_real (f i)

theorem ennreal.Ico_eq_Iio {y : ℝ≥0∞} :

set.Ico 0 y = set.Iio y

theorem ennreal.mem_Iio_self_add {x ε : ℝ≥0∞} :

x ≠ ⊤ → 0 < ε → x ∈ set.Iio (x + ε)

theorem ennreal.not_mem_Ioo_self_sub {x y ε : ℝ≥0∞} :

x = 0 → x ∉ set.Ioo (x - ε) y

theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ℝ≥0∞} :

x ≠ ⊤ → x ≠ 0 → 0 < ε₁ → 0 < ε₂ → x ∈ 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]

theorem ennreal.bit0_eq_top_iff {a : ℝ≥0∞} :

bit0 a = ⊤ ↔ a = ⊤

@[simp]

theorem ennreal.bit1_inj {a b : ℝ≥0∞} :

bit1 a = bit1 b ↔ a = b

@[simp]

theorem ennreal.bit1_ne_zero {a : ℝ≥0∞} :

@[simp]

theorem ennreal.bit1_eq_one_iff {a : ℝ≥0∞} :

bit1 a = 1 ↔ a = 0

@[simp]

theorem ennreal.bit1_eq_top_iff {a : ℝ≥0∞} :

bit1 a = ⊤ ↔ a = ⊤

@[instance]

def ennreal.has_inv :

has_inv ℝ≥0∞

Equations

ennreal.has_inv = {inv := λ (a : ℝ≥0∞), Inf {b : ℝ≥0∞ | 1 ≤ a * b}}

@[instance]

def ennreal.div_inv_monoid :

div_inv_monoid ℝ≥0∞

Equations

ennreal.div_inv_monoid = {mul := monoid.mul infer_instance, mul_assoc := ennreal.div_inv_monoid._proof_1, one := monoid.one infer_instance, one_mul := ennreal.div_inv_monoid._proof_2, mul_one := ennreal.div_inv_monoid._proof_3, npow := npow infer_instance, npow_zero' := ennreal.div_inv_monoid._proof_4, npow_succ' := ennreal.div_inv_monoid._proof_5, inv := has_inv.inv ennreal.has_inv, div := λ (a b : ℝ≥0∞), monoid.mul a b⁻¹, div_eq_mul_inv := ennreal.div_inv_monoid._proof_6}

@[simp]

theorem ennreal.inv_zero :

@[simp]

theorem ennreal.inv_top :

@[simp]

theorem ennreal.coe_inv {r : ℝ≥0} (hr : r ≠ 0) :

↑r⁻¹ = (↑r)⁻¹

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

↑r⁻¹ ≤ (↑r)⁻¹

theorem ennreal.coe_inv_two :

↑2⁻¹ = 2⁻¹

@[simp]

theorem ennreal.coe_div {r p : ℝ≥0} (hr : r ≠ 0) :

↑(p / r) = ↑p / ↑r

@[simp]

theorem ennreal.inv_one :

@[simp]

theorem ennreal.div_one {a : ℝ≥0∞} :

a / 1 = a

theorem ennreal.inv_pow {a : ℝ≥0∞} {n : ℕ} :

(a ^ n)⁻¹ = a⁻¹ ^ n

@[simp]

theorem ennreal.inv_inv {a : ℝ≥0∞} :

a⁻¹ ⁻¹ = a

theorem ennreal.inv_involutive :

function.involutive (λ (a : ℝ≥0∞), a⁻¹)

theorem ennreal.inv_bijective :

function.bijective (λ (a : ℝ≥0∞), a⁻¹)

@[simp]

theorem ennreal.inv_eq_inv {a b : ℝ≥0∞} :

a⁻¹ = b⁻¹ ↔ a = b

@[simp]

theorem ennreal.inv_eq_top {a : ℝ≥0∞} :

a⁻¹ = ⊤ ↔ a = 0

theorem ennreal.inv_ne_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 : 0 < y) :

x / y < ⊤

@[simp]

theorem ennreal.inv_eq_zero {a : ℝ≥0∞} :

a⁻¹ = 0 ↔ a = ⊤

theorem ennreal.inv_ne_zero {a : ℝ≥0∞} :

a⁻¹ ≠ 0 ↔ a ≠ ⊤

@[simp]

theorem ennreal.inv_pos {a : ℝ≥0∞} :

0 < a⁻¹ ↔ a ≠ ⊤

@[simp]

theorem ennreal.inv_lt_inv {a b : ℝ≥0∞} :

a⁻¹ < b⁻¹ ↔ b < a

theorem ennreal.inv_lt_iff_inv_lt {a b : ℝ≥0∞} :

a⁻¹ < b ↔ b⁻¹ < a

theorem ennreal.lt_inv_iff_lt_inv {a b : ℝ≥0∞} :

a < b⁻¹ ↔ b < a⁻¹

@[simp]

theorem ennreal.inv_le_inv {a b : ℝ≥0∞} :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem ennreal.inv_le_iff_inv_le {a b : ℝ≥0∞} :

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem ennreal.le_inv_iff_le_inv {a b : ℝ≥0∞} :

a ≤ b⁻¹ ↔ b ≤ a⁻¹

@[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

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} :

⊤ / ↑p = ⊤

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.div_le_of_le_mul {a b c : ℝ≥0∞} (h : a ≤ b * c) :

a / c ≤ b

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.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.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 < x → ↑r ≤ y) :

x ≤ y

theorem ennreal.eq_top_of_forall_nnreal_le {x : ℝ≥0∞} (h : ∀ (r : ℝ≥0), ↑r ≤ x) :

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

theorem ennreal.inv_two_add_inv_two :

2⁻¹ + 2⁻¹ = 1

theorem ennreal.add_halves (a : ℝ≥0∞) :

a / 2 + a / 2 = 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 : 0 < a) :

0 < a / 2

theorem ennreal.one_half_lt_one :

theorem ennreal.half_lt_self {a : ℝ≥0∞} (hz : a ≠ 0) (ht : a ≠ ⊤) :

a / 2 < a

theorem ennreal.sub_half {a : ℝ≥0∞} (h : a ≠ ⊤) :

a - a / 2 = a / 2

theorem ennreal.one_sub_inv_two :

1 - 2⁻¹ = 2⁻¹

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

theorem ennreal.to_real_add {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

(a + b).to_real = a.to_real + b.to_real

theorem ennreal.to_real_add_le {a b : ℝ≥0∞} :

(a + b).to_real ≤ a.to_real + b.to_real

theorem ennreal.of_real_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ennreal.of_real (p + q) = ennreal.of_real p + ennreal.of_real q

theorem ennreal.of_real_add_le {p q : ℝ} :

ennreal.of_real (p + q) ≤ ennreal.of_real p + ennreal.of_real q

@[simp]

theorem ennreal.to_real_le_to_real {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_real ≤ b.to_real ↔ a ≤ b

@[simp]

theorem ennreal.to_real_lt_to_real {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a.to_real < b.to_real ↔ a < b

theorem ennreal.to_real_max {a b : ℝ≥0∞} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

(max a b).to_real = max a.to_real b.to_real

theorem ennreal.to_nnreal_pos_iff {a : ℝ≥0∞} :

0 < a.to_nnreal ↔ 0 < a ∧ a ≠ ⊤

theorem ennreal.to_real_pos_iff {a : ℝ≥0∞} :

0 < a.to_real ↔ 0 < a ∧ a ≠ ⊤

theorem ennreal.of_real_le_of_real {p q : ℝ} (h : p ≤ q) :

ennreal.of_real p ≤ ennreal.of_real q

theorem ennreal.of_real_le_of_le_to_real {a : ℝ} {b : ℝ≥0∞} (h : a ≤ b.to_real) :

ennreal.of_real a ≤ b

@[simp]

theorem ennreal.of_real_le_of_real_iff {p q : ℝ} (h : 0 ≤ q) :

ennreal.of_real p ≤ ennreal.of_real q ↔ p ≤ q

@[simp]

theorem ennreal.of_real_lt_of_real_iff {p q : ℝ} (h : 0 < q) :

ennreal.of_real p < ennreal.of_real q ↔ p < q

theorem ennreal.of_real_lt_of_real_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :

ennreal.of_real p < ennreal.of_real q ↔ p < q

@[simp]

theorem ennreal.of_real_pos {p : ℝ} :

0 < ennreal.of_real p ↔ 0 < p

@[simp]

theorem ennreal.of_real_eq_zero {p : ℝ} :

ennreal.of_real p = 0 ↔ p ≤ 0

theorem ennreal.of_real_le_iff_le_to_real {a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ⊤) :

ennreal.of_real a ≤ b ↔ a ≤ b.to_real

theorem ennreal.of_real_lt_iff_lt_to_real {a : ℝ} {b : ℝ≥0∞} (ha : 0 ≤ a) (hb : b ≠ ⊤) :

ennreal.of_real a < b ↔ a < b.to_real

theorem ennreal.le_of_real_iff_to_real_le {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :

a ≤ ennreal.of_real b ↔ a.to_real ≤ b

theorem ennreal.to_real_le_of_le_of_real {a : ℝ≥0∞} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ennreal.of_real b) :

a.to_real ≤ b

theorem ennreal.lt_of_real_iff_to_real_lt {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ⊤) :

a < ennreal.of_real b ↔ a.to_real < b

theorem ennreal.of_real_mul {p q : ℝ} (hp : 0 ≤ p) :

ennreal.of_real (p * q) = (ennreal.of_real p) * ennreal.of_real q

theorem ennreal.of_real_inv_of_pos {x : ℝ} (hx : 0 < x) :

(ennreal.of_real x)⁻¹ = ennreal.of_real x⁻¹

theorem ennreal.of_real_div_of_pos {x y : ℝ} (hy : 0 < y) :

ennreal.of_real (x / y) = ennreal.of_real x / ennreal.of_real y

theorem ennreal.to_real_of_real_mul (c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) :

((ennreal.of_real c) * a).to_real = c * a.to_real

@[simp]

theorem ennreal.to_nnreal_mul_top (a : ℝ≥0∞) :

(a * ⊤).to_nnreal = 0

@[simp]

theorem ennreal.to_nnreal_top_mul (a : ℝ≥0∞) :

(⊤ * a).to_nnreal = 0

@[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 < ⊤) :

a.to_real = b.to_real ↔ a = b

def ennreal.to_nnreal_hom :

ℝ≥0∞ →* ℝ≥0

ennreal.to_nnreal as a monoid_hom.

Equations

ennreal.to_nnreal_hom = {to_fun := ennreal.to_nnreal, map_one' := ennreal.to_nnreal_hom._proof_1, map_mul' := ennreal.to_nnreal_hom._proof_2}

theorem ennreal.to_nnreal_mul {a b : ℝ≥0∞} :

(a * b).to_nnreal = (a.to_nnreal) * b.to_nnreal

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

def ennreal.to_real_hom :

ℝ≥0∞ →* ℝ

ennreal.to_real as a monoid_hom.

Equations

ennreal.to_real_hom = ↑nnreal.to_real_hom.comp ennreal.to_nnreal_hom

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 ∈ s → 0 ≤ f i) :

ennreal.of_real (∏ (i : α) in s, f i) = ∏ (i : α) in s, ennreal.of_real (f i)

@[simp]

theorem ennreal.to_nnreal_bit0 {x : ℝ≥0∞} :

(bit0 x).to_nnreal = bit0 x.to_nnreal

@[simp]

theorem ennreal.to_nnreal_bit1 {x : ℝ≥0∞} (hx_top : x ≠ ⊤) :

(bit1 x).to_nnreal = bit1 x.to_nnreal

@[simp]

theorem ennreal.to_real_bit0 {x : ℝ≥0∞} :

(bit0 x).to_real = bit0 x.to_real

@[simp]

theorem ennreal.to_real_bit1 {x : ℝ≥0∞} (hx_top : x ≠ ⊤) :

(bit1 x).to_real = bit1 x.to_real

@[simp]

theorem ennreal.of_real_bit0 {r : ℝ} (hr : 0 ≤ r) :

ennreal.of_real (bit0 r) = bit0 (ennreal.of_real r)

@[simp]

theorem ennreal.of_real_bit1 {r : ℝ} (hr : 0 ≤ r) :

ennreal.of_real (bit1 r) = bit1 (ennreal.of_real 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 ∈ t → f 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 {ι : Sort u_1} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ≠ ⊤) :

(infi f) * x = ⨅ (i : ι), (f i) * x

theorem ennreal.mul_infi {ι : Sort u_1} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ≠ ⊤) :

x * infi f = ⨅ (i : ι), x * f i

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) = ⊤

theorem ennreal.le_of_add_le_add_left {a b c : ℝ≥0∞} :

a < ⊤ → a + b ≤ a + c → b ≤ c

le_of_add_le_add_left is normally applicable to ordered_cancel_add_comm_monoid, but it holds in ℝ≥0∞ with the additional assumption that a < ∞.

theorem ennreal.le_of_add_le_add_right {a b c : ℝ≥0∞} :

a < ⊤ → b + a ≤ c + a → b ≤ c

le_of_add_le_add_right is normally applicable to ordered_cancel_add_comm_monoid, but it holds in ℝ≥0∞ with the additional assumption that a < ∞.