Documentation

Mathlib.Data.ENNReal.Operations

Properties of addition, multiplication and subtraction on extended non-negative real numbers #

In this file we prove elementary properties of algebraic operations on ℝ≥0∞, including addition, multiplication, natural powers and truncated subtraction, as well as how these interact with the order structure on ℝ≥0∞. Notably excluded from this list are inversion and division, the definitions and properties of which can be found in Data.ENNReal.Inv.

Note: the definitions of the operations included in this file can be found in Data.ENNReal.Basic.

theorem ENNReal.mul_lt_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :

a * b < c * d

theorem ENNReal.mul_left_mono {a : ENNReal} :

Monotone fun (x : ENNReal) => a * x

theorem ENNReal.mul_right_mono {a : ENNReal} :

Monotone fun (x : ENNReal) => x * a

theorem ENNReal.pow_strictMono {n : ℕ} :

n ≠ 0 → StrictMono fun (x : ENNReal) => x ^ n

theorem ENNReal.pow_lt_pow_left {a : ENNReal} {b : ENNReal} (h : a < b) {n : ℕ} (hn : n ≠ 0) :

a ^ n < b ^ n

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

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

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

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

theorem ENNReal.mul_left_strictMono {a : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

StrictMono fun (x : ENNReal) => a * x

theorem ENNReal.mul_lt_mul_left' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :

a * b < a * c

theorem ENNReal.mul_lt_mul_right' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :

b * a < c * a

theorem ENNReal.mul_eq_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b = a * c ↔ b = c

theorem ENNReal.mul_eq_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

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

theorem ENNReal.mul_le_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b ≤ a * c ↔ b ≤ c

theorem ENNReal.mul_le_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

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

theorem ENNReal.mul_lt_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b < a * c ↔ b < c

theorem ENNReal.mul_lt_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

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

theorem ENNReal.pow_pos {a : ENNReal} :

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

theorem ENNReal.pow_ne_zero {a : ENNReal} :

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

theorem ENNReal.not_lt_zero {a : ENNReal} :

¬a < 0

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

a ≠ ⊤ → a + b ≤ a + c → b ≤ c

theorem ENNReal.le_of_add_le_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b + a ≤ c + a → b ≤ c

theorem ENNReal.add_lt_add_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b < c → a + b < a + c

theorem ENNReal.add_lt_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b < c → b + a < c + a

theorem ENNReal.add_le_add_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)

theorem ENNReal.add_le_add_iff_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)

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

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

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

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

theorem ENNReal.add_lt_add_of_le_of_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :

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

