Mathlib.Data.EReal.Operations

EReal.add_bot theorem

(x : EReal) : x + ⊥ = ⊥

Full source

@[simp]
theorem add_bot (x : EReal) : x + ⊥ = ⊥ :=
  WithBot.add_bot _

Addition with $-\infty$ in Extended Real Numbers

Informal description

For any extended real number $x \in \mathbb{EReal}$, the sum of $x$ and $-\infty$ (denoted as $\bot$) is $-\infty$, i.e., $x + (-\infty) = -\infty$.

EReal.bot_add theorem

(x : EReal) : ⊥ + x = ⊥

Full source

@[simp]
theorem bot_add (x : EReal) : ⊥ + x = ⊥ :=
  WithBot.bot_add _

Left Addition with Negative Infinity in Extended Reals

Informal description

For any extended real number $x \in \mathbb{EReal}$, the sum of $-\infty$ (denoted as $\bot$) and $x$ is equal to $-\infty$, i.e., $-\infty + x = -\infty$.

EReal.add_eq_bot_iff theorem

{x y : EReal} : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Full source

@[simp]
theorem add_eq_bot_iff {x y : EReal} : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥ :=
  WithBot.add_eq_bot

Sum Equals Negative Infinity Criterion in Extended Reals

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}}$, the sum $x + y$ equals $-\infty$ if and only if either $x = -\infty$ or $y = -\infty$.

EReal.add_ne_bot_iff theorem

{x y : EReal} : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Full source

lemma add_ne_bot_iff {x y : EReal} : x + y ≠ ⊥x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥ := WithBot.add_ne_bot

Sum Not Equal to Negative Infinity in Extended Reals

Informal description

For any extended real numbers $x$ and $y$, the sum $x + y$ is not equal to $-\infty$ if and only if both $x$ and $y$ are not equal to $-\infty$.

EReal.bot_lt_add_iff theorem

{x y : EReal} : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Full source

@[simp]
theorem bot_lt_add_iff {x y : EReal} : ⊥⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y := by
  simp [bot_lt_iff_ne_bot]

Sum Greater Than Negative Infinity Criterion in Extended Reals

Informal description

For any extended real numbers $x$ and $y$, the sum $x + y$ is greater than $-\infty$ if and only if both $x$ and $y$ are greater than $-\infty$.

EReal.top_add_top theorem

: (⊤ : EReal) + ⊤ = ⊤

Full source

@[simp]
theorem top_add_top : (⊤ : EReal) + ⊤ = ⊤ :=
  rfl

Sum of Two Positive Infinities in Extended Reals is Positive Infinity

Informal description

The sum of two positive infinities in the extended real numbers is equal to positive infinity, i.e., $\top + \top = \top$.

EReal.top_add_coe theorem

(x : ℝ) : (⊤ : EReal) + x = ⊤

Full source

@[simp]
theorem top_add_coe (x : ℝ) : (⊤ : EReal) + x = ⊤ :=
  rfl

Addition of Infinity with Real Number Yields Infinity

Informal description

For any real number $x$, the sum of $\top$ (positive infinity) and $x$ in the extended real numbers $\overline{\mathbb{R}}$ is equal to $\top$, i.e., $\top + x = \top$.

EReal.top_add_of_ne_bot theorem

{x : EReal} (h : x ≠ ⊥) : ⊤ + x = ⊤

Full source

/-- For any extended real number `x` which is not `⊥`, the sum of `⊤` and `x` is equal to `⊤`. -/
@[simp]
theorem top_add_of_ne_bot {x : EReal} (h : x ≠ ⊥) : ⊤ + x = ⊤ := by
  induction x
  · exfalso; exact h (Eq.refl ⊥)
  · exact top_add_coe _
  · exact top_add_top

Addition of Positive Infinity with Non-Negative-Infinity Extended Real Yields Positive Infinity

Informal description

For any extended real number $x \neq -\infty$, the sum of $+\infty$ and $x$ is $+\infty$, i.e., $+\infty + x = +\infty$.

EReal.top_add_iff_ne_bot theorem

{x : EReal} : ⊤ + x = ⊤ ↔ x ≠ ⊥

Full source

/-- For any extended real number `x`, the sum of `⊤` and `x` is equal to `⊤`
if and only if `x` is not `⊥`. -/
theorem top_add_iff_ne_bot {x : EReal} : ⊤⊤ + x = ⊤ ↔ x ≠ ⊥ := by
  constructor <;> intro h
  · rintro rfl
    rw [add_bot] at h
    exact bot_ne_top h
  · cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h

Characterization of When Adding Infinity Preserves Infinity in Extended Reals

Informal description

For any extended real number $x \in \mathbb{EReal}$, the sum of $+\infty$ and $x$ equals $+\infty$ if and only if $x \neq -\infty$. In other words, $\top + x = \top \leftrightarrow x \neq \bot$.

EReal.add_top_of_ne_bot theorem

{x : EReal} (h : x ≠ ⊥) : x + ⊤ = ⊤

Full source

/-- For any extended real number `x` which is not `⊥`, the sum of `x` and `⊤` is equal to `⊤`. -/
@[simp]
theorem add_top_of_ne_bot {x : EReal} (h : x ≠ ⊥) : x + ⊤ = ⊤ := by
  rw [add_comm, top_add_of_ne_bot h]

Addition of Non-Negative-Infinity Extended Real with Positive Infinity Yields Positive Infinity

Informal description

For any extended real number $x \neq -\infty$, the sum of $x$ and $+\infty$ is $+\infty$, i.e., $x + \infty = \infty$.

EReal.add_top_iff_ne_bot theorem

