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 Mathlib.Data.ENNReal.Inv.

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

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

@[deprecated mul_left_mono (since := "2024-10-15")]

theorem ENNReal.mul_left_mono {a : ENNReal} : Monotone fun (x : ENNReal) => a * x

@[deprecated mul_right_mono (since := "2024-10-15")]

theorem ENNReal.mul_right_mono {a : ENNReal} : Monotone fun (x : ENNReal) => x * a

theorem ENNReal.pow_right_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (a : ENNReal) => a ^ n

@[deprecated ENNReal.pow_right_strictMono (since := "2024-10-15")]

theorem ENNReal.pow_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (a : ENNReal) => a ^ n

Alias of ENNReal.pow_right_strictMono.

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

@[deprecated max_mul (since := "2024-10-15")]

theorem ENNReal.max_mul {a b c : ENNReal} : (a ⊔ b) * c = a * c ⊔ b * c

@[deprecated mul_max (since := "2024-10-15")]

theorem ENNReal.mul_max {a b c : ENNReal} : a * (b ⊔ c) = 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 b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) : a * b < a * c

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

theorem ENNReal.mul_right_inj {a b c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) : a * b = a * c ↔ b = c

@[deprecated ENNReal.mul_right_inj (since := "2025-01-20")]

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

Alias of ENNReal.mul_right_inj.

theorem ENNReal.mul_left_inj {a b c : ENNReal} (h0 : c ≠ 0) (hinf : c ≠ ⊤) : a * c = b * c ↔ a = b

@[deprecated ENNReal.mul_left_inj (since := "2025-01-20")]

theorem ENNReal.mul_eq_mul_right {a b c : ENNReal} (h0 : c ≠ 0) (hinf : c ≠ ⊤) : a * c = b * c ↔ a = b

Alias of ENNReal.mul_left_inj.

theorem ENNReal.mul_le_mul_left {a b c : ENNReal} (h0 : 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} (h0 : 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)

theorem ENNReal.mul_eq_left {a b : ENNReal} (ha₀ : a ≠ 0) (ha : a ≠ ⊤) : a * b = a ↔ b = 1

theorem ENNReal.mul_eq_right {a b : ENNReal} (hb₀ : b ≠ 0) (hb : b ≠ ⊤) : a * b = b ↔ a = 1

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 b c : ENNReal} : a ≠ ⊤ → a + b ≤ a + c → b ≤ c

theorem ENNReal.le_of_add_le_add_right {a b c : ENNReal} : a ≠ ⊤ → b + a ≤ c + a → b ≤ c

theorem ENNReal.add_lt_add_left {a b c : ENNReal} : a ≠ ⊤ → b < c → a + b < a + c

theorem ENNReal.add_lt_add_right {a b c : ENNReal} : a ≠ ⊤ → b < c → b + a < c + a

theorem ENNReal.add_le_add_iff_left {a b c : ENNReal} : a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)

theorem ENNReal.add_le_add_iff_right {a b c : ENNReal} : a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)

theorem ENNReal.add_lt_add_iff_left {a b c : ENNReal} : a ≠ ⊤ → (a + b < a + c ↔ b < c)

theorem ENNReal.add_lt_add_iff_right {a b c : ENNReal} : a ≠ ⊤ → (b + a < c + a ↔ b < c)

theorem ENNReal.add_lt_add_of_le_of_lt {a b c d : ENNReal} : a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

theorem ENNReal.add_lt_add_of_lt_of_le {a b c d : ENNReal} : c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

instance ENNReal.addLeftReflectLT : AddLeftReflectLT ENNReal

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

