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.lean 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.lean.

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 ⊥.

@[deprecated Right.add_pos_of_nonneg_of_pos (since := "2025-08-14")]

theorem EReal.add_pos_of_nonneg_of_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a b : α} (ha : 0 ≤ a) (hb : 0 < b) :

0 < a + b

Alias of Right.add_pos_of_nonneg_of_pos.

Assumes right covariance. The lemma assuming left covariance is Left.add_pos_of_nonneg_of_pos.

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

0 < a + b

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

@[deprecated EReal.add_ne_top_iff_ne_top₂ (since := "2025-08-14")]

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

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

Alias of EReal.add_ne_top_iff_ne_top₂.

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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

@[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 = { toNeg := EReal.instNeg, neg_neg := 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.

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.

@[simp]

theorem EReal.neg_lt_zero {a : EReal} :

-a < 0 ↔ 0 < a

@[simp]

theorem EReal.neg_le_zero {a : EReal} :

-a ≤ 0 ↔ 0 ≤ a

@[simp]

theorem EReal.neg_pos {a : EReal} :

0 < -a ↔ a < 0

@[simp]

theorem EReal.neg_nonneg {a : EReal} :

0 ≤ -a ↔ a ≤ 0

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

def EReal.recENNReal {motive : EReal → Sort u_1} (coe : (x : ENNReal) → motive ↑x) (neg_coe : (x : ENNReal) → 0 < x → motive (-↑x)) (x : EReal) :

motive x

Induction principle for EReals splitting into cases ↑(x : ℝ≥0∞) and -↑(x : ℝ≥0∞). In the latter case, we additionally assume 0 < x.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem EReal.recENNReal_coe_ennreal {motive : EReal → Sort u_1} (coe : (x : ENNReal) → motive ↑x) (neg_coe : (x : ENNReal) → 0 < x → motive (-↑x)) (x : ENNReal) :

recENNReal coe neg_coe ↑x = coe x

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

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_nonneg {a b : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :

0 ≤ a * b

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 = { toInvolutiveNeg := EReal.instInvolutiveNeg, neg_mul := EReal.neg_mul, mul_neg := 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

def Mathlib.Meta.Positivity.evalERealAdd :

Extension for the positivity tactic: sum of two EReals.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Mathlib.Meta.Positivity.evalERealMul :

Extension for the positivity tactic: product of two EReals.

Equations

One or more equations did not get rendered due to their size.

Instances For