theorem ENNReal.add_lt_add_of_lt_of_le {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :

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

instance ENNReal.contravariantClass_add_lt :

ContravariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x < x_1

Equations

ENNReal.contravariantClass_add_lt = ⋯

theorem ENNReal.lt_add_right {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) :

a < a + b

@[simp]

theorem ENNReal.add_eq_top {a : ENNReal} {b : ENNReal} :

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

@[simp]

theorem ENNReal.add_lt_top {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.toNNReal_add {r₁ : ENNReal} {r₂ : ENNReal} (h₁ : r₁ ≠ ⊤) (h₂ : r₂ ≠ ⊤) :

(r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

theorem ENNReal.not_lt_top {x : ENNReal} :

¬x < ⊤ ↔ x = ⊤

theorem ENNReal.add_ne_top {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.mul_top' {a : ENNReal} :

a * ⊤ = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.mul_top {a : ENNReal} (h : a ≠ 0) :

theorem ENNReal.top_mul' {a : ENNReal} :

⊤ * a = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.top_mul {a : ENNReal} (h : a ≠ 0) :

theorem ENNReal.top_mul_top :

⊤ * ⊤ = ⊤

theorem ENNReal.top_pow {n : ℕ} (h : 0 < n) :

theorem ENNReal.mul_eq_top {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.mul_lt_top {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.mul_ne_top {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.lt_top_of_mul_ne_top_left {a : ENNReal} {b : ENNReal} (h : a * b ≠ ⊤) (hb : b ≠ 0) :

theorem ENNReal.lt_top_of_mul_ne_top_right {a : ENNReal} {b : ENNReal} (h : a * b ≠ ⊤) (ha : a ≠ 0) :

theorem ENNReal.mul_lt_top_iff {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.mul_self_lt_top_iff {a : ENNReal} :

a * a < ⊤ ↔ a < ⊤

theorem ENNReal.mul_pos_iff {a : ENNReal} {b : ENNReal} :

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

theorem ENNReal.mul_pos {a : ENNReal} {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 = ⊤) :

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

theorem ENNReal.pow_lt_top {a : ENNReal} :

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

@[simp]

theorem ENNReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : α → NNReal} :

↑(Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ↑(f a)

@[simp]

theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : α → NNReal} :

↑(Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => ↑(f a)

theorem ENNReal.add_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :

a + b < c + d

theorem ENNReal.addLECancellable_iff_ne {a : ENNReal} :

AddLECancellable a ↔ a ≠ ⊤

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

theorem ENNReal.cancel_of_ne {a : ENNReal} (h : a ≠ ⊤) :

AddLECancellable a

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

theorem ENNReal.cancel_of_lt {a : ENNReal} (h : a < ⊤) :

AddLECancellable a

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

theorem ENNReal.cancel_of_lt' {a : ENNReal} {b : ENNReal} (h : a < b) :

AddLECancellable a

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

theorem ENNReal.cancel_coe {a : NNReal} :

AddLECancellable ↑a

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

theorem ENNReal.add_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤) :

a + b = a + c ↔ b = c

theorem ENNReal.add_left_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤) :

b + a = c + a ↔ b = c

theorem ENNReal.sub_eq_sInf {a : ENNReal} {b : ENNReal} :

a - b = sInf {d : ENNReal | a ≤ d + b}

@[simp]

theorem ENNReal.coe_sub {r : NNReal} {p : NNReal} :

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

This is a special case of WithTop.coe_sub in the ENNReal namespace

@[simp]

theorem ENNReal.top_sub_coe {r : NNReal} :

⊤ - ↑r = ⊤

This is a special case of WithTop.top_sub_coe in the ENNReal namespace

theorem ENNReal.sub_top {a : ENNReal} :

a - ⊤ = 0

This is a special case of WithTop.sub_top in the ENNReal namespace

@[simp]

theorem ENNReal.sub_eq_top_iff {a : ENNReal} {b : ENNReal} :

a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.sub_ne_top {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

@[simp]

theorem ENNReal.nat_cast_sub (m : ℕ) (n : ℕ) :

↑(m - n) = ↑m - ↑n

theorem ENNReal.sub_eq_of_eq_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a = c + b → a - b = c

theorem ENNReal.eq_sub_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hc : c ≠ ⊤) :

a + c = b → a = b - c

theorem ENNReal.sub_eq_of_eq_add_rev {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a = b + c → a - b = c

theorem ENNReal.sub_eq_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) (hc : a + b = c) :

c - b = a

@[simp]

theorem ENNReal.add_sub_cancel_left {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

a + b - a = b

@[simp]

theorem ENNReal.add_sub_cancel_right {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) :

a + b - b = a

theorem ENNReal.lt_add_of_sub_lt_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤ ∨ b ≠ ⊤) :

a - b < c → a < b + c

theorem ENNReal.lt_add_of_sub_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤ ∨ c ≠ ⊤) :

a - c < b → a < b + c

theorem ENNReal.le_sub_of_add_le_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ≠ ⊤) :

a + b ≤ c → b ≤ c - a

theorem ENNReal.le_sub_of_add_le_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a + b ≤ c → a ≤ c - b

theorem ENNReal.sub_lt_of_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hac : c ≤ a) (h : a < b + c) :

a - c < b

theorem ENNReal.sub_lt_iff_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) (hab : b ≤ a) :

a - b < c ↔ a < c + b

theorem ENNReal.sub_lt_self {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (ha₀ : a ≠ 0) (hb : b ≠ 0) :

a - b < a

theorem ENNReal.sub_lt_self_iff {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

a - b < a ↔ 0 < a ∧ 0 < b

theorem ENNReal.sub_lt_of_sub_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} (h₂ : c ≤ a) (h₃ : a ≠ ⊤ ∨ b ≠ ⊤) (h₁ : a - b < c) :

a - c < b

theorem ENNReal.sub_sub_cancel {a : ENNReal} {b : ENNReal} (h : a ≠ ⊤) (h2 : b ≤ a) :

a - (a - b) = b

theorem ENNReal.sub_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ≠ ⊤) (hb : b ≤ a) (hc : c ≤ a) :

a - b = a - c ↔ b = c

theorem ENNReal.sub_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < b → b < a → c ≠ ⊤) :

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

theorem ENNReal.mul_sub {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < c → c < b → a ≠ ⊤) :

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

theorem ENNReal.sub_le_sub_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : c ≤ a) (h' : a ≠ ⊤) :

a - b ≤ a - c ↔ c ≤ b

theorem ENNReal.prod_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a ≠ ⊤) :

