Documentation

Mathlib.Data.EReal.Operations

Addition, negation, subtraction and multiplication on extended real numbers #

Addition and multiplication in EReal are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties. In particular, it is an order-reversing isomorphism.

The construction of EReal as WithBot (WithTop ℝ) endows a LinearOrderedAddCommMonoid structure on it. However, addition is badly behaved at (⊥, ⊤) and (⊤, ⊥), so this cannot be upgraded to a group structure. Our choice is that ⊥ + ⊤ = ⊤ + ⊥ = ⊥, to make sure that the exponential and logarithm between EReal and ℝ≥0∞ respect the operations. Note that the convention 0 * ∞ = 0 on ℝ≥0∞ is enforced by measure theory. Subtraction, defined as x - y = x + (-y), does not have nice properties but is sometimes convenient to have.

There is also a CommMonoidWithZero structure on EReal, but Mathlib.Data.EReal.Basic only provides MulZeroOneClass because a proof of associativity by hand would have 125 cases. The CommMonoidWithZero instance is instead delivered in Mathlib.Data.EReal.Inv.

We define 0 * x = x * 0 = 0 for any x, with the other cases defined non-ambiguously. This does not distribute with addition, as ⊥ = ⊥ + ⊤ = 1 * ⊥ + (-1) * ⊥ ≠ (1 - 1) * ⊥ = 0 * ⊥ = 0. Distributivity x * (y + z) = x * y + x * z is recovered in the case where either 0 ≤ x < ⊤, see EReal.left_distrib_of_nonneg_of_ne_top, or 0 ≤ y, z. See EReal.left_distrib_of_nonneg (similarly for right distributivity).

Addition #

@[simp]

theorem EReal.add_bot (x : EReal) :

@[simp]

theorem EReal.bot_add (x : EReal) :

@[simp]

theorem EReal.add_eq_bot_iff {x y : EReal} :

x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

theorem EReal.add_ne_bot_iff {x y : EReal} :

x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

@[simp]

theorem EReal.bot_lt_add_iff {x y : EReal} :

⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

@[simp]

theorem EReal.top_add_top :

⊤ + ⊤ = ⊤

@[simp]

theorem EReal.top_add_coe (x : ℝ) :

⊤ + ↑x = ⊤

@[simp]

theorem EReal.top_add_of_ne_bot {x : EReal} (h : x ≠ ⊥) :

For any extended real number x which is not ⊥, the sum of ⊤ and x is equal to ⊤.

theorem EReal.top_add_iff_ne_bot {x : EReal} :

⊤ + x = ⊤ ↔ x ≠ ⊥

For any extended real number x, the sum of ⊤ and x is equal to ⊤ if and only if x is not ⊥.

@[simp]

theorem EReal.add_top_of_ne_bot {x : EReal} (h : x ≠ ⊥) :

For any extended real number x which is not ⊥, the sum of x and ⊤ is equal to ⊤.

theorem EReal.add_top_iff_ne_bot {x : EReal} :

x + ⊤ = ⊤ ↔ x ≠ ⊥

For any extended real number x, the sum of x and ⊤ is equal to ⊤ if and only if x is not ⊥.

theorem EReal.add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) :

0 < a + b

For any two extended real numbers a and b, if both a and b are greater than 0, then their sum is also greater than 0.

@[simp]

theorem EReal.coe_add_top (x : ℝ) :

↑x + ⊤ = ⊤

theorem EReal.toReal_add {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :

(x + y).toReal = x.toReal + y.toReal

theorem EReal.toENNReal_add {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :

(x + y).toENNReal = x.toENNReal + y.toENNReal

theorem EReal.toENNReal_add_le {x y : EReal} :

(x + y).toENNReal ≤ x.toENNReal + y.toENNReal

theorem EReal.addLECancellable_coe (x : ℝ) :

AddLECancellable ↑x

theorem EReal.add_lt_add_right_coe {x y : EReal} (h : x < y) (z : ℝ) :

x + ↑z < y + ↑z

theorem EReal.add_lt_add_left_coe {x y : EReal} (h : x < y) (z : ℝ) :

↑z + x < ↑z + y

theorem EReal.add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) :

x + z < y + t

theorem EReal.add_lt_add_of_lt_of_le' {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hbot : t ≠ ⊥) (htop : t = ⊤ → z = ⊤ → x = ⊥) :

x + z < y + t

theorem EReal.add_lt_add_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) :