{x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥

Full source

/-- For any extended real number `x`, the sum of `x` and `⊤` is equal to `⊤`
if and only if `x` is not `⊥`. -/
theorem add_top_iff_ne_bot {x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥ := by rw [add_comm, top_add_iff_ne_bot]

Characterization of When Adding Infinity Preserves Infinity in Extended Reals: $x + \infty = \infty \leftrightarrow x \neq -\infty$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the sum $x + \infty$ equals $\infty$ if and only if $x \neq -\infty$. In other words, $x + \top = \top \leftrightarrow x \neq \bot$.

EReal.add_pos theorem

{a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

Full source

/-- 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`. -/
theorem add_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a + b := by
  induction a
  · exfalso; exact not_lt_bot ha
  · induction b
    · exfalso; exact not_lt_bot hb
    · norm_cast at *; exact Left.add_pos ha hb
    · exact add_top_of_ne_bot (bot_lt_zero.trans ha).ne' ▸ hb
  · rw [top_add_of_ne_bot (bot_lt_zero.trans hb).ne']
    exact ha

Positivity of Sum of Positive Extended Reals

Informal description

For any two extended real numbers $a$ and $b$, if $0 < a$ and $0 < b$, then $0 < a + b$.

EReal.coe_add_top theorem

(x : ℝ) : (x : EReal) + ⊤ = ⊤

Full source

@[simp]
theorem coe_add_top (x : ℝ) : (x : EReal) + ⊤ = ⊤ :=
  rfl

Addition of Real and Infinity in Extended Reals: $x + \infty = \infty$

Informal description

For any real number $x \in \mathbb{R}$, when cast to the extended reals $\overline{\mathbb{R}}$, we have $x + \top = \top$, where $\top$ represents positive infinity in the extended real numbers.

EReal.toReal_add theorem

 {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) : toReal (x + y) = toReal x + toReal y

Full source

theorem toReal_add {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
    toReal (x + y) = toReal x + toReal y := by
  lift x to ℝ using ⟨hx, h'x⟩
  lift y to ℝ using ⟨hy, h'y⟩
  rfl

Real Part of Sum of Finite Extended Reals Equals Sum of Real Parts

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$ such that $x$ is neither positive infinity ($\top$) nor negative infinity ($\bot$), and $y$ is neither positive infinity nor negative infinity, the real part of their sum equals the sum of their real parts, i.e., $\text{toReal}(x + y) = \text{toReal}(x) + \text{toReal}(y)$.

EReal.toENNReal_add theorem

{x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : (x + y).toENNReal = x.toENNReal + y.toENNReal

Full source

lemma toENNReal_add {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (x + y).toENNReal = x.toENNReal + y.toENNReal := by
  induction x <;> induction y <;> try {· simp_all}
  norm_cast
  simp_rw [real_coe_toENNReal]
  simp_all [ENNReal.ofReal_add]

Additivity of `toENNReal` for Non-Negative Extended Reals

Informal description

For any extended real numbers $x$ and $y$ such that $0 \leq x$ and $0 \leq y$, the extended non-negative real number obtained by applying the `toENNReal` function to their sum equals the sum of their individual `toENNReal` values, i.e., $(x + y).\text{toENNReal} = x.\text{toENNReal} + y.\text{toENNReal}$.

EReal.toENNReal_add_le theorem

{x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toENNReal

Full source

lemma toENNReal_add_le {x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toENNReal := by
  induction x <;> induction y <;> try {· simp}
  exact ENNReal.ofReal_add_le

Subadditivity of Extended Real to Extended Non-Negative Real Conversion

Informal description

For any extended real numbers $x, y \in \mathbb{EReal}$, the extended non-negative real number obtained by converting the sum $x + y$ is less than or equal to the sum of the conversions of $x$ and $y$, i.e., $(x + y).\text{toENNReal} \leq x.\text{toENNReal} + y.\text{toENNReal}$.

EReal.addLECancellable_coe theorem

(x : ℝ) : AddLECancellable (x : EReal)

Full source

theorem addLECancellable_coe (x : ℝ) : AddLECancellable (x : EReal)
  | _, ⊤, _ => le_top
  | ⊥, _, _ => bot_le
  | ⊤, (z : ℝ), h => by simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h
  | _, ⊥, h => by simpa using h
  | (y : ℝ), (z : ℝ), h => by
    simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

Additive Cancellability of Real Numbers in Extended Reals

Informal description

For any real number $x \in \mathbb{R}$, the extended real number obtained by embedding $x$ into $\mathbb{EReal}$ is additively cancellable, meaning that for any $y, z \in \mathbb{EReal}$, if $x + y \leq x + z$, then $y \leq z$.

EReal.add_lt_add_right_coe theorem

{x y : EReal} (h : x < y) (z : ℝ) : x + z < y + z

Full source

theorem add_lt_add_right_coe {x y : EReal} (h : x < y) (z : ℝ) : x + z < y + z :=
  not_le.1 <| mt (addLECancellable_coe z).add_le_add_iff_right.1 h.not_le

Right Addition Preserves Strict Inequality for Extended Reals with Real Coefficients

Informal description

For any extended real numbers $x, y \in \mathbb{EReal}$ such that $x < y$, and for any real number $z \in \mathbb{R}$, it holds that $x + z < y + z$.

EReal.add_lt_add_left_coe theorem

{x y : EReal} (h : x < y) (z : ℝ) : (z : EReal) + x < z + y

Full source

theorem add_lt_add_left_coe {x y : EReal} (h : x < y) (z : ℝ) : (z : EReal) + x < z + y := by
  simpa [add_comm] using add_lt_add_right_coe h z

Left Addition Preserves Strict Inequality for Extended Reals with Real Coefficients

Informal description

For any extended real numbers $x, y \in \mathbb{EReal}$ such that $x < y$, and for any real number $z \in \mathbb{R}$, it holds that $z + x < z + y$.

EReal.add_lt_add theorem

{x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t

Full source

theorem add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t := by
  rcases eq_or_ne x ⊥ with (rfl | hx)
  · simp [h1, bot_le.trans_lt h2]
  · lift x to ℝ using ⟨h1.ne_top, hx⟩
    calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := add_le_add_right h1.le _

Addition Preserves Strict Inequality in Extended Reals

Informal description

For any extended real numbers $x, y, z, t \in \mathbb{EReal}$ such that $x < y$ and $z < t$, it holds that $x + z < y + t$.

EReal.add_lt_add_of_lt_of_le' theorem

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

Full source

theorem 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 := by
  rcases h'.eq_or_lt with (rfl | hlt)
  · rcases eq_or_ne z ⊤ with (rfl | hz)
    · obtain rfl := htop rfl rfl
      simpa
    lift z to ℝ using ⟨hz, hbot⟩
    exact add_lt_add_right_coe h z
  · exact add_lt_add h hlt

Strict Inequality Preservation under Addition with Extended Reals and Side Conditions

Informal description

For any extended real numbers $x, y, z, t \in \mathbb{EReal}$ such that $x < y$, $z \leq t$, $t \neq -\infty$, and if $t = +\infty$ and $z = +\infty$ then $x = -\infty$, it holds that $x + z < y + t$.

EReal.add_lt_add_of_lt_of_le theorem

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

Full source

/-- See also `EReal.add_lt_add_of_lt_of_le'` for a version with weaker but less convenient
assumptions. -/
theorem 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 :=
  add_lt_add_of_lt_of_le' h h' (ne_bot_of_le_ne_bot hz h') fun ht' => (ht ht').elim

Strict Inequality Preservation under Addition with Bounded Extended Reals

Informal description

For any extended real numbers $x, y, z, t \in \mathbb{EReal}$ such that $x < y$, $z \leq t$, $z \neq -\infty$, and $t \neq +\infty$, it holds that $x + z < y + t$.

EReal.add_lt_top theorem

{x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y < ⊤

Full source

theorem add_lt_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y < ⊤ :=
  add_lt_add hx.lt_top hy.lt_top

Sum of Non-Top Extended Reals is Below Top

Informal description

For any extended real numbers $x, y \in \mathbb{EReal}$ such that $x \neq \top$ and $y \neq \top$, their sum satisfies $x + y < \top$.

EReal.add_ne_top theorem

{x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y ≠ ⊤

Full source

lemma add_ne_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y ≠ ⊤ :=
  lt_top_iff_ne_top.mp <| add_lt_top hx hy

Sum of Non-Top Extended Reals is Not Top

Informal description

For any extended real numbers $x$ and $y$ such that $x \neq +\infty$ and $y \neq +\infty$, their sum $x + y$ is not equal to $+\infty$.

EReal.add_ne_top_iff_ne_top₂ theorem

{x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Full source

lemma add_ne_top_iff_ne_top₂ {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :
    x + y ≠ ⊤x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤ := by
  refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩
  cases x <;> simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]
  cases y <;> simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

Sum Not Equal to Positive Infinity Condition for Extended Reals (Two-Sided Version)

Informal description

For any extended real numbers $x$ and $y$ such that $x \neq -\infty$ and $y \neq -\infty$, the sum $x + y$ is not equal to $+\infty$ if and only if both $x \neq +\infty$ and $y \neq +\infty$.

EReal.add_ne_top_iff_ne_top_left theorem

{x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤

Full source

lemma add_ne_top_iff_ne_top_left {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :
    x + y ≠ ⊤x + y ≠ ⊤ ↔ x ≠ ⊤ := by
  cases x <;> simp [add_ne_top_iff_ne_top₂, hy, hy']

Sum Not Equal to Positive Infinity Condition for Extended Reals

Informal description

For any extended real numbers $x$ and $y$ where $y \neq -\infty$ and $y \neq +\infty$, the sum $x + y$ is not equal to $+\infty$ if and only if $x \neq +\infty$.

EReal.add_ne_top_iff_ne_top_right theorem

{x y : EReal} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) : x + y ≠ ⊤ ↔ y ≠ ⊤

Full source

lemma add_ne_top_iff_ne_top_right {x y : EReal} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) :
    x + y ≠ ⊤x + y ≠ ⊤ ↔ y ≠ ⊤ := add_comm x y ▸ add_ne_top_iff_ne_top_left hx hx'

Sum Not Equal to Positive Infinity Condition for Extended Reals (Right Version)

Informal description

For any extended real numbers $x$ and $y$ where $x \neq -\infty$ and $x \neq +\infty$, the sum $x + y$ is not equal to $+\infty$ if and only if $y \neq +\infty$.

EReal.add_ne_top_iff_of_ne_bot theorem

{x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Full source

lemma add_ne_top_iff_of_ne_bot {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :
    x + y ≠ ⊤x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤ := by
  refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩
  induction x <;> simp_all
  induction y <;> simp_all

Sum Not Equal to Positive Infinity Condition for Non-Negative-Infinity Extended Reals

Informal description

For any extended real numbers $x$ and $y$ such that $x \neq -\infty$ and $y \neq -\infty$, the sum $x + y$ is not equal to $+\infty$ if and only if both $x \neq +\infty$ and $y \neq +\infty$.

EReal.add_ne_top_iff_of_ne_bot_of_ne_top theorem

{x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : x + y ≠ ⊤ ↔ x ≠ ⊤

Full source

lemma add_ne_top_iff_of_ne_bot_of_ne_top {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :
    x + y ≠ ⊤x + y ≠ ⊤ ↔ x ≠ ⊤ := by
  induction x <;> simp [add_ne_top_iff_of_ne_bot, hy, hy']

Sum Not Equal to Positive Infinity Condition for Extended Reals

Informal description

For extended real numbers $x$ and $y$ where $y \neq -\infty$ and $y \neq +\infty$, the sum $x + y$ is not equal to $+\infty$ if and only if $x \neq +\infty$.

EReal.instLinearOrderedAddCommMonoidWithTopOrderDual instance

: LinearOrderedAddCommMonoidWithTop ERealᵒᵈ

Full source

/-- We do not have a notion of `LinearOrderedAddCommMonoidWithBot` but we can at least make
the order dual of the extended reals into a `LinearOrderedAddCommMonoidWithTop`. -/
instance : LinearOrderedAddCommMonoidWithTop ERealERealᵒᵈ where
  le_top := by simp
  top_add' := by
    rw [OrderDual.forall]
    intro x
    rw [← OrderDual.toDual_bot, ← toDual_add, bot_add, OrderDual.toDual_bot]

Order Dual of Extended Reals as Linearly Ordered Additive Monoid with Top

Informal description

The order dual of the extended real numbers $\overline{\mathbb{R}}^{\text{op}}$ forms a linearly ordered commutative additive monoid with a top element, where the addition operation is compatible with the linear order and the top element is additively absorbing.

EReal.neg definition

: EReal → EReal

Full source

/-- negation on `EReal` -/
protected def neg : EReal → EReal
  | ⊥ => ⊤
  | ⊤ => ⊥
  | (x : ℝ) => (-x : ℝ)

Negation on extended real numbers

Informal description

The negation function on extended real numbers maps: - $-\infty$ to $\infty$ - $\infty$ to $-\infty$ - A real number $x$ to its additive inverse $-x$ in the reals

EReal.instNeg instance

: Neg EReal

Full source

instance : Neg EReal := ⟨EReal.neg⟩

Negation Operation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ are equipped with a negation operation defined by: - $-(-\infty) = \infty$ - $-(\infty) = -\infty$ - $-(x) = -x$ for any real number $x \in \mathbb{R}$ This operation is an order-reversing isomorphism and satisfies the usual properties of negation.

EReal.instSubNegZeroMonoid instance

: SubNegZeroMonoid EReal

Full source

instance : SubNegZeroMonoid EReal where
  neg_zero := congr_arg Real.toEReal neg_zero
  zsmul := zsmulRec

Sub-Neg-Zero Monoid Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ form a sub-neg-zero monoid, where subtraction is defined as $x - y = x + (-y)$ with the negation operation satisfying $-(-\infty) = \infty$, $-(\infty) = -\infty$, and $-(x) = -x$ for any real number $x \in \mathbb{R}$.

EReal.neg_top theorem

: -(⊤ : EReal) = ⊥

Full source

@[simp]
theorem neg_top : -(⊤ : EReal) = ⊥ :=
  rfl

Negation of Infinity in Extended Real Numbers: $-(\infty) = -\infty$

Informal description

The negation of the extended real number $\infty$ (denoted as $\top$) is $-\infty$ (denoted as $\bot$), i.e., $-(\infty) = -\infty$.

EReal.neg_bot theorem

: -(⊥ : EReal) = ⊤

Full source

@[simp]
theorem neg_bot : -(⊥ : EReal) = ⊤ :=
  rfl

Negation of $-\infty$ in Extended Real Numbers: $-(-\infty) = \infty$

Informal description

The negation of the extended real number $-\infty$ (denoted as $\bot$) is $\infty$ (denoted as $\top$), i.e., $-(-\infty) = \infty$.

EReal.coe_neg theorem

(x : ℝ) : (↑(-x) : EReal) = -↑x

Full source

@[simp, norm_cast] theorem coe_neg (x : ℝ) : (↑(-x) : EReal) = -↑x := rfl

Negation Commutes with Coercion from Reals to Extended Reals

Informal description

For any real number $x$, the extended real number obtained by coercing $-x$ is equal to the negation of the extended real number obtained by coercing $x$, i.e., $(-x : \overline{\mathbb{R}}) = - (x : \overline{\mathbb{R}})$.

EReal.coe_sub theorem

(x y : ℝ) : (↑(x - y) : EReal) = x - y

Full source

@[simp, norm_cast] theorem coe_sub (x y : ℝ) : (↑(x - y) : EReal) = x - y := rfl

Coercion Preserves Subtraction in Extended Real Numbers

Informal description

For any real numbers $x$ and $y$, the extended real number obtained by coercing the difference $x - y$ is equal to the difference of the coercions of $x$ and $y$ in the extended reals, i.e., $(x - y : \overline{\mathbb{R}}) = (x : \overline{\mathbb{R}}) - (y : \overline{\mathbb{R}})$.

EReal.coe_zsmul theorem

(n : ℤ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal)

Full source

@[norm_cast]
theorem coe_zsmul (n : ℤ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_zsmul' (⟨⟨(↑), coe_zero⟩, coe_add⟩ : ℝℝ →+ EReal) coe_neg _ _

Integer Scalar Multiplication Commutes with Coercion to Extended Reals

Informal description

For any integer $n$ and real number $x$, the extended real number obtained by coercing the integer scalar multiple $n \cdot x$ is equal to the integer scalar multiple of the extended real number obtained by coercing $x$, i.e., $(n \cdot x : \overline{\mathbb{R}}) = n \cdot (x : \overline{\mathbb{R}})$.

EReal.instInvolutiveNeg instance

: InvolutiveNeg EReal

Full source

instance : InvolutiveNeg EReal where
  neg_neg a :=
    match a with
    | ⊥ => rfl
    | ⊤ => rfl
    | (a : ℝ) => congr_arg Real.toEReal (neg_neg a)

Involutive Negation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ are equipped with an involutive negation operation, meaning that $-(-x) = x$ for any $x \in \overline{\mathbb{R}}$. This operation is defined by: - $-(-\infty) = \infty$ - $-(\infty) = -\infty$ - $-(x) = -x$ for any real number $x \in \mathbb{R}$

EReal.toReal_neg theorem

: ∀ {a : EReal}, toReal (-a) = -toReal a

Full source

@[simp]
theorem toReal_neg : ∀ {a : EReal}, toReal (-a) = -toReal a
  | ⊤ => by simp
  | ⊥ => by simp
  | (x : ℝ) => rfl

Negation Commutes with Real Projection on Extended Reals

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the real part of its negation is equal to the negation of its real part, i.e., $\text{toReal}(-a) = -\text{toReal}(a)$.

EReal.neg_eq_top_iff theorem

{x : EReal} : -x = ⊤ ↔ x = ⊥

Full source

@[simp]
theorem neg_eq_top_iff {x : EReal} : -x = ⊤ ↔ x = ⊥ :=
  neg_injective.eq_iff' rfl

Negation of Extended Real Equals Infinity iff Original Equals Negative Infinity

Informal description

For any extended real number $x \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the negation of $x$ equals $\infty$ if and only if $x$ equals $-\infty$, i.e., $-x = \infty \leftrightarrow x = -\infty$.

EReal.neg_eq_bot_iff theorem

{x : EReal} : -x = ⊥ ↔ x = ⊤

Full source

@[simp]
theorem neg_eq_bot_iff {x : EReal} : -x = ⊥ ↔ x = ⊤ :=
  neg_injective.eq_iff' rfl

Negation of Extended Real Equals Negative Infinity iff Original Equals Infinity

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the negation of $x$ equals $-\infty$ if and only if $x$ equals $\infty$, i.e., $-x = -\infty \leftrightarrow x = \infty$.

EReal.neg_eq_zero_iff theorem

{x : EReal} : -x = 0 ↔ x = 0

Full source

@[simp]
theorem neg_eq_zero_iff {x : EReal} : -x = 0 ↔ x = 0 :=
  neg_injective.eq_iff' neg_zero

Negation of Extended Real Equals Zero iff Original Equals Zero

Informal description

For any extended real number $x \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the negation of $x$ equals $0$ if and only if $x$ equals $0$, i.e., $-x = 0 \leftrightarrow x = 0$.

EReal.neg_strictAnti theorem

: StrictAnti (-· : EReal → EReal)

Full source

theorem neg_strictAnti : StrictAnti (- · : EReal → EReal) :=
  WithBot.strictAnti_iff.2 ⟨WithTop.strictAnti_iff.2
    ⟨coe_strictMono.comp_strictAnti fun _ _ => neg_lt_neg, fun _ => bot_lt_coe _⟩,
      WithTop.forall.2 ⟨bot_lt_top, fun _ => coe_lt_top _⟩⟩

Negation is Strictly Antitone on Extended Real Numbers

Informal description

The negation function $x \mapsto -x$ on the extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ is strictly antitone, meaning that for any $a, b \in \overline{\mathbb{R}}$, if $a < b$ then $-b < -a$.

EReal.neg_le_neg_iff theorem

{a b : EReal} : -a ≤ -b ↔ b ≤ a

Full source

@[simp] theorem neg_le_neg_iff {a b : EReal} : -a ≤ -b ↔ b ≤ a := neg_strictAnti.le_iff_le

Negation Reverses Order in Extended Real Numbers

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the negation $-a$ is less than or equal to $-b$ if and only if $b$ is less than or equal to $a$, i.e., $-a \leq -b \leftrightarrow b \leq a$.

EReal.neg_lt_neg_iff theorem

{a b : EReal} : -a < -b ↔ b < a

Full source

@[simp] theorem neg_lt_neg_iff {a b : EReal} : -a < -b ↔ b < a := neg_strictAnti.lt_iff_lt

Negation Reverses Strict Order in Extended Real Numbers

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the negation $-a$ is strictly less than $-b$ if and only if $b$ is strictly less than $a$, i.e., $-a < -b \leftrightarrow b < a$.

EReal.neg_le theorem

{a b : EReal} : -a ≤ b ↔ -b ≤ a

Full source

/-- `-a ≤ b` if and only if `-b ≤ a` on `EReal`. -/
protected theorem neg_le {a b : EReal} : -a ≤ b ↔ -b ≤ a := by
 rw [← neg_le_neg_iff, neg_neg]

Negation and Order Reversal in Extended Real Numbers: $-a \leq b \leftrightarrow -b \leq a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, the inequality $-a \leq b$ holds if and only if $-b \leq a$.

EReal.neg_le_of_neg_le theorem

{a b : EReal} (h : -a ≤ b) : -b ≤ a

Full source

/-- If `-a ≤ b` then `-b ≤ a` on `EReal`. -/
protected theorem neg_le_of_neg_le {a b : EReal} (h : -a ≤ b) : -b ≤ a := EReal.neg_le.mp h

Negation Reverses Order in Extended Real Numbers: $-a \leq b \implies -b \leq a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, if $-a \leq b$, then $-b \leq a$.

EReal.le_neg theorem

{a b : EReal} : a ≤ -b ↔ b ≤ -a

Full source

/-- `a ≤ -b` if and only if `b ≤ -a` on `EReal`. -/
protected theorem le_neg {a b : EReal} : a ≤ -b ↔ b ≤ -a := by
  rw [← neg_le_neg_iff, neg_neg]

Order Reversal under Negation in Extended Real Numbers: $a \leq -b \leftrightarrow b \leq -a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the inequality $a \leq -b$ holds if and only if $b \leq -a$.

EReal.le_neg_of_le_neg theorem

{a b : EReal} (h : a ≤ -b) : b ≤ -a

Full source

/-- If `a ≤ -b` then `b ≤ -a` on `EReal`. -/
protected theorem le_neg_of_le_neg {a b : EReal} (h : a ≤ -b) : b ≤ -a := EReal.le_neg.mp h

Order Reversal under Negation in Extended Real Numbers

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, if $a \leq -b$, then $b \leq -a$.

EReal.neg_lt_comm theorem

{a b : EReal} : -a < b ↔ -b < a

Full source

/-- `-a < b` if and only if `-b < a` on `EReal`. -/
theorem neg_lt_comm {a b : EReal} : -a < b ↔ -b < a := by rw [← neg_lt_neg_iff, neg_neg]

Negation Reverses Strict Inequality in Extended Real Numbers

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the inequality $-a < b$ holds if and only if $-b < a$.

EReal.neg_lt_of_neg_lt theorem

{a b : EReal} (h : -a < b) : -b < a

Full source

/-- If `-a < b` then `-b < a` on `EReal`. -/
protected theorem neg_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a := neg_lt_comm.mp h

Negation Reverses Strict Inequality in Extended Real Numbers: $-a < b \Rightarrow -b < a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, if $-a < b$, then $-b < a$.

EReal.lt_neg_comm theorem

{a b : EReal} : a < -b ↔ b < -a

Full source

/-- `-a < b` if and only if `-b < a` on `EReal`. -/
theorem lt_neg_comm {a b : EReal} : a < -b ↔ b < -a := by
  rw [← neg_lt_neg_iff, neg_neg]

Order Reversal under Negation in Extended Real Numbers: $a < -b \leftrightarrow b < -a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the inequality $a < -b$ holds if and only if $b < -a$ holds.

EReal.lt_neg_of_lt_neg theorem

{a b : EReal} (h : a < -b) : b < -a

Full source

/-- If `a < -b` then `b < -a` on `EReal`. -/
protected theorem lt_neg_of_lt_neg {a b : EReal} (h : a < -b) : b < -a := lt_neg_comm.mp h

Order Reversal under Negation in Extended Real Numbers: $a < -b$ implies $b < -a$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, if $a < -b$, then $b < -a$.

EReal.negOrderIso definition

: EReal ≃o ERealᵒᵈ

Full source

/-- Negation as an order reversing isomorphism on `EReal`. -/
def negOrderIso : ERealEReal ≃o ERealᵒᵈ :=
  { Equiv.neg EReal with
    toFun := fun x => OrderDual.toDual (-x)
    invFun := fun x => -OrderDual.ofDual x
    map_rel_iff' := neg_le_neg_iff }

Negation as an order-reversing isomorphism on extended real numbers

Informal description

The negation operation on extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ defines an order-reversing isomorphism between $\overline{\mathbb{R}}$ and its order dual $\overline{\mathbb{R}}^{\text{op}}$. Specifically, the map $x \mapsto -x$ is an order isomorphism that reverses the ordering, satisfying $-a \leq -b$ if and only if $b \leq a$ for any $a, b \in \overline{\mathbb{R}}$.

EReal.neg_add theorem

{x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) : -(x + y) = -x - y

Full source

lemma neg_add {x y : EReal} (h1 : x ≠ ⊥x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤x ≠ ⊤ ∨ y ≠ ⊥) :
    - (x + y) = - x - y := by
  induction x <;> induction y <;> try tauto
  rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

Negation of Sum Equals Difference of Negations in Extended Reals

Informal description

For any extended real numbers $x$ and $y$ such that either $x \neq -\infty$ or $y \neq \infty$, and either $x \neq \infty$ or $y \neq -\infty$, the negation of their sum equals the difference of their negations, i.e., $-(x + y) = -x - y$.

EReal.neg_sub theorem

{x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y ≠ ⊤) : -(x - y) = -x + y

Full source

lemma neg_sub {x y : EReal} (h1 : x ≠ ⊥x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤x ≠ ⊤ ∨ y ≠ ⊤) :
    - (x - y) = - x + y := by
  rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all

Negation of Difference Equals Sum of Negations in Extended Reals

Informal description

For any extended real numbers $x$ and $y$ such that either $x \neq -\infty$ or $y \neq -\infty$, and either $x \neq \infty$ or $y \neq \infty$, the negation of their difference equals the sum of the negation of $x$ and $y$, i.e., $-(x - y) = -x + y$.

EReal.bot_sub theorem

(x : EReal) : ⊥ - x = ⊥

Full source

@[simp]
theorem bot_sub (x : EReal) : ⊥ - x = ⊥ :=
  bot_add x

Subtraction from Negative Infinity in Extended Reals Yields Negative Infinity

Informal description

For any extended real number $x \in \mathbb{EReal}$, the subtraction of $x$ from $-\infty$ (denoted as $\bot$) yields $-\infty$, i.e., $-\infty - x = -\infty$.

EReal.sub_top theorem

(x : EReal) : x - ⊤ = ⊥

Full source

@[simp]
theorem sub_top (x : EReal) : x - ⊤ = ⊥ :=
  add_bot x

Subtraction of Infinity in Extended Real Numbers Yields Negative Infinity

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the subtraction $x - \infty$ equals $-\infty$, i.e., $x - \infty = -\infty$.

EReal.top_sub_bot theorem

: (⊤ : EReal) - ⊥ = ⊤

Full source

@[simp]
theorem top_sub_bot : (⊤ : EReal) - ⊥ = ⊤ :=
  rfl

Subtraction Identity: $\infty - (-\infty) = \infty$ in Extended Reals

Informal description

For the extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the subtraction of $-\infty$ from $\infty$ equals $\infty$, i.e., $\infty - (-\infty) = \infty$.

EReal.top_sub_coe theorem

(x : ℝ) : (⊤ : EReal) - x = ⊤

Full source

@[simp]
theorem top_sub_coe (x : ℝ) : (⊤ : EReal) - x = ⊤ :=
  rfl

Subtraction of Real from Infinity in Extended Reals Yields Infinity

Informal description

For any real number $x \in \mathbb{R}$, the subtraction of $x$ from positive infinity $\infty$ in the extended real numbers $\overline{\mathbb{R}}$ equals $\infty$, i.e., $\infty - x = \infty$.

EReal.coe_sub_bot theorem

(x : ℝ) : (x : EReal) - ⊥ = ⊤

Full source

@[simp]
theorem coe_sub_bot (x : ℝ) : (x : EReal) - ⊥ = ⊤ :=
  rfl

Subtraction of Negative Infinity from Real in Extended Reals Yields Positive Infinity

Informal description

For any real number $x \in \mathbb{R}$, the subtraction of $-\infty$ (denoted as $\bot$) from $x$ in the extended real numbers $\overline{\mathbb{R}}$ equals $+\infty$ (denoted as $\top$), i.e., $x - (-\infty) = +\infty$.

EReal.sub_bot theorem

{x : EReal} (h : x ≠ ⊥) : x - ⊥ = ⊤

Full source

@[simp]
lemma sub_bot {x : EReal} (h : x ≠ ⊥) : x - ⊥ = ⊤ := by
  cases x <;> tauto

Subtraction of Negative Infinity from Non-Negative-Infinity Extended Real Yields Positive Infinity

Informal description

For any extended real number $x \neq -\infty$, the subtraction $x - (-\infty)$ equals $+\infty$.

EReal.top_sub theorem

{x : EReal} (hx : x ≠ ⊤) : ⊤ - x = ⊤

Full source

@[simp]
lemma top_sub {x : EReal} (hx : x ≠ ⊤) : ⊤ - x = ⊤ := by
  cases x <;> tauto

Subtraction from Infinity in Extended Reals: $\infty - x = \infty$ for $x \neq \infty$

Informal description

For any extended real number $x \neq \infty$, the subtraction $\infty - x$ equals $\infty$.

EReal.sub_self theorem

{x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0

Full source

@[simp]
lemma sub_self {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) : x - x = 0 := by
  cases x <;> simp_all [← coe_sub]

Subtraction of Extended Real from Itself Yields Zero

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ such that $x \neq +\infty$ and $x \neq -\infty$, the subtraction $x - x$ equals $0$.

EReal.sub_self_le_zero theorem

{x : EReal} : x - x ≤ 0

Full source

lemma sub_self_le_zero {x : EReal} : x - x ≤ 0 := by
  cases x <;> simp

Nonpositivity of Self-Subtraction in Extended Reals: $x - x \leq 0$

Informal description

For any extended real number $x \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the subtraction $x - x$ is less than or equal to $0$, i.e., $x - x \leq 0$.

EReal.sub_nonneg theorem

{x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x

Full source

lemma sub_nonneg {x y : EReal} (h_top : x ≠ ⊤x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥x ≠ ⊥ ∨ y ≠ ⊥) :
    0 ≤ x - y ↔ y ≤ x := by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

Nonnegativity of Subtraction in Extended Reals: $0 \leq x - y \leftrightarrow y \leq x$

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$ such that either $x \neq +\infty$ or $y \neq +\infty$, and either $x \neq -\infty$ or $y \neq -\infty$, the inequality $0 \leq x - y$ holds if and only if $y \leq x$.

EReal.sub_nonpos theorem

{x y : EReal} : x - y ≤ 0 ↔ x ≤ y

Full source

lemma sub_nonpos {x y : EReal} : x - y ≤ 0 ↔ x ≤ y := by
  cases x <;> cases y <;> simp [← EReal.coe_sub]

Nonpositivity of Subtraction in Extended Reals: $x - y \leq 0 \leftrightarrow x \leq y$

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the inequality $x - y \leq 0$ holds if and only if $x \leq y$.

EReal.sub_pos theorem

{x y : EReal} : 0 < x - y ↔ y < x

Full source

lemma sub_pos {x y : EReal} : 0 < x - y ↔ y < x := by
  cases x <;> cases y <;> simp [← EReal.coe_sub]

Positivity of Subtraction in Extended Reals: $0 < x - y \leftrightarrow y < x$

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the difference $x - y$ is positive if and only if $y < x$, i.e., $0 < x - y \leftrightarrow y < x$.

EReal.sub_neg theorem

{x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) : x - y < 0 ↔ x < y

Full source

lemma sub_neg {x y : EReal} (h_top : x ≠ ⊤x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥x ≠ ⊥ ∨ y ≠ ⊥) :
    x - y < 0 ↔ x < y := by
  cases x <;> cases y <;> simp_all [← EReal.coe_sub]

Negativity of Subtraction in Extended Reals: $x - y < 0 \leftrightarrow x < y$ under Non-Infinite Conditions

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, if either $x \neq +\infty$ or $y \neq +\infty$, and either $x \neq -\infty$ or $y \neq -\infty$, then the difference $x - y$ is negative if and only if $x < y$, i.e., $x - y < 0 \leftrightarrow x < y$.

EReal.sub_le_sub theorem

{x y z t : EReal} (h : x ≤ y) (h' : t ≤ z) : x - z ≤ y - t

Full source

theorem sub_le_sub {x y z t : EReal} (h : x ≤ y) (h' : t ≤ z) : x - z ≤ y - t :=
  add_le_add h (neg_le_neg_iff.2 h')

Monotonicity of Subtraction in Extended Reals: $x \leq y$ and $t \leq z$ implies $x - z \leq y - t$

Informal description

For any extended real numbers $x, y, z, t \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, if $x \leq y$ and $t \leq z$, then $x - z \leq y - t$.

EReal.sub_lt_sub_of_lt_of_le theorem

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

Full source

theorem 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 :=
  add_lt_add_of_lt_of_le h (neg_le_neg_iff.2 h') (by simp [ht]) (by simp [hz])

Strict Inequality Preservation under Subtraction with Bounded Extended Reals

Informal description

For any extended real numbers $x, y, z, t \in \overline{\mathbb{R}}$ such that $x < y$, $z \leq t$, $z \neq -\infty$, and $t \neq +\infty$, it holds that $x - t < y - z$.

EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal theorem

(x : ℝ) : (x : EReal) = Real.toNNReal x - Real.toNNReal (-x)

Full source

theorem coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (x : ℝ) :
    (x : EReal) = Real.toNNReal x - Real.toNNReal (-x) := by
  rcases le_total 0 x with (h | h)
  · lift x to ℝ≥0 using h
    rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero,
      coe_ennreal_zero, sub_zero]
    rfl
  · rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
      Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]
    exact neg_nonneg.2 h

Extended Real Coercion as Difference of Non-Negative Projections

Informal description

For any real number $x$, the extended real number obtained by coercing $x$ is equal to the difference between the non-negative real projection of $x$ and the non-negative real projection of $-x$, i.e., $(x : \overline{\mathbb{R}}) = \text{toNNReal}(x) - \text{toNNReal}(-x)$.

EReal.toReal_sub theorem

 {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) : toReal (x - y) = toReal x - toReal y

Full source

theorem toReal_sub {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
    toReal (x - y) = toReal x - toReal y := by
  lift x to ℝ using ⟨hx, h'x⟩
  lift y to ℝ using ⟨hy, h'y⟩
  rfl

Real Projection of Subtraction for Finite Extended Real Numbers

Informal description

For any extended real numbers $x$ and $y$ such that $x$ is neither $\infty$ nor $-\infty$ and $y$ is neither $\infty$ nor $-\infty$, the real-valued projection of their difference $x - y$ equals the difference of their real-valued projections, i.e., $\text{toReal}(x - y) = \text{toReal}(x) - \text{toReal}(y)$.

EReal.toENNReal_sub theorem

{x y : EReal} (hy : 0 ≤ y) : (x - y).toENNReal = x.toENNReal - y.toENNReal

Full source

lemma toENNReal_sub {x y : EReal} (hy : 0 ≤ y) :
    (x - y).toENNReal = x.toENNReal - y.toENNReal := by
  induction x <;> induction y <;> try {· simp_all [zero_tsub, ENNReal.sub_top]}
  rename_i x y
  by_cases hxy : x ≤ y
  · rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]
    exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm
  · rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe,
      ofReal_sub x (EReal.coe_nonneg.mp hy)]
    simp

Projection of Subtraction to Extended Non-Negative Reals for Non-Negative $y$

Informal description

For any extended real numbers $x$ and $y$ with $y \geq 0$, the extended non-negative real projection of the difference $x - y$ equals the difference of the extended non-negative real projections of $x$ and $y$, i.e., $\text{toENNReal}(x - y) = \text{toENNReal}(x) - \text{toENNReal}(y)$.

EReal.add_sub_cancel_right theorem

{a : EReal} {b : Real} : a + b - b = a

Full source

lemma add_sub_cancel_right {a : EReal} {b : Real} : a + b - b = a := by
  cases a <;> norm_cast
  exact _root_.add_sub_cancel_right _ _

Right Cancellation of Addition and Subtraction for Extended Real Numbers

Informal description

For any extended real number $a$ and any real number $b$, the equality $(a + b) - b = a$ holds.

EReal.add_sub_cancel_left theorem

{a : EReal} {b : Real} : b + a - b = a

Full source

lemma add_sub_cancel_left {a : EReal} {b : Real} : b + a - b = a := by
  rw [add_comm, EReal.add_sub_cancel_right]

Left Cancellation of Addition and Subtraction for Extended Real Numbers

Informal description

For any extended real number $a$ and any real number $b$, the equality $(b + a) - b = a$ holds.

EReal.sub_add_cancel theorem

{a : EReal} {b : Real} : a - b + b = a

Full source

lemma sub_add_cancel {a : EReal} {b : Real} : a - b + b = a := by
  rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]

Subtraction-Add Cancellation for Extended Real Numbers

Informal description

For any extended real number $a$ and any real number $b$, the equality $(a - b) + b = a$ holds.

EReal.sub_add_cancel_right theorem

{a : EReal} {b : Real} : b - (a + b) = -a

Full source

lemma sub_add_cancel_right {a : EReal} {b : Real} : b - (a + b) = -a := by
  cases a <;> norm_cast
  exact _root_.sub_add_cancel_right _ _

Subtraction-Add Cancellation Identity for Extended Real Numbers

Informal description

For any extended real number $a$ and any real number $b$, we have $b - (a + b) = -a$.

EReal.sub_add_cancel_left theorem

{a : EReal} {b : Real} : b - (b + a) = -a

Full source

lemma sub_add_cancel_left {a : EReal} {b : Real} : b - (b + a) = -a := by
  rw [add_comm, sub_add_cancel_right]

Left Subtraction-Add Cancellation Identity for Extended Real Numbers

Informal description

For any extended real number $a$ and any real number $b$, we have $b - (b + a) = -a$.

EReal.le_sub_iff_add_le theorem

{a b c : EReal} (hb : b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤ ∨ c ≠ ⊤) : a ≤ c - b ↔ a + b ≤ c

Full source

lemma le_sub_iff_add_le {a b c : EReal} (hb : b ≠ ⊥b ≠ ⊥ ∨ c ≠ ⊥) (ht : b ≠ ⊤b ≠ ⊤ ∨ c ≠ ⊤) :
    a ≤ c - b ↔ a + b ≤ c := by
  induction b with
  | bot =>
    simp only [ne_eq, not_true_eq_false, false_or] at hb
    simp only [sub_bot hb, le_top, add_bot, bot_le]
  | coe b =>
    rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
  | top =>
    simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
    refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
    by_contra ha
    exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Inequality Relating Subtraction and Addition in Extended Reals: $a \leq c - b \leftrightarrow a + b \leq c$

Informal description

For any extended real numbers $a, b, c \in \mathbb{EReal}$ such that either $b \neq -\infty$ or $c \neq -\infty$, and either $b \neq \infty$ or $c \neq \infty$, the inequality $a \leq c - b$ holds if and only if $a + b \leq c$.

EReal.sub_le_iff_le_add theorem

{a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : a - b ≤ c ↔ a ≤ c + b

Full source

lemma sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤b ≠ ⊤ ∨ c ≠ ⊥) :
    a - b ≤ c ↔ a ≤ c + b := by
  suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
  refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa

Subtraction-Inequality Equivalence in Extended Reals: $a - b \leq c \leftrightarrow a \leq c + b$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that either $b \neq -\infty$ or $c \neq \infty$, and either $b \neq \infty$ or $c \neq -\infty$, the inequality $a - b \leq c$ holds if and only if $a \leq c + b$.

EReal.lt_sub_iff_add_lt theorem

{a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : c < a - b ↔ c + b < a

Full source

protected theorem lt_sub_iff_add_lt {a b c : EReal} (h₁ : b ≠ ⊥b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤b ≠ ⊤ ∨ c ≠ ⊥) :
    c < a - b ↔ c + b < a :=
  lt_iff_lt_of_le_iff_le (sub_le_iff_le_add h₁ h₂)

Strict Inequality Equivalence for Subtraction in Extended Reals: $c < a - b \leftrightarrow c + b < a$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that either $b \neq -\infty$ or $c \neq \infty$, and either $b \neq \infty$ or $c \neq -\infty$, the strict inequality $c < a - b$ holds if and only if $c + b < a$.

EReal.sub_le_of_le_add theorem

{a b c : EReal} (h : a ≤ b + c) : a - c ≤ b

Full source

theorem sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) : a - c ≤ b := by
  induction c with
  | bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
  | coe c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
  | top => simp only [sub_top, bot_le]

Subtraction Inequality from Addition Inequality in Extended Reals

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a \leq b + c$, then $a - c \leq b$.

EReal.sub_le_of_le_add' theorem

{a b c : EReal} (h : a ≤ b + c) : a - b ≤ c

Full source

/-- See also `EReal.sub_le_of_le_add`. -/
theorem sub_le_of_le_add' {a b c : EReal} (h : a ≤ b + c) : a - b ≤ c :=
  sub_le_of_le_add (add_comm b c ▸ h)

Subtraction Inequality from Addition Inequality in Extended Reals (Symmetric Version)

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a \leq b + c$, then $a - b \leq c$.

EReal.add_le_of_le_sub theorem

{a b c : EReal} (h : a ≤ b - c) : a + c ≤ b

Full source

lemma add_le_of_le_sub {a b c : EReal} (h : a ≤ b - c) : a + c ≤ b := by
  rw [← neg_neg c]
  exact sub_le_of_le_add h

Addition Inequality from Subtraction Inequality in Extended Reals

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a \leq b - c$, then $a + c \leq b$.

EReal.sub_lt_iff theorem

{a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤ ∨ c ≠ ⊤) : c - b < a ↔ c < a + b

Full source

lemma sub_lt_iff {a b c : EReal} (h₁ : b ≠ ⊥b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤b ≠ ⊤ ∨ c ≠ ⊤) :
    c - b < a ↔ c < a + b :=
  lt_iff_lt_of_le_iff_le (le_sub_iff_add_le h₁ h₂)

Inequality Relating Subtraction and Addition in Extended Reals: $c - b < a \leftrightarrow c < a + b$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that either $b \neq -\infty$ or $c \neq -\infty$, and either $b \neq \infty$ or $c \neq \infty$, the inequality $c - b < a$ holds if and only if $c < a + b$.

EReal.add_lt_of_lt_sub theorem

{a b c : EReal} (h : a < b - c) : a + c < b

Full source

lemma add_lt_of_lt_sub {a b c : EReal} (h : a < b - c) : a + c < b := by
  contrapose! h
  exact sub_le_of_le_add h

Addition Preserves Strict Inequality Under Subtraction in Extended Reals

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a < b - c$, then $a + c < b$.

EReal.sub_lt_of_lt_add theorem

{a b c : EReal} (h : a < b + c) : a - c < b

Full source

lemma sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) : a - c < b :=
  add_lt_of_lt_sub <| by rwa [sub_eq_add_neg, neg_neg]

Subtraction Preserves Strict Inequality Under Addition in Extended Reals

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a < b + c$, then $a - c < b$.

EReal.sub_lt_of_lt_add' theorem

{a b c : EReal} (h : a < b + c) : a - b < c

Full source

/-- See also `EReal.sub_lt_of_lt_add`. -/
lemma sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) : a - b < c :=
  sub_lt_of_lt_add <| by rwa [add_comm]

Subtraction preserves strict inequality under addition in extended reals (variant)

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, if $a < b + c$, then $a - b < c$.

EReal.le_of_forall_lt_iff_le theorem

{x y : EReal} : (∀ z : ℝ, x < z → y ≤ z) ↔ y ≤ x

Full source

lemma le_of_forall_lt_iff_le {x y : EReal} : (∀ z : ℝ, x < z → y ≤ z) ↔ y ≤ x := by
  refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
  rw [WithTop.forall]
  aesop

Characterization of Extended Real Order via Real Numbers (Upper Version)

Informal description

For any extended real numbers $x$ and $y$, the following are equivalent: 1. For every real number $z$, if $x < z$ then $y \leq z$ 2. $y \leq x$ In other words, $y$ is less than or equal to $x$ if and only if every real number greater than $x$ is also greater than or equal to $y$.

EReal.ge_of_forall_gt_iff_ge theorem

{x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x

Full source

lemma ge_of_forall_gt_iff_ge {x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x := by
  refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
  rw [WithTop.forall]
  aesop

Characterization of Extended Real Order via Real Numbers

Informal description

For any extended real numbers $x$ and $y$, the following are equivalent: 1. For every real number $z$, if $z < y$ then $z \leq x$ 2. $y \leq x$ In other words, $y$ is less than or equal to $x$ if and only if every real number less than $y$ is also less than or equal to $x$.

EReal.add_le_of_forall_lt theorem

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

Full source

lemma add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c := by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd
  exact hd.le.trans (h _ ha' _ hb')

Addition Upper Bound in Extended Reals via Pointwise Conditions

Informal description

For extended real numbers $a, b, c \in \mathbb{EReal}$, if for all $a' < a$ and $b' < b$ we have $a' + b' \leq c$, then $a + b \leq c$.

EReal.le_add_of_forall_gt theorem

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

Full source

lemma le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤a ≠ ⊤ ∨ b ≠ ⊥)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b := by
  rw [← neg_le_neg_iff, neg_add h₁ h₂]
  refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_
  rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]
  exact h _ (EReal.lt_neg_of_lt_neg ha') _ (EReal.lt_neg_of_lt_neg hb')

Lower Bound on Sum in Extended Reals via Pointwise Conditions

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, if either $a \neq -\infty$ or $b \neq \infty$, and either $a \neq \infty$ or $b \neq -\infty$, and for all $a' > a$ and $b' > b$ we have $c \leq a' + b'$, then $c \leq a + b$.

ENNReal.toEReal_sub theorem

{x y : ℝ≥0∞} (hy_top : y ≠ ∞) (h_le : y ≤ x) : (x - y).toEReal = x.toEReal - y.toEReal

Full source

lemma _root_.ENNReal.toEReal_sub {x y : ℝ≥0∞} (hy_top : y ≠ ∞) (h_le : y ≤ x) :
    (x - y).toEReal = x.toEReal - y.toEReal := by
  lift y to ℝ≥0 using hy_top
  cases x with
  | top => simp [coe_nnreal_eq_coe_real]
  | coe x =>
    simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

Compatibility of Subtraction with Casting from Extended Non-Negative Reals to Extended Reals

Informal description

For any extended non-negative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $y$ is finite ($y \neq \infty$) and $y \leq x$, the extended real number obtained by casting the subtraction $x - y$ is equal to the subtraction of the casted values, i.e., $(x - y).\text{toEReal} = x.\text{toEReal} - y.\text{EReal}$.

EReal.top_mul_top theorem

: (⊤ : EReal) * ⊤ = ⊤

Full source

@[simp] lemma top_mul_top : (⊤ : EReal) * ⊤ = ⊤ := rfl

Product of Positive Infinity with Itself in Extended Reals

Informal description

The product of the extended real number $\top$ (positive infinity) with itself is $\top$, i.e., $\top \cdot \top = \top$ in the extended real numbers.

EReal.top_mul_bot theorem

: (⊤ : EReal) * ⊥ = ⊥

Full source

@[simp] lemma top_mul_bot : (⊤ : EReal) * ⊥ = ⊥ := rfl

Product of Positive and Negative Infinity in Extended Reals: $\top * \bot = \bot$

Informal description

In the extended real numbers $\overline{\mathbb{R}}$, the product of $+\infty$ and $-\infty$ is $-\infty$, i.e., $\top * \bot = \bot$.

EReal.bot_mul_top theorem

: (⊥ : EReal) * ⊤ = ⊥

Full source

@[simp] lemma bot_mul_top : (⊥ : EReal) * ⊤ = ⊥ := rfl

Product of Negative and Positive Infinity in Extended Reals

Informal description

The product of the extended real numbers $-\infty$ (denoted as $\bot$) and $+\infty$ (denoted as $\top$) is $-\infty$, i.e., $\bot \cdot \top = \bot$.

EReal.bot_mul_bot theorem

: (⊥ : EReal) * ⊥ = ⊤

Full source

@[simp] lemma bot_mul_bot : (⊥ : EReal) * ⊥ = ⊤ := rfl

Product of Negative Infinities in Extended Reals: $(-\infty) \cdot (-\infty) = +\infty$

Informal description

The product of the extended real numbers $-\infty$ and $-\infty$ is equal to $+\infty$, i.e., $(-\infty) \cdot (-\infty) = +\infty$.

EReal.coe_mul_top_of_pos theorem

{x : ℝ} (h : 0 < x) : (x : EReal) * ⊤ = ⊤

Full source

lemma coe_mul_top_of_pos {x : ℝ} (h : 0 < x) : (x : EReal) * ⊤ = ⊤ :=
  if_pos h

Multiplication of Positive Real with Infinity in Extended Reals

Informal description

For any real number $x > 0$, the product of $x$ (viewed as an extended real number) with $\infty$ equals $\infty$, i.e., $x \cdot \infty = \infty$.

EReal.coe_mul_top_of_neg theorem

{x : ℝ} (h : x < 0) : (x : EReal) * ⊤ = ⊥

Full source

lemma coe_mul_top_of_neg {x : ℝ} (h : x < 0) : (x : EReal) * ⊤ = ⊥ :=
  (if_neg h.not_lt).trans (if_neg h.ne)

Product of Negative Real and Infinity in Extended Reals

Informal description

For any real number $x < 0$, the product of $x$ (considered as an extended real number) and $\infty$ is equal to $-\infty$, i.e., $x \cdot \infty = -\infty$.

EReal.top_mul_coe_of_pos theorem

{x : ℝ} (h : 0 < x) : (⊤ : EReal) * x = ⊤

Full source

lemma top_mul_coe_of_pos {x : ℝ} (h : 0 < x) : (⊤ : EReal) * x = ⊤ :=
  if_pos h

Multiplication of Positive Infinity by Positive Real Number Yields Positive Infinity

Informal description

For any real number $x$ such that $0 < x$, the product of $\top$ (the positive infinity in extended real numbers) and $x$ is $\top$, i.e., $\top \cdot x = \top$.

EReal.top_mul_coe_of_neg theorem

{x : ℝ} (h : x < 0) : (⊤ : EReal) * x = ⊥

Full source

lemma top_mul_coe_of_neg {x : ℝ} (h : x < 0) : (⊤ : EReal) * x = ⊥ :=
  (if_neg h.not_lt).trans (if_neg h.ne)

Multiplication of Infinity by Negative Real Yields Negative Infinity

Informal description

For any real number $x$ such that $x < 0$, the product of $\infty$ and $x$ in the extended real numbers is $-\infty$, i.e., $\infty \cdot x = -\infty$.

EReal.mul_top_of_pos theorem

: ∀ {x : EReal}, 0 < x → x * ⊤ = ⊤

Full source

lemma mul_top_of_pos : ∀ {x : EReal}, 0 < x → x * ⊤ = ⊤
  | ⊥, h => absurd h not_lt_bot
  | (x : ℝ), h => coe_mul_top_of_pos (EReal.coe_pos.1 h)
  | ⊤, _ => rfl

Multiplication of Positive Extended Real with Infinity Yields Infinity

Informal description

For any extended real number $x$ such that $0 < x$, the product of $x$ with positive infinity $\top$ is $\top$, i.e., $x \cdot \top = \top$.

EReal.mul_top_of_neg theorem

: ∀ {x : EReal}, x < 0 → x * ⊤ = ⊥

Full source

lemma mul_top_of_neg : ∀ {x : EReal}, x < 0 → x * ⊤ = ⊥
  | ⊥, _ => rfl
  | (x : ℝ), h => coe_mul_top_of_neg (EReal.coe_neg'.1 h)
  | ⊤, h => absurd h not_top_lt

Negative Extended Real Multiplied by Infinity Yields Negative Infinity: $x < 0 \implies x \cdot \top = \bot$

Informal description

For any extended real number $x$ such that $x < 0$, the product of $x$ with positive infinity $\top$ is negative infinity $\bot$, i.e., $x \cdot \top = \bot$.

EReal.top_mul_of_pos theorem

{x : EReal} (h : 0 < x) : ⊤ * x = ⊤

Full source

lemma top_mul_of_pos {x : EReal} (h : 0 < x) : ⊤ * x = ⊤ := by
  rw [EReal.mul_comm]
  exact mul_top_of_pos h

Multiplication of Infinity with Positive Extended Real Yields Infinity: $\top \cdot x = \top$ for $x > 0$

Informal description

For any extended real number $x$ such that $0 < x$, the product of positive infinity $\top$ with $x$ is $\top$, i.e., $\top \cdot x = \top$.

EReal.top_mul_of_neg theorem

{x : EReal} (h : x < 0) : ⊤ * x = ⊥

Full source

lemma top_mul_of_neg {x : EReal} (h : x < 0) : ⊤ * x = ⊥ := by
  rw [EReal.mul_comm]
  exact mul_top_of_neg h

Multiplication of Infinity by Negative Extended Real Yields Negative Infinity: $\top \cdot x = \bot$ for $x < 0$

Informal description

For any extended real number $x$ such that $x < 0$, the product of positive infinity $\top$ and $x$ is negative infinity $\bot$, i.e., $\top \cdot x = \bot$.

EReal.top_mul_coe_ennreal theorem

{x : ℝ≥0∞} (hx : x ≠ 0) : ⊤ * (x : EReal) = ⊤

Full source

lemma top_mul_coe_ennreal {x : ℝ≥0∞} (hx : x ≠ 0) : ⊤ * (x : EReal) = ⊤ :=
  top_mul_of_pos <| coe_ennreal_pos.mpr <| pos_iff_ne_zero.mpr hx

Multiplication of Infinity by Nonzero Extended Non-Negative Real Yields Infinity: $\top \cdot x = \top$ for $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}, x \neq 0$

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$, the product of positive infinity $\top$ and $x$ (viewed as an extended real number) is $\top$, i.e., $\top \cdot x = \top$.

EReal.coe_ennreal_mul_top theorem

{x : ℝ≥0∞} (hx : x ≠ 0) : (x : EReal) * ⊤ = ⊤

Full source

lemma coe_ennreal_mul_top {x : ℝ≥0∞} (hx : x ≠ 0) : (x : EReal) * ⊤ = ⊤ := by
  rw [EReal.mul_comm, top_mul_coe_ennreal hx]

Multiplication of Nonzero Extended Non-Negative Real by Infinity Yields Infinity: $x \cdot \top = \top$ for $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}, x \neq 0$

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$, the product of $x$ (viewed as an extended real number) and positive infinity $\top$ is $\top$, i.e., $x \cdot \top = \top$.

EReal.coe_mul_bot_of_pos theorem

{x : ℝ} (h : 0 < x) : (x : EReal) * ⊥ = ⊥

Full source

lemma coe_mul_bot_of_pos {x : ℝ} (h : 0 < x) : (x : EReal) * ⊥ = ⊥ :=
  if_pos h

Multiplication of Positive Real by Negative Infinity in Extended Reals

Informal description

For any real number $x > 0$, the product of $x$ (viewed as an extended real number) and $-\infty$ in the extended reals equals $-\infty$, i.e., $x \cdot (-\infty) = -\infty$.

EReal.coe_mul_bot_of_neg theorem

{x : ℝ} (h : x < 0) : (x : EReal) * ⊥ = ⊤

Full source

lemma coe_mul_bot_of_neg {x : ℝ} (h : x < 0) : (x : EReal) * ⊥ = ⊤ :=
  (if_neg h.not_lt).trans (if_neg h.ne)

Product of negative real with $-\infty$ in extended reals is $+\infty$

Informal description

For any real number $x < 0$, the product of $x$ (viewed as an extended real number) with $-\infty$ in the extended reals equals $+\infty$, i.e., $x \cdot (-\infty) = +\infty$.

EReal.bot_mul_coe_of_pos theorem

{x : ℝ} (h : 0 < x) : (⊥ : EReal) * x = ⊥

Full source

lemma bot_mul_coe_of_pos {x : ℝ} (h : 0 < x) : (⊥ : EReal) * x = ⊥ :=
  if_pos h

Multiplication of Negative Infinity by Positive Real in Extended Reals

Informal description

For any real number $x$ such that $0 < x$, the product of $-\infty$ (denoted as $\bot$) and $x$ in the extended real numbers $\overline{\mathbb{R}}$ equals $-\infty$, i.e., $\bot \cdot x = \bot$.

EReal.bot_mul_coe_of_neg theorem

{x : ℝ} (h : x < 0) : (⊥ : EReal) * x = ⊤

Full source

lemma bot_mul_coe_of_neg {x : ℝ} (h : x < 0) : (⊥ : EReal) * x = ⊤ :=
  (if_neg h.not_lt).trans (if_neg h.ne)

Multiplication of Negative Infinity with Negative Real Number Yields Positive Infinity in Extended Reals

Informal description

For any real number $x < 0$, the product of $-\infty$ (denoted as $\bot$ in `EReal`) and $x$ in the extended real numbers equals $+\infty$ (denoted as $\top$ in `EReal$), i.e., $\bot \cdot x = \top$.

EReal.mul_bot_of_pos theorem

: ∀ {x : EReal}, 0 < x → x * ⊥ = ⊥

Full source

lemma mul_bot_of_pos : ∀ {x : EReal}, 0 < x → x * ⊥ = ⊥
  | ⊥, h => absurd h not_lt_bot
  | (x : ℝ), h => coe_mul_bot_of_pos (EReal.coe_pos.1 h)
  | ⊤, _ => rfl

Multiplication of Positive Extended Real by Negative Infinity Yields Negative Infinity

Informal description

For any extended real number $x$ such that $0 < x$, the product of $x$ and $-\infty$ (denoted as $\bot$) in the extended reals equals $-\infty$, i.e., $x \cdot (-\infty) = -\infty$.

EReal.mul_bot_of_neg theorem

: ∀ {x : EReal}, x < 0 → x * ⊥ = ⊤

Full source

lemma mul_bot_of_neg : ∀ {x : EReal}, x < 0 → x * ⊥ = ⊤
  | ⊥, _ => rfl
  | (x : ℝ), h => coe_mul_bot_of_neg (EReal.coe_neg'.1 h)
  | ⊤, h => absurd h not_top_lt

Negative Extended Real Multiplied by Negative Infinity Yields Positive Infinity: $x < 0 \Rightarrow x \cdot (-\infty) = +\infty$

Informal description

For any extended real number $x < 0$, the product of $x$ with $-\infty$ (denoted $\bot$) in the extended reals equals $+\infty$ (denoted $\top$), i.e., $x \cdot (-\infty) = +\infty$.

EReal.bot_mul_of_pos theorem

{x : EReal} (h : 0 < x) : ⊥ * x = ⊥

Full source

lemma bot_mul_of_pos {x : EReal} (h : 0 < x) : ⊥ * x = ⊥ := by
  rw [EReal.mul_comm]
  exact mul_bot_of_pos h

Negative Infinity Multiplied by Positive Extended Real Yields Negative Infinity

Informal description

For any extended real number $x$ such that $0 < x$, the product of $-\infty$ (denoted as $\bot$) and $x$ equals $-\infty$, i.e., $-\infty \cdot x = -\infty$.

EReal.bot_mul_of_neg theorem

{x : EReal} (h : x < 0) : ⊥ * x = ⊤

Full source

lemma bot_mul_of_neg {x : EReal} (h : x < 0) : ⊥ * x = ⊤ := by
  rw [EReal.mul_comm]
  exact mul_bot_of_neg h

Negative Infinity Multiplied by Negative Extended Real Yields Positive Infinity: $-\infty \cdot x = +\infty$ for $x < 0$

Informal description

For any extended real number $x < 0$, the product of $-\infty$ (denoted $\bot$) and $x$ equals $+\infty$ (denoted $\top$), i.e., $-\infty \cdot x = +\infty$.

EReal.toReal_mul theorem

{x y : EReal} : toReal (x * y) = toReal x * toReal y

Full source

lemma toReal_mul {x y : EReal} : toReal (x * y) = toReal x * toReal y := by
  induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg h]

Real Part of Product Equals Product of Real Parts in Extended Reals

Informal description

For any extended real numbers $x$ and $y$, the real part of their product is equal to the product of their real parts, i.e., $\text{toReal}(x \cdot y) = \text{toReal}(x) \cdot \text{toReal}(y)$.

EReal.instNoZeroDivisors instance

: NoZeroDivisors EReal

Full source

instance : NoZeroDivisors EReal where
  eq_zero_or_eq_zero_of_mul_eq_zero := by
    intro a b h
    contrapose! h
    cases a <;> cases b <;> try {· simp_all [← EReal.coe_mul]}
    · rcases lt_or_gt_of_ne h.2 with (h | h)
        <;> simp [EReal.bot_mul_of_neg, EReal.bot_mul_of_pos, h]
    · rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]
    · rcases lt_or_gt_of_ne h.1 with (h | h)
        <;> simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]
    · rcases lt_or_gt_of_ne h.2 with (h | h)
        <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

No Zero Divisors in Extended Real Numbers

Informal description

The extended real numbers $\mathbb{EReal}$ form a structure with no zero divisors, meaning that for any two extended real numbers $x$ and $y$, if $x \cdot y = 0$, then either $x = 0$ or $y = 0$.

EReal.mul_pos_iff theorem

{a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Full source

lemma mul_pos_iff {a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp

Positivity of Product in Extended Reals: $0 < a \cdot b \leftrightarrow (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$

Informal description

For any extended real numbers $a$ and $b$, the product $a \cdot b$ is positive if and only if either both $a$ and $b$ are positive, or both $a$ and $b$ are negative. In other words, $0 < a \cdot b \leftrightarrow (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$.

EReal.mul_nonneg_iff theorem

{a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Full source

lemma mul_nonneg_iff {a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
  simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]
  rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h')
    <;> simp only [h, h', true_or, true_and, or_true, and_true] <;> tauto

Nonnegativity of Product in Extended Reals: $0 \leq a \cdot b \leftrightarrow (0 \leq a \land 0 \leq b) \lor (a \leq 0 \land b \leq 0)$

Informal description

For any extended real numbers $a$ and $b$, the product $a \cdot b$ is nonnegative if and only if either both $a$ and $b$ are nonnegative, or both $a$ and $b$ are nonpositive. In other words, $0 \leq a \cdot b \leftrightarrow (0 \leq a \land 0 \leq b) \lor (a \leq 0 \land b \leq 0)$.

EReal.mul_pos theorem

{a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Full source

/-- The product of two positive extended real numbers is positive. -/
lemma mul_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
  mul_pos_iff.mpr (Or.inl ⟨ha, hb⟩)

Positivity of Product of Positive Extended Reals: $0 < a, 0 < b \Rightarrow 0 < a \cdot b$

Informal description

For any extended real numbers $a$ and $b$, if $0 < a$ and $0 < b$, then their product satisfies $0 < a \cdot b$.

EReal.induction₂_neg_left theorem

 {P : EReal → EReal → Prop} (neg_left : ∀ {x y}, P x y → P (-x) y) (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x)
  (top_zero : P ⊤ 0) (top_neg : ∀ x : ℝ, 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, P x y

Full source

/-- 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`. -/
@[elab_as_elim]
lemma induction₂_neg_left {P : EReal → EReal → Prop} (neg_left : ∀ {x y}, P x y → P (-x) y)
    (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x)
    (top_zero : P ⊤ 0) (top_neg : ∀ x : ℝ, 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, P x y :=
  have : ∀ y, (∀ x : ℝ, 0 < x → P x y) → ∀ x : ℝ, x < 0 → P x y := fun _ h x hx =>
    neg_neg (x : EReal) ▸ neg_left <| h _ (neg_pos_of_neg hx)
  @induction₂ P top_top top_pos top_zero top_neg top_bot pos_top pos_bot zero_top
    coe_coe zero_bot (this _ pos_top) (this _ pos_bot) (neg_left top_top)
    (fun x hx => neg_left <| top_pos x hx) (neg_left top_zero)
    (fun x hx => neg_left <| top_neg x hx) (neg_left top_bot)

Induction Principle for Extended Real Numbers with Negation Symmetry

Informal description

Let $P : \overline{\mathbb{R}} \to \overline{\mathbb{R}} \to \mathrm{Prop}$ be a property of pairs of extended real numbers. Suppose that: 1. (Negation symmetry) For all $x, y \in \overline{\mathbb{R}}$, $P(x, y)$ implies $P(-x, y)$. 2. (Top cases) $P(\infty, \infty)$ holds, and for all real $x > 0$, $P(\infty, x)$ holds, $P(\infty, 0)$ holds, and for all real $x < 0$, $P(\infty, x)$ holds, and $P(\infty, -\infty)$ holds. 3. (Zero cases) $P(0, \infty)$ and $P(0, -\infty)$ hold. 4. (Positive cases) For all real $x > 0$, $P(x, \infty)$ and $P(x, -\infty)$ hold. 5. (Real cases) For all real $x, y \in \mathbb{R}$, $P(x, y)$ holds. Then $P(x, y)$ holds for all $x, y \in \overline{\mathbb{R}}$.

EReal.induction₂_symm_neg theorem

 {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x y → P y x) (neg_left : ∀ {x y}, 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, P x y

Full source

/-- 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`. -/
@[elab_as_elim]
lemma induction₂_symm_neg {P : EReal → EReal → Prop}
    (symm : ∀ {x y}, P x y → P y x)
    (neg_left : ∀ {x y}, 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, P x y :=
  have neg_right : ∀ {x y}, P x y → P x (-y) := fun h => symm <| neg_left <| symm h
  have : ∀ x, (∀ y : ℝ, 0 < y → P x y) → ∀ y : ℝ, y < 0 → P x y := fun _ h y hy =>
    neg_neg (y : EReal) ▸ neg_right (h _ (neg_pos_of_neg hy))
  @induction₂_neg_left P neg_left top_top top_pos top_zero (this _ top_pos) (neg_right top_top)
    (symm top_zero) (symm <| neg_left top_zero) (fun x hx => symm <| top_pos x hx)
    (fun x hx => symm <| neg_left <| top_pos x hx) coe_coe

Symmetric Induction Principle for Extended Real Numbers with Negation Symmetry

Informal description

Let $P : \overline{\mathbb{R}} \to \overline{\mathbb{R}} \to \mathrm{Prop}$ be a symmetric property (i.e., $P(x, y) \Rightarrow P(y, x)$ for all $x, y \in \overline{\mathbb{R}}$) that satisfies the following conditions: 1. (Negation symmetry) For all $x, y \in \overline{\mathbb{R}}$, $P(x, y)$ implies $P(-x, y)$. 2. (Top cases) $P(\infty, \infty)$ holds, and for all real $x > 0$, $P(\infty, x)$ holds, and $P(\infty, 0)$ holds. 3. (Real cases) For all real $x, y \in \mathbb{R}$, $P(x, y)$ holds. Then $P(x, y)$ holds for all $x, y \in \overline{\mathbb{R}}$.

EReal.neg_mul theorem

(x y : EReal) : -x * y = -(x * y)

Full source

protected lemma neg_mul (x y : EReal) : -x * y = -(x * y) := by
  induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]

Negation Distributes over Multiplication in Extended Reals: $-x \cdot y = -(x \cdot y)$

Informal description

For any extended real numbers $x$ and $y$, the product of $-x$ and $y$ equals the negation of the product of $x$ and $y$, i.e., $-x \cdot y = -(x \cdot y)$.

EReal.instHasDistribNeg instance

: HasDistribNeg EReal

Full source

instance : HasDistribNeg EReal where
  neg_mul := EReal.neg_mul
  mul_neg := fun x y => by
    rw [x.mul_comm, x.mul_comm]
    exact y.neg_mul x

Negation Distributes over Addition and Multiplication in Extended Reals

Informal description

The extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$ form a structure where negation distributes over multiplication, satisfying both: 1. $- (x * y) = (-x) * y = x * (-y)$ for all $x, y \in \overline{\mathbb{R}}$ 2. $- (x + y) = (-x) + (-y)$ for all $x, y \in \overline{\mathbb{R}}$ This means negation interacts compatibly with both the additive and multiplicative structures of the extended reals.

EReal.mul_neg_iff theorem

{a b : EReal} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Full source

lemma mul_neg_iff {a b : EReal} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b := by
  nth_rw 1 [← neg_zero]
  rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

Sign Rule for Product in Extended Reals: $a \cdot b < 0 \leftrightarrow (a > 0 \land b < 0) \lor (a < 0 \land b > 0)$

Informal description

For any extended real numbers $a$ and $b$, the product $a \cdot b$ is negative if and only if either $a$ is positive and $b$ is negative, or $a$ is negative and $b$ is positive. In other words, $a \cdot b < 0 \leftrightarrow (0 < a \land b < 0) \lor (a < 0 \land 0 < b)$.

EReal.mul_nonpos_iff theorem

{a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Full source

lemma mul_nonpos_iff {a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
  nth_rw 1 [← neg_zero]
  rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

Nonpositivity of Product in Extended Reals: $a \cdot b \leq 0 \leftrightarrow (0 \leq a \land b \leq 0) \lor (a \leq 0 \land 0 \leq b)$

Informal description

For any extended real numbers $a$ and $b$, the product $a \cdot b$ is nonpositive if and only if either: 1. $0 \leq a$ and $b \leq 0$, or 2. $a \leq 0$ and $0 \leq b$.

EReal.mul_eq_top theorem

 (a b : EReal) : a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤)

Full source

lemma mul_eq_top (a b : EReal) :
    a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤) := by
  induction a, b using EReal.induction₂_symm with
  | symm h =>
    rw [EReal.mul_comm, h]
    refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;>
    cases H with
      | inl h => exact Or.inr (Or.inl ⟨h.2, h.1⟩)
      | inr h => cases h with
        | inl h => exact Or.inl ⟨h.2, h.1⟩
        | inr h => cases h with
          | inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
          | inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    simpa only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
      EReal.coe_pos, or_self, iff_false, EReal.coe_mul] using EReal.coe_ne_top _
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp

Conditions for Product to be $+\infty$ in Extended Reals

Informal description

For extended real numbers $a$ and $b$, the product $a \cdot b$ equals $+\infty$ if and only if one of the following holds: 1. $a = -\infty$ and $b < 0$, 2. $a < 0$ and $b = -\infty$, 3. $a = +\infty$ and $0 < b$, 4. $0 < a$ and $b = +\infty$.

EReal.mul_ne_top theorem

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

Full source

lemma mul_ne_top (a b : EReal) :
    a * b ≠ ⊤a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) := by
  rw [ne_eq, mul_eq_top]
  -- push the negation while keeping the disjunctions, that is converting `¬(p ∧ q)` into `¬p ∨ ¬q`
  -- rather than `p → ¬q`, since we already have disjunctions in the rhs
  set_option push_neg.use_distrib true in push_neg
  rfl

Conditions for Product to be Finite in Extended Reals

Informal description

For extended real numbers $a$ and $b$, the product $a \cdot b$ is not equal to $+\infty$ if and only if all of the following conditions hold: 1. Either $a \neq -\infty$ or $0 \leq b$, 2. Either $0 \leq a$ or $b \neq -\infty$, 3. Either $a \neq +\infty$ or $b \leq 0$, 4. Either $a \leq 0$ or $b \neq +\infty$.

EReal.mul_eq_bot theorem

 (a b : EReal) : a * b = ⊥ ↔ (a = ⊥ ∧ 0 < b) ∨ (0 < a ∧ b = ⊥) ∨ (a = ⊤ ∧ b < 0) ∨ (a < 0 ∧ b = ⊤)

Full source

lemma mul_eq_bot (a b : EReal) :
    a * b = ⊥ ↔ (a = ⊥ ∧ 0 < b) ∨ (0 < a ∧ b = ⊥) ∨ (a = ⊤ ∧ b < 0) ∨ (a < 0 ∧ b = ⊤) := by
  rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff,
    neg_lt_comm, lt_neg_comm, neg_zero]
  tauto

Conditions for Product to be $-\infty$ in Extended Reals: $a \cdot b = -\infty$

Informal description

For extended real numbers $a$ and $b$, the product $a \cdot b$ equals $-\infty$ if and only if one of the following holds: 1. $a = -\infty$ and $0 < b$, 2. $0 < a$ and $b = -\infty$, 3. $a = +\infty$ and $b < 0$, 4. $a < 0$ and $b = +\infty$.

EReal.mul_ne_bot theorem

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

Full source

lemma mul_ne_bot (a b : EReal) :
    a * b ≠ ⊥a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) := by
  rw [ne_eq, mul_eq_bot]
  set_option push_neg.use_distrib true in push_neg
  rfl

Conditions for Finite Product in Extended Reals: $a \cdot b \neq -\infty$

Informal description

For extended real numbers $a$ and $b$, the product $a \cdot b$ is not equal to $-\infty$ if and only if all of the following conditions hold: 1. Either $a \neq -\infty$ or $b \leq 0$, 2. Either $a \leq 0$ or $b \neq -\infty$, 3. Either $a \neq +\infty$ or $0 \leq b$, 4. Either $0 \leq a$ or $b \neq +\infty$.

EReal.toENNReal_mul theorem

{x y : EReal} (hx : 0 ≤ x) : (x * y).toENNReal = x.toENNReal * y.toENNReal

Full source

/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the second variable, see `EReal.toENNReal_mul'`. -/
lemma toENNReal_mul {x y : EReal} (hx : 0 ≤ x) :
    (x * y).toENNReal = x.toENNReal * y.toENNReal := by
  induction x <;> induction y
    <;> try {· simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]}
  · rcases eq_or_lt_of_le hx with (hx | hx)
    · simp [← hx]
    · simp_all [mul_top_of_pos hx]
  · rename_i a
    rcases lt_trichotomy a 0 with (ha | ha | ha)
    · simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]
    · simp [ha]
    · simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]

Multiplicativity of Extended Nonnegative Real Conversion for Nonnegative Extended Reals: $(x \cdot y).\text{toENNReal} = x.\text{toENNReal} \cdot y.\text{toENNReal}$ when $x \geq 0$

Informal description

For any extended real numbers $x$ and $y$ with $x \geq 0$, the extended nonnegative real value of the product $x \cdot y$ equals the product of the extended nonnegative real values of $x$ and $y$, i.e., $(x \cdot y).\text{toENNReal} = x.\text{toENNReal} \cdot y.\text{toENNReal}$.

EReal.toENNReal_mul' theorem

{x y : EReal} (hy : 0 ≤ y) : (x * y).toENNReal = x.toENNReal * y.toENNReal

Full source

/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the first variable, see `EReal.toENNReal_mul`. -/
lemma toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) :
    (x * y).toENNReal = x.toENNReal * y.toENNReal := by
  rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]

Multiplicativity of Extended Nonnegative Real Conversion: $(x \cdot y).\text{toENNReal} = x.\text{toENNReal} \cdot y.\text{toENNReal}$ when $y \geq 0$

Informal description

For any extended real numbers $x$ and $y$ with $y \geq 0$, the extended nonnegative real value of the product $x \cdot y$ equals the product of the extended nonnegative real values of $x$ and $y$, i.e., $(x \cdot y).\text{toENNReal} = x.\text{toENNReal} \cdot y.\text{toENNReal}$.

EReal.right_distrib_of_nonneg theorem

{a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b) * c = a * c + b * c

Full source

lemma right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    (a + b) * c = a * c + b * c := by
  rcases eq_or_lt_of_le ha with (rfl | a_pos)
  · simp
  rcases eq_or_lt_of_le hb with (rfl | b_pos)
  · simp
  rcases lt_trichotomy c 0 with (c_neg | rfl | c_pos)
  · induction c
    · rw [mul_bot_of_pos a_pos, mul_bot_of_pos b_pos, mul_bot_of_pos (add_pos a_pos b_pos),
        add_bot ⊥]
    · induction a
      · exfalso; exact not_lt_bot a_pos
      · induction b
        · norm_cast
        · norm_cast; exact right_distrib _ _ _
        · norm_cast
          rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_neg c_neg, add_bot]
      · rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_neg c_neg, bot_add]
    · exfalso; exact not_top_lt c_neg
  · simp
  · induction c
    · exfalso; exact not_lt_bot c_pos
    · induction a
      · exfalso; exact not_lt_bot a_pos
      · induction b
        · norm_cast
        · norm_cast; exact right_distrib _ _ _
        · norm_cast
          rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_pos c_pos,
            add_top_of_ne_bot (coe_ne_bot _)]
      · rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_pos c_pos,
          top_add_of_ne_bot (ne_bot_of_gt (mul_pos b_pos c_pos))]
    · rw [mul_top_of_pos a_pos, mul_top_of_pos b_pos, mul_top_of_pos (add_pos a_pos b_pos),
        top_add_top]

Right Distributivity of Multiplication over Addition for Non-Negative Extended Reals

Informal description

For any extended real numbers $a, b, c$ such that $a \geq 0$ and $b \geq 0$, the right distributive property holds: $(a + b) \cdot c = a \cdot c + b \cdot c$.

EReal.left_distrib_of_nonneg theorem

{a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) : c * (a + b) = c * a + c * b

Full source

lemma left_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    c * (a + b) = c * a + c * b := by
  nth_rewrite 1 [EReal.mul_comm]; nth_rewrite 2 [EReal.mul_comm]; nth_rewrite 3 [EReal.mul_comm]
  exact right_distrib_of_nonneg ha hb

Left Distributivity of Multiplication over Addition for Non-Negative Extended Reals

Informal description

For any extended real numbers $a, b, c$ such that $a \geq 0$ and $b \geq 0$, the left distributive property holds: $c \cdot (a + b) = c \cdot a + c \cdot b$.

EReal.left_distrib_of_nonneg_of_ne_top theorem

{x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) : x * (y + z) = x * y + x * z

Full source

lemma 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 := by
  cases hx_nonneg.eq_or_gt with
  | inl hx0 => simp [hx0]
  | inr hx0 =>
  lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
  cases y <;> cases z <;>
    simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul];
    rw_mod_cast [mul_add]

Left Distributivity of Multiplication over Addition for Non-Negative Finite Extended Reals

Informal description

For any extended real number $x$ such that $0 \leq x < \infty$ and any extended real numbers $y, z$, the left distributive property holds: $x \cdot (y + z) = x \cdot y + x \cdot z$.

EReal.right_distrib_of_nonneg_of_ne_top theorem

{x : EReal} (hx_nonneg : 0 ≤ x) (hx_ne_top : x ≠ ⊤) (y z : EReal) : (y + z) * x = y * x + z * x

Full source

lemma 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 := by
  simpa only [EReal.mul_comm] using left_distrib_of_nonneg_of_ne_top hx_nonneg hx_ne_top y z

Right Distributivity of Multiplication over Addition for Non-Negative Finite Extended Reals

Informal description

For any extended real number $x$ such that $0 \leq x < \infty$ and any extended real numbers $y, z$, the right distributive property holds: $(y + z) \cdot x = y \cdot x + z \cdot x$.

EReal.nsmul_eq_mul theorem

(n : ℕ) (x : EReal) : n • x = n * x

Full source

@[simp]
lemma nsmul_eq_mul (n : ℕ) (x : EReal) : n • x = n * x := by
  induction n with
  | zero => rw [zero_smul, Nat.cast_zero, zero_mul]
  | succ n ih =>
    rw [succ_nsmul, ih, Nat.cast_succ]
    convert (EReal.right_distrib_of_nonneg _ _).symm <;> simp

Scalar Multiplication Equals Multiplication for Natural Numbers in Extended Reals

Informal description

For any natural number $n$ and any extended real number $x$, the scalar multiplication $n \cdot x$ is equal to the product $n \times x$.