mathlib documentation

data.real.ennreal

Extended non-negative reals

We define ennreal := 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 ennreal and prove basic properties of these operations, order, and conversions to/from ℝ, ℝ≥0, and ℕ.

Main definitions

ennreal: 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 ennreal into a canonically ordered commutative semiring of characteristic zero.
Coercions to/from other types:
- coercion ℝ≥0 → ennreal is defined as has_coe, so one can use (p : ℝ≥0) in a context that expects a : ennreal, 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 : ennreal // a ≠ 0} and ℝ≥0.

Implementation notes

We define a can_lift ennreal ℝ≥0 instance, so one of the ways to prove theorems about an ennreal 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 : α → ennreal) (hf : ∀ x, f x ≠ ⊤).

Notations

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

def ennreal :

Type

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

Equations

ennreal = with_top ℝ≥0

@[instance]

def ennreal.nontrivial :

nontrivial ennreal

@[instance]

def ennreal.densely_ordered :

densely_ordered ennreal

@[instance]

def ennreal.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring ennreal

@[instance]

def ennreal.complete_linear_order :

complete_linear_order ennreal

@[instance]

def ennreal.inhabited :

inhabited ennreal

Equations

ennreal.inhabited = {default := 0}

@[instance]

def ennreal.has_coe :

has_coe ℝ≥0 ennreal

Equations

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

@[instance]

def ennreal.can_lift :

can_lift ennreal ℝ≥0

Equations

ennreal.can_lift = {coe := coe coe_to_lift, cond := λ (r : ennreal), r ≠ ⊤, prf := ennreal.can_lift._proof_1}

@[simp]

theorem ennreal.none_eq_top :

@[simp]

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

def ennreal.to_nnreal :

ennreal → ℝ≥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 :

ennreal → ℝ

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

Equations

a.to_real = ↑(a.to_nnreal)

def ennreal.of_real :

ℝ → ennreal

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

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

@[simp]

theorem ennreal.of_real_to_real {a : ennreal} :

a ≠ ⊤ → ennreal.of_real a.to_real = a

@[simp]

theorem ennreal.to_real_of_real {r : ℝ} :

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

↑(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 : ennreal} :

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

ennreal.of_real a.to_real ≤ a

theorem ennreal.forall_ennreal {p : ennreal → Prop} :

(∀ (a : ennreal), p a) ↔ (∀ (r : ℝ≥0), p ↑r) ∧ p ⊤

theorem ennreal.forall_ne_top {p : ennreal → Prop} :

(∀ (a : ennreal), a ≠ ⊤ → p a) ↔ ∀ (r : ℝ≥0), p ↑r

theorem ennreal.exists_ne_top {p : ennreal → Prop} :

(∃ (a : ennreal) (H : a ≠ ⊤), p a) ↔ ∃ (r : ℝ≥0), p ↑r

theorem ennreal.to_nnreal_eq_zero_iff (x : ennreal) :

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

theorem ennreal.to_real_eq_zero_iff (x : ennreal) :

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 : ennreal | a ≠ ⊤} ≃ ℝ≥0

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

Equations