@[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.toNNReal_add {r₁ r₂ : ENNReal} (h₁ : r₁ ≠ ⊤) (h₂ : r₂ ≠ ⊤) : (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

theorem ENNReal.toReal_le_add' {a b c : ENNReal} (hle : a ≤ b + c) (hb : b = ⊤ → a = ⊤) (hc : c = ⊤ → a = ⊤) : a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c and a = ∞ whenever b = ∞ or c = ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.toReal_le_add {a b c : ENNReal} (hle : a ≤ b + c) (hb : b ≠ ⊤) (hc : c ≠ ⊤) : a.toReal ≤ b.toReal + c.toReal

If a ≤ b + c, b ≠ ∞, and c ≠ ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.not_lt_top {x : ENNReal} : ¬x < ⊤ ↔ x = ⊤

theorem ENNReal.add_ne_top {a b : ENNReal} : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

theorem ENNReal.Finiteness.add_ne_top {a b : ENNReal} (ha : a ≠ ⊤) (hb : 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) : a * ⊤ = ⊤

theorem ENNReal.top_mul' {a : ENNReal} : ⊤ * a = if a = 0 then 0 else ⊤

@[simp]

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

theorem ENNReal.top_mul_top : ⊤ * ⊤ = ⊤

theorem ENNReal.top_pow {n : ℕ} (n_pos : 0 < n) : ⊤ ^ 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} : a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤

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_self_lt_top_iff {a : ENNReal} : a * a < ⊤ ↔ a < ⊤

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

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

@[simp]

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 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 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_sInf {a b : ENNReal} : a - b = sInf {d : ENNReal | a ≤ d + b}

@[simp]

theorem ENNReal.coe_sub {r 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

@[simp]

theorem ENNReal.top_sub {a : ENNReal} (ha : a ≠ ⊤) : ⊤ - a = ⊤

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 b : ENNReal} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.sub_ne_top_iff {a b : ENNReal} : a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

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

@[simp]

theorem ENNReal.natCast_sub (m n : ℕ) : ↑(m - n) = ↑m - ↑n

theorem ENNReal.sub_eq_of_eq_add {a b c : ENNReal} (hb : b ≠ ⊤) : a = c + b → a - b = c

See ENNReal.sub_eq_of_eq_add' for a version assuming that a = c + b itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add' {a b c : ENNReal} (ha : a ≠ ⊤) : a = c + b → a - b = c

Weaker version of ENNReal.sub_eq_of_eq_add assuming that a = c + b itself is finite rather han b.

theorem ENNReal.eq_sub_of_add_eq {a b c : ENNReal} (hc : c ≠ ⊤) : a + c = b → a = b - c

See ENNReal.eq_sub_of_add_eq' for a version assuming that b = a + c itself is finite rather than c.

theorem ENNReal.eq_sub_of_add_eq' {a b c : ENNReal} (hb : b ≠ ⊤) : a + c = b → a = b - c

Weaker version of ENNReal.eq_sub_of_add_eq assuming that b = a + c itself is finite rather than c.

theorem ENNReal.sub_eq_of_eq_add_rev {a b c : ENNReal} (hb : b ≠ ⊤) : a = b + c → a - b = c

See ENNReal.sub_eq_of_eq_add_rev' for a version assuming that a = b + c itself is finite rather than b.

theorem ENNReal.sub_eq_of_eq_add_rev' {a b c : ENNReal} (ha : a ≠ ⊤) : a = b + c → a - b = c

Weaker version of ENNReal.sub_eq_of_eq_add_rev assuming that a = b + c itself is finite rather than b.

@[deprecated ENNReal.sub_eq_of_eq_add (since := "2024-09-30")]

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

@[simp]

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

@[simp]

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

theorem ENNReal.sub_add_eq_add_sub {a b c : ENNReal} (hab : b ≤ a) (b_ne_top : b ≠ ⊤) : a - b + c = a + c - b

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

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

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

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

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

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.sub_le_sub_iff_left {a b c : ENNReal} (h : c ≤ a) (h' : a ≠ ⊤) : a - b ≤ a - c ↔ c ≤ b

theorem ENNReal.le_toReal_sub {a b : ENNReal} (hb : b ≠ ⊤) : a.toReal - b.toReal ≤ (a - b).toReal

@[simp]

theorem ENNReal.toNNReal_sub {a b : ENNReal} (hb : b ≠ ⊤) : (a - b).toNNReal = a.toNNReal - b.toNNReal

@[simp]

theorem ENNReal.toReal_sub_of_le {a b : ENNReal} (hba : b ≤ a) (ha : a ≠ ⊤) : (a - b).toReal = a.toReal - b.toReal

theorem ENNReal.ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

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.mem_Ioo_self_sub_add {x ε₁ ε₂ : ENNReal} : x ≠ ⊤ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Set.Ioo (x - ε₁) (x + ε₂)

@[simp]

theorem ENNReal.image_coe_Iic (x : NNReal) : ofNNReal '' Set.Iic x = Set.Iic ↑x

@[simp]

theorem ENNReal.image_coe_Ici (x : NNReal) : ofNNReal '' Set.Ici x = Set.Ico ↑x ⊤

@[simp]

theorem ENNReal.image_coe_Iio (x : NNReal) : ofNNReal '' Set.Iio x = Set.Iio ↑x

@[simp]

theorem ENNReal.image_coe_Ioi (x : NNReal) : ofNNReal '' Set.Ioi x = Set.Ioo ↑x ⊤

@[simp]

theorem ENNReal.image_coe_Icc (x y : NNReal) : ofNNReal '' Set.Icc x y = Set.Icc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ico (x y : NNReal) : ofNNReal '' Set.Ico x y = Set.Ico ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ioc (x y : NNReal) : ofNNReal '' Set.Ioc x y = Set.Ioc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_Ioo (x y : NNReal) : ofNNReal '' Set.Ioo x y = Set.Ioo ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIcc (x y : NNReal) : ofNNReal '' Set.uIcc x y = Set.uIcc ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIoc (x y : NNReal) : ofNNReal '' Ι x y = Ι ↑x ↑y

@[simp]

theorem ENNReal.image_coe_uIoo (x y : NNReal) : ofNNReal '' Set.uIoo x y = Set.uIoo ↑x ↑y