x + z < y + t

See also EReal.add_lt_add_of_lt_of_le' for a version with weaker but less convenient assumptions.

theorem EReal.add_lt_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

x + y < ⊤

theorem EReal.add_ne_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

theorem EReal.add_ne_top_iff_ne_top₂ {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :

x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem EReal.add_ne_top_iff_ne_top_left {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :

x + y ≠ ⊤ ↔ x ≠ ⊤

theorem EReal.add_ne_top_iff_ne_top_right {x y : EReal} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) :

x + y ≠ ⊤ ↔ y ≠ ⊤

theorem EReal.add_ne_top_iff_of_ne_bot {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :

x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

theorem EReal.add_ne_top_iff_of_ne_bot_of_ne_top {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :

x + y ≠ ⊤ ↔ x ≠ ⊤

instance EReal.instLinearOrderedAddCommMonoidWithTopOrderDual :

LinearOrderedAddCommMonoidWithTop EReal ᵒᵈ

We do not have a notion of LinearOrderedAddCommMonoidWithBot but we can at least make the order dual of the extended reals into a LinearOrderedAddCommMonoidWithTop.

Equations

EReal.instLinearOrderedAddCommMonoidWithTopOrderDual = LinearOrderedAddCommMonoidWithTop.mk EReal.instLinearOrderedAddCommMonoidWithTopOrderDual.proof_2

Negation #

def EReal.neg :

EReal → EReal

negation on EReal

Equations

Instances For

instance EReal.instNeg :

Equations

EReal.instNeg = { neg := EReal.neg }

instance EReal.instSubNegZeroMonoid :

SubNegZeroMonoid EReal

Equations

EReal.instSubNegZeroMonoid = SubNegZeroMonoid.mk EReal.instSubNegZeroMonoid.proof_5

@[simp]

theorem EReal.neg_top :

@[simp]

theorem EReal.neg_bot :

@[simp]

theorem EReal.coe_neg (x : ℝ) :

↑(-x) = -↑x

@[simp]

theorem EReal.coe_sub (x y : ℝ) :

↑(x - y) = ↑x - ↑y

theorem EReal.coe_zsmul (n : ℤ) (x : ℝ) :

↑(n • x) = n • ↑x

instance EReal.instInvolutiveNeg :

InvolutiveNeg EReal

Equations

EReal.instInvolutiveNeg = InvolutiveNeg.mk EReal.instInvolutiveNeg.proof_1

@[simp]

theorem EReal.toReal_neg {a : EReal} :

(-a).toReal = -a.toReal

@[simp]

theorem EReal.neg_eq_top_iff {x : EReal} :

-x = ⊤ ↔ x = ⊥

@[simp]

theorem EReal.neg_eq_bot_iff {x : EReal} :

-x = ⊥ ↔ x = ⊤

@[simp]

theorem EReal.neg_eq_zero_iff {x : EReal} :

-x = 0 ↔ x = 0

theorem EReal.neg_strictAnti :

StrictAnti fun (x : EReal) => -x

@[simp]

theorem EReal.neg_le_neg_iff {a b : EReal} :

-a ≤ -b ↔ b ≤ a

@[simp]

theorem EReal.neg_lt_neg_iff {a b : EReal} :

-a < -b ↔ b < a

theorem EReal.neg_le {a b : EReal} :

-a ≤ b ↔ -b ≤ a

-a ≤ b if and only if -b ≤ a on EReal.

theorem EReal.neg_le_of_neg_le {a b : EReal} (h : -a ≤ b) :

-b ≤ a

If -a ≤ b then -b ≤ a on EReal.

theorem EReal.le_neg {a b : EReal} :

a ≤ -b ↔ b ≤ -a

a ≤ -b if and only if b ≤ -a on EReal.

theorem EReal.le_neg_of_le_neg {a b : EReal} (h : a ≤ -b) :

b ≤ -a

If a ≤ -b then b ≤ -a on EReal.

theorem EReal.neg_lt_comm {a b : EReal} :

-a < b ↔ -b < a

-a < b if and only if -b < a on EReal.

@[deprecated EReal.neg_lt_comm (since := "2024-11-19")]

theorem EReal.neg_lt_iff_neg_lt {a b : EReal} :

-a < b ↔ -b < a

Alias of EReal.neg_lt_comm.

-a < b if and only if -b < a on EReal.

theorem EReal.neg_lt_of_neg_lt {a b : EReal} (h : -a < b) :

-b < a

If -a < b then -b < a on EReal.

theorem EReal.lt_neg_comm {a b : EReal} :

a < -b ↔ b < -a

-a < b if and only if -b < a on EReal.

theorem EReal.lt_neg_of_lt_neg {a b : EReal} (h : a < -b) :

b < -a

If a < -b then b < -a on EReal.

def EReal.negOrderIso :

EReal ≃o EReal ᵒᵈ

Negation as an order reversing isomorphism on EReal.

Equations

EReal.negOrderIso = { toFun := fun (x : EReal) => OrderDual.toDual (-x), invFun := fun (x : EReal ᵒᵈ) => -OrderDual.ofDual x, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

theorem EReal.neg_add {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) :

-(x + y) = -x - y

theorem EReal.neg_sub {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y ≠ ⊤) :

-(x - y) = -x + y

Subtraction #

Subtraction on EReal is defined by x - y = x + (-y). Since addition is badly behaved at some points, so is subtraction. There is no standard algebraic typeclass involving subtraction that is registered on EReal, beyond SubNegZeroMonoid, because of this bad behavior.

@[simp]

theorem EReal.bot_sub (x : EReal) :

@[simp]

theorem EReal.sub_top (x : EReal) :

@[simp]

theorem EReal.top_sub_bot :

⊤ - ⊥ = ⊤

@[simp]

theorem EReal.top_sub_coe (x : ℝ) :

⊤ - ↑x = ⊤

@[simp]

theorem EReal.coe_sub_bot (x : ℝ) :

↑x - ⊥ = ⊤

@[simp]

theorem EReal.sub_bot {x : EReal} (h : x ≠ ⊥) :

@[simp]

theorem EReal.top_sub {x : EReal} (hx : x ≠ ⊤) :

@[simp]

theorem EReal.sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) :

x - x = 0

theorem EReal.sub_self_le_zero {x : EReal} :

x - x ≤ 0

theorem EReal.sub_nonneg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :

0 ≤ x - y ↔ y ≤ x

theorem EReal.sub_nonpos {x y : EReal} :

x - y ≤ 0 ↔ x ≤ y

theorem EReal.sub_pos {x y : EReal} :

0 < x - y ↔ y < x

theorem EReal.sub_neg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :

x - y < 0 ↔ x < y

theorem EReal.sub_le_sub {x y z t : EReal} (h : x ≤ y) (h' : t ≤ z) :

x - z ≤ y - t

theorem EReal.sub_lt_sub_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) :

x - t < y - z

theorem EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (x : ℝ) :

↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

theorem EReal.toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :

(x - y).toReal = x.toReal - y.toReal

theorem EReal.toENNReal_sub {x y : EReal} (hy : 0 ≤ y) :

(x - y).toENNReal = x.toENNReal - y.toENNReal

theorem EReal.add_sub_cancel_right {a : EReal} {b : ℝ} :

a + ↑b - ↑b = a

theorem EReal.add_sub_cancel_left {a : EReal} {b : ℝ} :

↑b + a - ↑b = a

theorem EReal.sub_add_cancel {a : EReal} {b : ℝ} :

a - ↑b + ↑b = a

theorem EReal.sub_add_cancel_right {a : EReal} {b : ℝ} :

↑b - (a + ↑b) = -a

theorem EReal.sub_add_cancel_left {a : EReal} {b : ℝ} :

↑b - (↑b + a) = -a

theorem EReal.le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :

a ≤ c - b ↔ a + b ≤ c

theorem EReal.sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) :

a - b ≤ c ↔ a ≤ c + b

theorem EReal.lt_sub_iff_add_lt {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) :

c < a - b ↔ c + b < a

theorem EReal.sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) :

a - c ≤ b

theorem EReal.sub_le_of_le_add' {a b c : EReal} (h : a ≤ b + c) :

a - b ≤ c

See also EReal.sub_le_of_le_add.

theorem EReal.add_le_of_le_sub {a b c : EReal} (h : a ≤ b - c) :

a + c ≤ b

theorem EReal.sub_lt_iff {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤ ∨ c ≠ ⊤) :

c - b < a ↔ c < a + b

theorem EReal.add_lt_of_lt_sub {a b c : EReal} (h : a < b - c) :

a + c < b

theorem EReal.sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) :