(Finset.prod s fun (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 ∈ s, f a ≠ ⊤) :

(Finset.sum s fun (a : α) => f a) < ⊤

A sum of finite numbers is still finite

theorem ENNReal.sum_lt_top_iff {α : Type u_1} {s : Finset α} {f : α → ENNReal} :

(Finset.sum s fun (a : α) => f 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} :

(Finset.sum s fun (x : α) => f x) = ⊤ ↔ ∃ 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 : (Finset.sum s fun (x : α) => f x) ≠ ⊤) {a : α} (ha : a ∈ s) :

f a < ⊤

theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :

(Finset.sum s fun (a : α) => f a).toNNReal = Finset.sum s fun (a : α) => (f a).toNNReal

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

theorem ENNReal.toReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :

(Finset.sum s fun (a : α) => f a).toReal = Finset.sum s fun (a : α) => (f a).toReal

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

theorem ENNReal.ofReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

ENNReal.ofReal (Finset.sum s fun (i : α) => f i) = Finset.sum s fun (i : α) => ENNReal.ofReal (f i)

theorem ENNReal.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f : α → ENNReal} {g : α → ENNReal} (Hlt : ∀ i ∈ s, f i < g i) :

(Finset.sum s fun (i : α) => f i) < Finset.sum s fun (i : α) => g i

theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f : α → ENNReal} {g : α → ENNReal} (Hle : (Finset.sum s fun (i : α) => f i) ≤ Finset.sum s fun (i : α) => g i) :

∃ i ∈ s, f i ≤ g i

theorem ENNReal.Ico_eq_Iio {y : ENNReal} :

Set.Ico 0 y = Set.Iio y

theorem ENNReal.mem_Iio_self_add {x : ENNReal} {ε : ENNReal} :

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

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

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

noncomputable instance ENNReal.instMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_1} [MulAction ENNReal M] :

MulAction NNReal M

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

Equations

ENNReal.instMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = MulAction.compHom M ↑ENNReal.ofNNRealHom

theorem ENNReal.smul_def {M : Type u_1} [MulAction ENNReal M] (c : NNReal) (x : M) :

c • x = ↑c • x

instance ENNReal.instIsScalarTowerNNRealToSMulToMonoidToMonoidWithZeroInstNNRealSemiringInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiringToSMulInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_1} {N : Type u_2} [MulAction ENNReal M] [MulAction ENNReal N] [SMul M N] [IsScalarTower ENNReal M N] :

IsScalarTower NNReal M N

Equations

⋯ = ⋯

instance ENNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass ENNReal M N] :

SMulCommClass NNReal M N

Equations

⋯ = ⋯

instance ENNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction ENNReal N] [SMul M N] [SMulCommClass M ENNReal N] :

SMulCommClass M NNReal N

Equations

⋯ = ⋯

noncomputable instance ENNReal.instDistribMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_1} [AddMonoid M] [DistribMulAction ENNReal M] :

DistribMulAction NNReal M

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

Equations

ENNReal.instDistribMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = DistribMulAction.compHom M ↑ENNReal.ofNNRealHom

noncomputable instance ENNReal.instModuleNNRealInstNNRealSemiring {M : Type u_1} [AddCommMonoid M] [Module ENNReal M] :

Module NNReal M

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

Equations

ENNReal.instModuleNNRealInstNNRealSemiring = Module.compHom M ENNReal.ofNNRealHom

noncomputable instance ENNReal.instAlgebraNNRealInstNNRealCommSemiring {A : Type u_1} [Semiring A] [Algebra ENNReal A] :

Algebra NNReal A

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

Equations

ENNReal.instAlgebraNNRealInstNNRealCommSemiring = Algebra.mk (RingHom.comp (algebraMap ENNReal A) ENNReal.ofNNRealHom) ⋯ ⋯

theorem ENNReal.coe_smul {R : Type u_1} (r : R) (s : NNReal) [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal NNReal] [IsScalarTower R NNReal ENNReal] :

↑(r • s) = r • ↑s

theorem ENNReal.smul_top {R : Type u_1} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] [DecidableEq R] (c : R) :

c • ⊤ = if c = 0 then 0 else ⊤