ennreal.ne_top_equiv_nnreal = {to_fun := λ (x : ↥{a : ennreal | 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 : ennreal → α) :

(⨅ (x : {x // x ≠ ⊤}), f ↑x) = ⨅ (x : ℝ≥0), f ↑x

theorem ennreal.infi_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal → α) :

(⨅ (x : ennreal) (H : x ≠ ⊤), f x) = ⨅ (x : ℝ≥0), f ↑x

theorem ennreal.csupr_ne_top {α : Type u_1} [has_Sup α] (f : ennreal → α) :

(⨆ (x : {x // x ≠ ⊤}), f ↑x) = ⨆ (x : ℝ≥0), f ↑x

theorem ennreal.supr_ne_top {α : Type u_1} [complete_lattice α] (f : ennreal → α) :

(⨆ (x : ennreal) (H : x ≠ ⊤), f x) = ⨆ (x : ℝ≥0), f ↑x

theorem ennreal.infi_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal → α} :

(⨅ (n : ennreal), f n) = (⨅ (n : ℝ≥0), f ↑n) ⊓ f ⊤

theorem ennreal.supr_ennreal {α : Type u_1} [complete_lattice α] {f : ennreal → α} :

(⨆ (n : ennreal), f n) = (⨆ (n : ℝ≥0), f ↑n) ⊔ f ⊤

@[simp]

theorem ennreal.add_top {a : ennreal} :

@[simp]

theorem ennreal.top_add {a : ennreal} :

def ennreal.of_nnreal_hom :

ℝ≥0 →+* ennreal

Coercion ℝ≥0 → ennreal 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

theorem ennreal.add_eq_top {a b : ennreal} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

theorem ennreal.add_lt_top {a b : ennreal} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

theorem ennreal.to_nnreal_add {r₁ r₂ : ennreal} :

r₁ < ⊤ → r₂ < ⊤ → (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal

theorem ennreal.lt_top_iff_ne_top {a : ennreal} :

a < ⊤ ↔ a ≠ ⊤

theorem ennreal.bot_lt_iff_ne_bot {a : ennreal} :

0 < a ↔ a ≠ 0

theorem ennreal.not_lt_top {x : ennreal} :

¬x < ⊤ ↔ x = ⊤

theorem ennreal.add_ne_top {a b : ennreal} :

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

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

⊤ * ⊤ = ⊤

theorem ennreal.top_pow {n : ℕ} :

0 < n → ⊤ ^ n = ⊤

theorem ennreal.mul_eq_top {a b : ennreal} :

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

theorem ennreal.mul_ne_top {a b : ennreal} :

a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤

theorem ennreal.mul_lt_top {a b : ennreal} :

a < ⊤ → b < ⊤ → a * b < ⊤

theorem ennreal.ne_top_of_mul_ne_top_left {a b : ennreal} :

a * b ≠ ⊤ → b ≠ 0 → a ≠ ⊤

theorem ennreal.ne_top_of_mul_ne_top_right {a b : ennreal} :

a * b ≠ ⊤ → a ≠ 0 → b ≠ ⊤

theorem ennreal.lt_top_of_mul_lt_top_left {a b : ennreal} :

a * b < ⊤ → b ≠ 0 → a < ⊤

theorem ennreal.lt_top_of_mul_lt_top_right {a b : ennreal} :

a * b < ⊤ → a ≠ 0 → b < ⊤

theorem ennreal.mul_lt_top_iff {a b : ennreal} :

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

@[simp]

theorem ennreal.mul_pos {a b : ennreal} :

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

theorem ennreal.pow_eq_top {a : ennreal} (n : ℕ) :

a ^ n = ⊤ → a = ⊤

theorem ennreal.pow_ne_top {a : ennreal} (h : a ≠ ⊤) {n : ℕ} :

theorem ennreal.pow_lt_top {a : ennreal} (a_1 : 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.nat_ne_top (n : ℕ) :

@[simp]

theorem ennreal.top_ne_nat (n : ℕ) :

@[simp]

theorem ennreal.one_lt_top :

theorem ennreal.le_coe_iff {a : ennreal} {r : ℝ≥0} :

a ≤ ↑r ↔ ∃ (p : ℝ≥0), a = ↑p ∧ p ≤ r

theorem ennreal.coe_le_iff {a : ennreal} {r : ℝ≥0} :

↑r ≤ a ↔ ∀ (p : ℝ≥0), a = ↑p → r ≤ p

theorem ennreal.lt_iff_exists_coe {a b : ennreal} :

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

theorem ennreal.pow_le_pow {a : ennreal} {n m : ℕ} :

1 ≤ a → n ≤ m → a ^ n ≤ a ^ m

@[simp]

theorem ennreal.max_eq_zero_iff {a b : ennreal} :

max a b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem ennreal.max_zero_left {a : ennreal} :

max 0 a = a

@[simp]

theorem ennreal.max_zero_right {a : ennreal} :

max a 0 = a

@[simp]

theorem ennreal.sup_eq_max {a b : ennreal} :

a ⊔ b = max a b

theorem ennreal.pow_pos {a : ennreal} (a_1 : 0 < a) (n : ℕ) :

0 < a ^ n

theorem ennreal.pow_ne_zero {a : ennreal} (a_1 : a ≠ 0) (n : ℕ) :

a ^ n ≠ 0

@[simp]

theorem ennreal.not_lt_zero {a : ennreal} :

¬a < 0

theorem ennreal.add_lt_add_iff_left {a b c : ennreal} :

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

theorem ennreal.add_lt_add_iff_right {a b c : ennreal} :

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

theorem ennreal.lt_add_right {a b : ennreal} :

a < ⊤ → 0 < b → a < a + b

theorem ennreal.le_of_forall_epsilon_le {a b : ennreal} :

(∀ (ε : ℝ≥0), 0 < ε → b < ⊤ → a ≤ b + ↑ε) → a ≤ b

theorem ennreal.lt_iff_exists_rat_btwn {a b : ennreal} :

a < b ↔ ∃ (q : ℚ), 0 ≤ q ∧ a < ↑(nnreal.of_real ↑q) ∧ ↑(nnreal.of_real ↑q) < b

theorem ennreal.lt_iff_exists_real_btwn {a b : ennreal} :

a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ennreal.of_real r ∧ ennreal.of_real r < b

theorem ennreal.lt_iff_exists_nnreal_btwn {a b : ennreal} :

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

theorem ennreal.lt_iff_exists_add_pos_lt {a b : ennreal} :

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

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

theorem ennreal.coe_nat_le_coe_nat {m n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

@[instance]

def ennreal.char_zero :

char_zero ennreal

theorem ennreal.exists_nat_gt {r : ennreal} :

r ≠ ⊤ → (∃ (n : ℕ), r < ↑n)

theorem ennreal.add_lt_add {a b c d : ennreal} :

a < c → 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.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 ennreal} :

⊤ ∈ 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 : ennreal} :

a ≤ b → c ≤ d → a * c ≤ b * d

theorem ennreal.mul_left_mono {a : ennreal} :

monotone (has_mul.mul a)

theorem ennreal.mul_right_mono {a : ennreal} :

monotone (λ (x : ennreal), x * a)

theorem ennreal.max_mul {a b c : ennreal} :

(max a b) * c = max (a * c) (b * c)

theorem ennreal.mul_max {a b c : ennreal} :

a * max b c = max (a * b) (a * c)

theorem ennreal.mul_eq_mul_left {a b c : ennreal} :

a ≠ 0 → 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} :

a ≠ 0 → 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} :

a ≠ 0 → 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)

@[instance]

def ennreal.has_sub :

has_sub ennreal

Equations

ennreal.has_sub = {sub := λ (a b : ennreal), Inf {d : ennreal | 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 : ennreal} :

a ≤ b → a - b = 0

@[simp]

theorem ennreal.sub_self {a : ennreal} :

a - a = 0

@[simp]

theorem ennreal.zero_sub {a : ennreal} :

0 - a = 0

@[simp]

theorem ennreal.sub_infty {a : ennreal} :

a - ⊤ = 0

theorem ennreal.sub_le_sub {a b c d : ennreal} :

a ≤ b → d ≤ c → a - c ≤ b - d

@[simp]

theorem ennreal.add_sub_self {a b : ennreal} :

b < ⊤ → a + b - b = a

@[simp]

theorem ennreal.add_sub_self' {a b : ennreal} :

a < ⊤ → a + b - a = b

theorem ennreal.add_right_inj {a b c : ennreal} :

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

theorem ennreal.add_left_inj {a b c : ennreal} :

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

@[simp]

theorem ennreal.sub_add_cancel_of_le {a b : ennreal} :

b ≤ a → a - b + b = a

@[simp]

theorem ennreal.add_sub_cancel_of_le {a b : ennreal} :

b ≤ a → b + (a - b) = a

theorem ennreal.sub_add_self_eq_max {a b : ennreal} :

a - b + b = max a b

theorem ennreal.le_sub_add_self {a b : ennreal} :

a ≤ a - b + b

@[simp]

theorem ennreal.sub_le_iff_le_add {a b c : ennreal} :

a - b ≤ c ↔ a ≤ c + b

theorem ennreal.sub_le_iff_le_add' {a b c : ennreal} :

a - b ≤ c ↔ a ≤ b + c

theorem ennreal.sub_eq_of_add_eq {a b c : ennreal} :

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

theorem ennreal.sub_le_of_sub_le {a b c : ennreal} :

a - b ≤ c → a - c ≤ b

theorem ennreal.sub_lt_sub_self {a b : ennreal} :

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

@[simp]

theorem ennreal.sub_eq_zero_iff_le {a b : ennreal} :

a - b = 0 ↔ a ≤ b

@[simp]

theorem ennreal.zero_lt_sub_iff_lt {a b : ennreal} :

0 < a - b ↔ b < a

theorem ennreal.lt_sub_iff_add_lt {a b c : ennreal} :

a < b - c ↔ a + c < b

theorem ennreal.sub_le_self (a b : ennreal) :

a - b ≤ a

@[simp]

theorem ennreal.sub_zero {a : ennreal} :

a - 0 = a

theorem ennreal.sub_le_sub_add_sub {a b c : ennreal} :

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

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

theorem ennreal.sub_sub_cancel {a b : ennreal} :

a < ⊤ → b ≤ a → a - (a - b) = b

theorem ennreal.sub_right_inj {a b c : ennreal} :

a < ⊤ → b ≤ a → c ≤ a → (a - b = a - c ↔ b = c)

theorem ennreal.sub_mul {a b c : ennreal} :

(0 < b → b < a → c ≠ ⊤) → (a - b) * c = a * c - b * c

theorem ennreal.mul_sub {a b c : ennreal} :

(0 < c → c < b → a ≠ ⊤) → a * (b - c) = a * b - a * c

theorem ennreal.sub_mul_ge {a b c : ennreal} :

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

theorem ennreal.sum_lt_top {α : Type u_1} {s : finset α} {f : α → ennreal} :

(∀ (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 : α → ennreal} :

∑ (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 : α → ennreal} :

∑ (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 : α → ennreal} :

(∀ (a : α), a ∈ s → f a < ⊤) → (∑ (a : α) in s, f a).to_nnreal = ∑ (a : α) in s, (f a).to_nnreal

seeing ennreal as nnreal does not change their sum, unless one of the ennreal is infinity

theorem ennreal.to_real_sum {α : Type u_1} {s : finset α} {f : α → ennreal} :

(∀ (a : α), a ∈ s → f a < ⊤) → (∑ (a : α) in s, f a).to_real = ∑ (a : α) in s, (f a).to_real

seeing ennreal as real does not change their sum, unless one of the ennreal is infinity

theorem ennreal.Ico_eq_Iio {y : ennreal} :

set.Ico 0 y = set.Iio y

theorem ennreal.mem_Iio_self_add {x ε : ennreal} :

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

theorem ennreal.not_mem_Ioo_self_sub {x y ε : ennreal} :

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

theorem ennreal.mem_Ioo_self_sub_add {x ε₁ ε₂ : ennreal} :

x ≠ ⊤ → x ≠ 0 → 0 < ε₁ → 0 < ε₂ → x ∈ set.Ioo (x - ε₁) (x + ε₂)

@[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_eq_top_iff {a : ennreal} :

bit0 a = ⊤ ↔ a = ⊤

@[simp]

theorem ennreal.bit1_inj {a b : ennreal} :

bit1 a = bit1 b ↔ a = b

@[simp]

theorem ennreal.bit1_ne_zero {a : ennreal} :

@[simp]

theorem ennreal.bit1_eq_one_iff {a : ennreal} :

bit1 a = 1 ↔ a = 0

@[simp]

theorem ennreal.bit1_eq_top_iff {a : ennreal} :

bit1 a = ⊤ ↔ a = ⊤

@[instance]

def ennreal.has_inv :

has_inv ennreal

Equations

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

@[instance]

def ennreal.has_div :

has_div ennreal

Equations

ennreal.has_div = {div := λ (a b : ennreal), a * b⁻¹}

theorem ennreal.div_def {a b : ennreal} :

a / b = a * b⁻¹

theorem ennreal.mul_div_assoc {a b c : ennreal} :

a * b / c = a * (b / c)

@[simp]

theorem ennreal.inv_zero :

@[simp]

theorem ennreal.inv_top :

@[simp]

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

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

r ≠ 0 → ↑(p / r) = ↑p / ↑r

@[simp]

theorem ennreal.inv_one :

@[simp]

theorem ennreal.div_one {a : ennreal} :

a / 1 = a

theorem ennreal.inv_pow {a : ennreal} {n : ℕ} :

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

@[simp]

theorem ennreal.inv_inv {a : ennreal} :

a⁻¹ ⁻¹ = a

theorem ennreal.inv_involutive :

function.involutive (λ (a : ennreal), a⁻¹)

theorem ennreal.inv_bijective :

function.bijective (λ (a : ennreal), a⁻¹)

@[simp]

theorem ennreal.inv_eq_inv {a b : ennreal} :

a⁻¹ = b⁻¹ ↔ a = b

@[simp]

theorem ennreal.inv_eq_top {a : ennreal} :

a⁻¹ = ⊤ ↔ a = 0

theorem ennreal.inv_ne_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} :

x < ⊤ → 0 < y → x / y < ⊤

@[simp]

theorem ennreal.inv_eq_zero {a : ennreal} :

a⁻¹ = 0 ↔ a = ⊤

theorem ennreal.inv_ne_zero {a : ennreal} :

a⁻¹ ≠ 0 ↔ a ≠ ⊤

@[simp]

theorem ennreal.inv_pos {a : ennreal} :

0 < a⁻¹ ↔ a ≠ ⊤

@[simp]

theorem ennreal.inv_lt_inv {a b : ennreal} :

a⁻¹ < b⁻¹ ↔ b < a

theorem ennreal.inv_lt_iff_inv_lt {a b : ennreal} :

a⁻¹ < b ↔ b⁻¹ < a

theorem ennreal.lt_inv_iff_lt_inv {a b : ennreal} :

a < b⁻¹ ↔ b < a⁻¹

@[simp]

theorem ennreal.inv_le_inv {a b : ennreal} :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem ennreal.inv_le_iff_inv_le {a b : ennreal} :

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem ennreal.le_inv_iff_le_inv {a b : ennreal} :

a ≤ b⁻¹ ↔ b ≤ a⁻¹

@[simp]

theorem ennreal.inv_lt_one {a : ennreal} :

a⁻¹ < 1 ↔ 1 < a

@[simp]

theorem ennreal.div_top {a : ennreal} :

a / ⊤ = 0

@[simp]

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

⊤ / ↑p = ⊤

theorem ennreal.top_div_of_ne_top {a : ennreal} :

a ≠ ⊤ → ⊤ / a = ⊤

theorem ennreal.top_div_of_lt_top {a : ennreal} :

a < ⊤ → ⊤ / a = ⊤

theorem ennreal.top_div {a : ennreal} :

⊤ / a = ite (a = ⊤) 0 ⊤

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

theorem ennreal.le_div_iff_mul_le {a b c : ennreal} :

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

theorem ennreal.div_le_iff_le_mul {a b c : ennreal} :

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

theorem ennreal.div_le_of_le_mul {a b c : ennreal} :

a ≤ b * c → a / c ≤ b

theorem ennreal.div_lt_iff {a b c : ennreal} :

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

theorem ennreal.mul_lt_of_lt_div {a b c : ennreal} :

a < b / c → a * c < b

theorem ennreal.inv_le_iff_le_mul {a b : ennreal} :

(b = ⊤ → a ≠ 0) → (a = ⊤ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b)

@[simp]

theorem ennreal.le_inv_iff_mul_le {a b : ennreal} :

a ≤ b⁻¹ ↔ a * b ≤ 1

theorem ennreal.mul_inv_cancel {a : ennreal} :

a ≠ 0 → a ≠ ⊤ → a * a⁻¹ = 1

theorem ennreal.inv_mul_cancel {a : ennreal} :

a ≠ 0 → a ≠ ⊤ → a⁻¹ * a = 1

theorem ennreal.mul_le_iff_le_inv {a b r : ennreal} :

r ≠ 0 → r ≠ ⊤ → (r * a ≤ b ↔ a ≤ r⁻¹ * b)

theorem ennreal.le_of_forall_lt_one_mul_lt {x y : ennreal} :

(∀ (a : ennreal), a < 1 → a * x ≤ y) → x ≤ y

theorem ennreal.div_add_div_same {a b c : ennreal} :

a / c + b / c = (a + b) / c

theorem ennreal.div_self {a : ennreal} :

a ≠ 0 → a ≠ ⊤ → a / a = 1

theorem ennreal.mul_div_cancel {a b : ennreal} :

a ≠ 0 → a ≠ ⊤ → (b / a) * a = b

theorem ennreal.mul_div_cancel' {a b : ennreal} :

a ≠ 0 → a ≠ ⊤ → a * (b / a) = b

theorem ennreal.inv_two_add_inv_two :

2⁻¹ + 2⁻¹ = 1

theorem ennreal.add_halves (a : ennreal) :

a / 2 + a / 2 = 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 ≠ ⊤

theorem ennreal.half_pos {a : ennreal} :

0 < a → 0 < a / 2

theorem ennreal.one_half_lt_one :

theorem ennreal.half_lt_self {a : ennreal} :

a ≠ 0 → a ≠ ⊤ → a / 2 < a

theorem ennreal.sub_half {a : ennreal} :

a ≠ ⊤ → a - a / 2 = a / 2

theorem ennreal.one_sub_inv_two :

1 - 2⁻¹ = 2⁻¹

theorem ennreal.exists_inv_nat_lt {a : ennreal} :

a ≠ 0 → (∃ (n : ℕ), (↑n)⁻¹ < a)

theorem ennreal.exists_nat_mul_gt {a b : ennreal} :

a ≠ 0 → b ≠ ⊤ → (∃ (n : ℕ), b < (↑n) * a)

theorem ennreal.to_real_add {a b : ennreal} :

a ≠ ⊤ → b ≠ ⊤ → (a + b).to_real = a.to_real + b.to_real

theorem ennreal.to_real_add_le {a b : ennreal} :

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

theorem ennreal.of_real_add {p q : ℝ} :

0 ≤ p → 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 : ennreal} :

a ≠ ⊤ → b ≠ ⊤ → (a.to_real ≤ b.to_real ↔ a ≤ b)

@[simp]

theorem ennreal.to_real_lt_to_real {a b : ennreal} :

a ≠ ⊤ → b ≠ ⊤ → (a.to_real < b.to_real ↔ a < b)

theorem ennreal.to_real_max {a b : ennreal} :

a ≠ ⊤ → b ≠ ⊤ → (max a b).to_real = max a.to_real b.to_real

theorem ennreal.to_nnreal_pos_iff {a : ennreal} :

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

theorem ennreal.to_real_pos_iff {a : ennreal} :

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

theorem ennreal.of_real_le_of_real {p q : ℝ} :

p ≤ q → ennreal.of_real p ≤ ennreal.of_real q

theorem ennreal.of_real_le_of_le_to_real {a : ℝ} {b : ennreal} :

a ≤ b.to_real → ennreal.of_real a ≤ b

@[simp]

theorem ennreal.of_real_le_of_real_iff {p q : ℝ} :

0 ≤ q → (ennreal.of_real p ≤ ennreal.of_real q ↔ p ≤ q)

@[simp]

theorem ennreal.of_real_lt_of_real_iff {p q : ℝ} :

0 < q → (ennreal.of_real p < ennreal.of_real q ↔ p < q)

theorem ennreal.of_real_lt_of_real_iff_of_nonneg {p q : ℝ} :

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

b ≠ ⊤ → (ennreal.of_real a ≤ b ↔ a ≤ b.to_real)

theorem ennreal.of_real_lt_iff_lt_to_real {a : ℝ} {b : ennreal} :

0 ≤ a → b ≠ ⊤ → (ennreal.of_real a < b ↔ a < b.to_real)

theorem ennreal.le_of_real_iff_to_real_le {a : ennreal} {b : ℝ} :

a ≠ ⊤ → 0 ≤ b → (a ≤ ennreal.of_real b ↔ a.to_real ≤ b)

theorem ennreal.to_real_le_of_le_of_real {a : ennreal} {b : ℝ} :

0 ≤ b → a ≤ ennreal.of_real b → a.to_real ≤ b

theorem ennreal.lt_of_real_iff_to_real_lt {a : ennreal} {b : ℝ} :

a ≠ ⊤ → (a < ennreal.of_real b ↔ a.to_real < b)

theorem ennreal.of_real_mul {p q : ℝ} :

0 ≤ p → ennreal.of_real (p * q) = (ennreal.of_real p) * ennreal.of_real q

theorem ennreal.to_real_of_real_mul (c : ℝ) (a : ennreal) :

0 ≤ c → ((ennreal.of_real c) * a).to_real = c * a.to_real

@[simp]

theorem ennreal.to_real_mul_top (a : ennreal) :

(a * ⊤).to_real = 0

@[simp]

theorem ennreal.to_real_top_mul (a : ennreal) :

(⊤ * a).to_real = 0

theorem ennreal.to_real_eq_to_real {a b : ennreal} :

a < ⊤ → b < ⊤ → (a.to_real = b.to_real ↔ a = b)

theorem ennreal.to_real_mul_to_real {a b : ennreal} :

(a.to_real) * b.to_real = (a * b).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} :

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

(∀ (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 ι] :

(∀ (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 : ι → ennreal} {x : ennreal} :

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

theorem ennreal.mul_infi {ι : Sort u_1} [nonempty ι] {f : ι → ennreal} {x : ennreal} :

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

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

theorem ennreal.supr_coe_nat :

(⨆ (n : ℕ), ↑n) = ⊤

theorem ennreal.le_of_add_le_add_left {a b c : ennreal} :

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 ennreal with the additional assumption that a < ∞.