a - c < b

theorem EReal.sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) :

a - b < c

See also EReal.sub_lt_of_lt_add.

Addition and order #

theorem EReal.le_of_forall_lt_iff_le {x y : EReal} :

(∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x

theorem EReal.ge_of_forall_gt_iff_ge {x y : EReal} :

(∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x

theorem EReal.add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) :

a + b ≤ c

theorem EReal.le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥) (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') :

c ≤ a + b

@[deprecated EReal.add_le_of_forall_lt (since := "2024-11-19")]

theorem EReal.top_add_le_of_forall_add_le {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) :

a + b ≤ c

Alias of EReal.add_le_of_forall_lt.

@[deprecated EReal.add_le_of_forall_lt (since := "2024-11-19")]

theorem EReal.add_le_of_forall_add_le {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) :

a + b ≤ c

Alias of EReal.add_le_of_forall_lt.

@[deprecated EReal.le_add_of_forall_gt (since := "2024-11-19")]

theorem EReal.le_add_of_forall_le_add {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥) (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') :

c ≤ a + b

Alias of EReal.le_add_of_forall_gt.

theorem ENNReal.toEReal_sub {x y : ENNReal} (hy_top : y ≠ ⊤) (h_le : y ≤ x) :

↑(x - y) = ↑x - ↑y

Multiplication #

@[simp]

theorem EReal.top_mul_top :

⊤ * ⊤ = ⊤

@[simp]

theorem EReal.top_mul_bot :

⊤ * ⊥ = ⊥

@[simp]

theorem EReal.bot_mul_top :

⊥ * ⊤ = ⊥

@[simp]

theorem EReal.bot_mul_bot :

⊥ * ⊥ = ⊤

theorem EReal.coe_mul_top_of_pos {x : ℝ} (h : 0 < x) :

↑x * ⊤ = ⊤

theorem EReal.coe_mul_top_of_neg {x : ℝ} (h : x < 0) :

↑x * ⊤ = ⊥

theorem EReal.top_mul_coe_of_pos {x : ℝ} (h : 0 < x) :

⊤ * ↑x = ⊤

theorem EReal.top_mul_coe_of_neg {x : ℝ} (h : x < 0) :

⊤ * ↑x = ⊥

theorem EReal.mul_top_of_pos {x : EReal} :

0 < x → x * ⊤ = ⊤

theorem EReal.mul_top_of_neg {x : EReal} :

x < 0 → x * ⊤ = ⊥

theorem EReal.top_mul_of_pos {x : EReal} (h : 0 < x) :

theorem EReal.top_mul_of_neg {x : EReal} (h : x < 0) :

theorem EReal.top_mul_coe_ennreal {x : ENNReal} (hx : x ≠ 0) :

⊤ * ↑x = ⊤

theorem EReal.coe_ennreal_mul_top {x : ENNReal} (hx : x ≠ 0) :

↑x * ⊤ = ⊤

theorem EReal.coe_mul_bot_of_pos {x : ℝ} (h : 0 < x) :

↑x * ⊥ = ⊥

theorem EReal.coe_mul_bot_of_neg {x : ℝ} (h : x < 0) :

↑x * ⊥ = ⊤

theorem EReal.bot_mul_coe_of_pos {x : ℝ} (h : 0 < x) :

⊥ * ↑x = ⊥

theorem EReal.bot_mul_coe_of_neg {x : ℝ} (h : x < 0) :

⊥ * ↑x = ⊤

theorem EReal.mul_bot_of_pos {x : EReal} :

0 < x → x * ⊥ = ⊥

theorem EReal.mul_bot_of_neg {x : EReal} :

x < 0 → x * ⊥ = ⊤

theorem EReal.bot_mul_of_pos {x : EReal} (h : 0 < x) :

theorem EReal.bot_mul_of_neg {x : EReal} (h : x < 0) :

theorem EReal.toReal_mul {x y : EReal} :

(x * y).toReal = x.toReal * y.toReal

instance EReal.instNoZeroDivisors :

NoZeroDivisors EReal

theorem EReal.mul_pos_iff {a b : EReal} :

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

theorem EReal.mul_nonneg_iff {a b : EReal} :

0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem EReal.mul_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) :

0 < a * b

The product of two positive extended real numbers is positive.

theorem EReal.induction₂_neg_left {P : EReal → EReal → Prop} (neg_left : ∀ {x y : EReal}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (top_neg : ∀ x < 0, P ⊤ ↑x) (top_bot : P ⊤ ⊥) (zero_top : P 0 ⊤) (zero_bot : P 0 ⊥) (pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤) (pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (x y : EReal) :

P x y

Induct on two ereals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that P x y implies P (-x) y for all x, y.

theorem EReal.induction₂_symm_neg {P : EReal → EReal → Prop} (symm : ∀ {x y : EReal}, P x y → P y x) (neg_left : ∀ {x y : EReal}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x) (top_zero : P ⊤ 0) (coe_coe : ∀ (x y : ℝ), P ↑x ↑y) (x y : EReal) :

P x y

Induct on two ereals by performing case splits on the sign of one whenever the other is infinite. This version eliminates some cases by assuming that P is symmetric and P x y implies P (-x) y for all x, y.

theorem EReal.neg_mul (x y : EReal) :

-x * y = -(x * y)

instance EReal.instHasDistribNeg :

HasDistribNeg EReal

Equations

EReal.instHasDistribNeg = HasDistribNeg.mk EReal.neg_mul EReal.instHasDistribNeg.proof_1

theorem EReal.mul_neg_iff {a b : EReal} :

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

theorem EReal.mul_nonpos_iff {a b : EReal} :

a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem EReal.mul_eq_top (a b : EReal) :

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

theorem EReal.mul_ne_top (a b : EReal) :

a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

theorem EReal.mul_eq_bot (a b : EReal) :

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

theorem EReal.mul_ne_bot (a b : EReal) :

a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

theorem EReal.toENNReal_mul {x y : EReal} (hx : 0 ≤ x) :

(x * y).toENNReal = x.toENNReal * y.toENNReal

EReal.toENNReal is multiplicative. For the version with the nonnegativity hypothesis on the second variable, see EReal.toENNReal_mul'.

theorem EReal.toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) :

(x * y).toENNReal = x.toENNReal * y.toENNReal

EReal.toENNReal is multiplicative. For the version with the nonnegativity hypothesis on the first variable, see EReal.toENNReal_mul.

theorem EReal.right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :

(a + b) * c = a * c + b * c

theorem EReal.left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :

c * (a + b) = c * a + c * b

theorem EReal.left_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) :

x * (y + z) = x * y + x * z

theorem EReal.right_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) :

(y + z) * x = y * x + z * x

@[simp]

theorem EReal.nsmul_eq_mul (n : ℕ) (x : EReal) :

n • x = ↑n * x