Mathlib.Data.EReal.Inv

EReal.abs definition

: EReal → ℝ≥0∞

Full source

/-- The absolute value from `EReal` to `ℝ≥0∞`, mapping `⊥` and `⊤` to `⊤` and
a real `x` to `|x|`. -/
protected def abs : EReal → ℝ≥0∞
  | ⊥ => ⊤
  | ⊤ => ⊤
  | (x : ℝ) => ENNReal.ofReal |x|

Absolute value on extended real numbers

Informal description

The absolute value function from the extended real numbers $\overline{\mathbb{R}}$ to the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is defined as follows: - For $-\infty$ (denoted as `⊥`) and $+\infty$ (denoted as `⊤`), the absolute value is $\infty$. - For a real number $x \in \mathbb{R}$, the absolute value is the usual absolute value $|x|$ (mapped into $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via the embedding $\mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$).

EReal.abs_top theorem

: (⊤ : EReal).abs = ⊤

Full source

@[simp] theorem abs_top : (⊤ : EReal).abs = ⊤ := rfl

Absolute value of positive infinity in extended reals: $|+\infty| = \infty$

Informal description

The absolute value of $+\infty$ in the extended real numbers is $\infty$, i.e., $|+\infty| = \infty$.

EReal.abs_bot theorem

: (⊥ : EReal).abs = ⊤

Full source

@[simp] theorem abs_bot : (⊥ : EReal).abs = ⊤ := rfl

Absolute value of negative infinity in extended reals: $|-\infty| = \infty$

Informal description

The absolute value of $-\infty$ in the extended real numbers is $\infty$, i.e., $|-\infty| = \infty$.

EReal.abs_def theorem

(x : ℝ) : (x : EReal).abs = ENNReal.ofReal |x|

Full source

theorem abs_def (x : ℝ) : (x : EReal).abs = ENNReal.ofReal |x| := rfl

Absolute value of real numbers in extended reals: $|x|_{\overline{\mathbb{R}}} = |x|_{\mathbb{R}_{\geq 0}\cup\{\infty\}}$

Informal description

For any real number $x \in \mathbb{R}$, the absolute value of $x$ in the extended real numbers equals the extended non-negative real number obtained from the ordinary absolute value $|x|$, i.e., $|x|_{\overline{\mathbb{R}}} = \text{ENNReal.ofReal}(|x|)$.

EReal.abs_coe_lt_top theorem

(x : ℝ) : (x : EReal).abs < ⊤

Full source

theorem abs_coe_lt_top (x : ℝ) : (x : EReal).abs < ⊤ :=
  ENNReal.ofReal_lt_top

Finite Absolute Value for Real Numbers in Extended Reals

Informal description

For any real number $x \in \mathbb{R}$, the absolute value of $x$ in the extended real numbers is strictly less than infinity, i.e., $|x|_{\overline{\mathbb{R}}} < \infty$.

EReal.abs_eq_zero_iff theorem

{x : EReal} : x.abs = 0 ↔ x = 0

Full source

@[simp]
theorem abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0 := by
  induction x
  · simp only [abs_bot, ENNReal.top_ne_zero, bot_ne_zero]
  · simp only [abs_def, coe_eq_zero, ENNReal.ofReal_eq_zero, abs_nonpos_iff]
  · simp only [abs_top, ENNReal.top_ne_zero, top_ne_zero]

Zero Absolute Value Characterization in Extended Reals

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the absolute value of $x$ is zero if and only if $x$ is zero, i.e., $|x| = 0 \leftrightarrow x = 0$.

EReal.abs_zero theorem

: (0 : EReal).abs = 0

Full source

@[simp]
theorem abs_zero : (0 : EReal).abs = 0 := by rw [abs_eq_zero_iff]

Absolute Value of Zero in Extended Reals: $|0| = 0$

Informal description

The absolute value of the extended real number $0$ is $0$, i.e., $|0| = 0$.

EReal.coe_abs theorem

(x : ℝ) : ((x : EReal).abs : EReal) = (|x| : ℝ)

Full source

@[simp]
theorem coe_abs (x : ℝ) : ((x : EReal).abs : EReal) = (|x| : ℝ) := by
  rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]; rfl

Absolute Value Compatibility: $|x|_{\overline{\mathbb{R}}} = |x|_{\mathbb{R}}$ for Real $x$

Informal description

For any real number $x \in \mathbb{R}$, the absolute value of $x$ in the extended real numbers, when cast back to an extended real number, equals the extended real number obtained from the ordinary absolute value $|x|$ of $x$, i.e., $|x|_{\overline{\mathbb{R}}} = |x|_{\mathbb{R}}$.

EReal.abs_neg theorem

: ∀ x : EReal, (-x).abs = x.abs

Full source

@[simp]
protected theorem abs_neg : ∀ x : EReal, (-x).abs = x.abs
  | ⊤ => rfl
  | ⊥ => rfl
  | (x : ℝ) => by rw [abs_def, ← coe_neg, abs_def, abs_neg]

Absolute Value is Even on Extended Reals: $|-x| = |x|$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the absolute value of $-x$ equals the absolute value of $x$, i.e., $|-x| = |x|$.

EReal.abs_mul theorem

(x y : EReal) : (x * y).abs = x.abs * y.abs

Full source

@[simp]
theorem abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs := by
  induction x, y using induction₂_symm_neg with
  | top_zero => simp only [zero_mul, mul_zero, abs_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
    rw [Ne, abs_eq_zero_iff, coe_eq_zero]
    exact h.ne'
  | neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

Absolute Value Multiplicativity on Extended Reals: $|xy| = |x||y|$

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}}$, the absolute value of their product equals the product of their absolute values, i.e., $|x \cdot y| = |x| \cdot |y|$.

EReal.sign_top theorem

: sign (⊤ : EReal) = 1

Full source

theorem sign_top : sign (⊤ : EReal) = 1 := rfl

Sign of Positive Infinity in Extended Reals is One

Informal description

The sign function evaluated at the extended real number $\top$ (positive infinity) is equal to $1$, i.e., $\text{sign}(\top) = 1$.

EReal.sign_bot theorem

: sign (⊥ : EReal) = -1

Full source

theorem sign_bot : sign (⊥ : EReal) = -1 := rfl

Sign of Negative Infinity in Extended Reals is Minus One

Informal description

The sign function evaluated at the extended real number $\bot$ (negative infinity) is equal to $-1$, i.e., $\text{sign}(\bot) = -1$.

EReal.sign_coe theorem

(x : ℝ) : sign (x : EReal) = sign x

Full source

@[simp]
theorem sign_coe (x : ℝ) : sign (x : EReal) = sign x := by
  simp only [sign, OrderHom.coe_mk, EReal.coe_pos, EReal.coe_neg']

Sign Preservation under Real to Extended Real Embedding

Informal description

For any real number $x$, the sign function evaluated at the extended real number obtained by embedding $x$ into the extended reals is equal to the sign of $x$, i.e., $\text{sign}(x : \overline{\mathbb{R}}) = \text{sign}(x)$.

EReal.coe_coe_sign theorem

(x : SignType) : ((x : ℝ) : EReal) = x

Full source

@[simp, norm_cast]
theorem coe_coe_sign (x : SignType) : ((x : ℝ) : EReal) = x := by cases x <;> rfl

Preservation of Sign Type under Double Casting to Extended Reals

Informal description

For any element $x$ of the sign type (i.e., $-1$, $0$, or $1$), the extended real number obtained by first casting $x$ to a real number and then to an extended real number is equal to $x$ itself, i.e., $(x : \mathbb{R}) : \overline{\mathbb{R}} = x$.

EReal.sign_neg theorem

: ∀ x : EReal, sign (-x) = -sign x

Full source

@[simp] theorem sign_neg : ∀ x : EReal, sign (-x) = -sign x
  | ⊤ => rfl
  | ⊥ => rfl
  | (x : ℝ) => by rw [← coe_neg, sign_coe, sign_coe, Left.sign_neg]

Sign of Negation in Extended Real Numbers: $\text{sign}(-x) = -\text{sign}(x)$

Informal description

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

EReal.sign_mul theorem

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

Full source

@[simp]
theorem sign_mul (x y : EReal) : sign (x * y) = sign x * sign y := by
  induction x, y using induction₂_symm_neg with
  | top_zero => simp only [zero_mul, mul_zero, sign_zero]
  | top_top => rfl
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul, ENNReal.ofReal_mul (abs_nonneg _)]
  | top_pos _ h =>
    rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
  | neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]

Sign of Product Equals Product of Signs in Extended Reals

Informal description

For any extended real numbers $x$ and $y$ in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$, the sign of their product satisfies $\text{sign}(x \cdot y) = \text{sign}(x) \cdot \text{sign}(y)$.

EReal.sign_mul_abs theorem

: ∀ x : EReal, (sign x * x.abs : EReal) = x

Full source

@[simp] protected theorem sign_mul_abs : ∀ x : EReal, (sign x * x.abs : EReal) = x
  | ⊥ => by simp
  | ⊤ => by simp
  | (x : ℝ) => by rw [sign_coe, coe_abs, ← coe_coe_sign, ← coe_mul, sign_mul_abs]

Decomposition of Extended Real Number into Sign and Absolute Value: $\text{sign}(x) \cdot |x| = x$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the product of its sign and its absolute value equals $x$ itself, i.e., $\text{sign}(x) \cdot |x| = x$.

EReal.abs_mul_sign theorem

(x : EReal) : (x.abs * sign x : EReal) = x

Full source

@[simp] protected theorem abs_mul_sign (x : EReal) : (x.abs * sign x : EReal) = x := by
  rw [EReal.mul_comm, EReal.sign_mul_abs]

Absolute Value and Sign Decomposition: $|x| \cdot \text{sign}(x) = x$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the product of its absolute value and its sign equals $x$ itself, i.e., $|x| \cdot \text{sign}(x) = x$.

EReal.sign_eq_and_abs_eq_iff_eq theorem

{x y : EReal} : x.abs = y.abs ∧ sign x = sign y ↔ x = y

Full source

theorem sign_eq_and_abs_eq_iff_eq {x y : EReal} :
    x.abs = y.abs ∧ sign x = sign yx.abs = y.abs ∧ sign x = sign y ↔ x = y := by
  constructor
  · rintro ⟨habs, hsign⟩
    rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]
  · rintro rfl
    exact ⟨rfl, rfl⟩

Characterization of Equality in Extended Reals via Sign and Absolute Value

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$, the absolute values of $x$ and $y$ are equal and their signs are equal if and only if $x = y$. In other words, $|x| = |y| \land \text{sign}(x) = \text{sign}(y) \leftrightarrow x = y$.

EReal.le_iff_sign theorem

 {x y : EReal} :
  x ≤ y ↔
    sign x < sign y ∨
      sign x = SignType.neg ∧ sign y = SignType.neg ∧ y.abs ≤ x.abs ∨
        sign x = SignType.zero ∧ sign y = SignType.zero ∨ sign x = SignType.pos ∧ sign y = SignType.pos ∧ x.abs ≤ y.abs

Full source

theorem le_iff_sign {x y : EReal} :
    x ≤ y ↔ sign x < sign y ∨
      sign x = SignType.neg ∧ sign y = SignType.neg ∧ y.abs ≤ x.abs ∨
        sign x = SignType.zero ∧ sign y = SignType.zero ∨
          sign x = SignType.pos ∧ sign y = SignType.pos ∧ x.abs ≤ y.abs := by
  constructor
  · intro h
    refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
    rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
    cases hy : sign y <;> rw [hs, hy] at h ⊢
    · simp
    · left; simpa using h
    · right; right; simpa using h
  · rintro (h | h | h | h)
    · exact (sign.monotone.reflect_lt h).le
    all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]

Characterization of Extended Real Ordering via Signs and Absolute Values

Informal description

For any extended real numbers $x$ and $y$, the inequality $x \leq y$ holds if and only if one of the following conditions is satisfied: 1. The sign of $x$ is strictly less than the sign of $y$, or 2. Both $x$ and $y$ are negative and $|y| \leq |x|$, or 3. Both $x$ and $y$ are zero, or 4. Both $x$ and $y$ are positive and $|x| \leq |y|$. Here, the sign function $\text{sign}(x)$ takes values in $\{\text{neg}, \text{zero}, \text{pos}\}$ corresponding to negative, zero, and positive numbers respectively, with the ordering $\text{neg} < \text{zero} < \text{pos}$.

EReal.instCommMonoidWithZero instance

: CommMonoidWithZero EReal

Full source

instance : CommMonoidWithZero EReal :=
  { inferInstanceAs (MulZeroOneClass EReal) with
    mul_assoc := fun x y z => by
      rw [← sign_eq_and_abs_eq_iff_eq]
      simp only [mul_assoc, abs_mul, eq_self_iff_true, sign_mul, and_self_iff]
    mul_comm := EReal.mul_comm }

Commutative Monoid with Zero Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a commutative monoid with zero, where the multiplication operation is commutative, associative, has an identity element (1), and satisfies the property that any element multiplied by zero is zero.

EReal.instPosMulMono instance

: PosMulMono EReal

Full source

instance : PosMulMono EReal := posMulMono_iff_covariant_pos.2 <| .mk <| by
  rintro ⟨x, x0⟩ a b h
  simp only [le_iff_sign, EReal.sign_mul, sign_pos x0, one_mul, EReal.abs_mul] at h ⊢
  exact h.imp_right <| Or.imp (And.imp_right <| And.imp_right (mul_le_mul_left' · _)) <|
    Or.imp_right <| And.imp_right <| And.imp_right (mul_le_mul_left' · _)

Monotonicity of Left Multiplication by Nonnegative Extended Reals

Informal description

For the extended real numbers $\overline{\mathbb{R}}$, left multiplication by nonnegative elements is monotone. That is, for any $b \geq 0$ in $\overline{\mathbb{R}}$ and any $a_1 \leq a_2$ in $\overline{\mathbb{R}}$, we have $b \cdot a_1 \leq b \cdot a_2$.

EReal.instMulPosMono instance

: MulPosMono EReal

Full source

instance : MulPosMono EReal := posMulMono_iff_mulPosMono.1 inferInstance

Monotonicity of Right Multiplication by Nonnegative Extended Reals

Informal description

For the extended real numbers $\overline{\mathbb{R}}$, right multiplication by nonnegative elements is monotone. That is, for any $b \geq 0$ in $\overline{\mathbb{R}}$ and any $a_1 \leq a_2$ in $\overline{\mathbb{R}}$, we have $a_1 \cdot b \leq a_2 \cdot b$.

EReal.instPosMulReflectLT instance

: PosMulReflectLT EReal

Full source

instance : PosMulReflectLT EReal := PosMulMono.toPosMulReflectLT

Strict Order Reflection by Left Multiplication with Nonnegative Extended Reals

Informal description

For the extended real numbers $\overline{\mathbb{R}}$, left multiplication by nonnegative elements reflects the strict order. That is, for any $b \geq 0$ in $\overline{\mathbb{R}}$ and any $a_1, a_2 \in \overline{\mathbb{R}}$, if $b \cdot a_1 < b \cdot a_2$, then $a_1 < a_2$.

EReal.instMulPosReflectLT instance

: MulPosReflectLT EReal

Full source

instance : MulPosReflectLT EReal := MulPosMono.toMulPosReflectLT

Strict Order Reflection by Right Multiplication with Nonnegative Extended Reals

Informal description

For the extended real numbers $\overline{\mathbb{R}}$, right multiplication by nonnegative elements reflects the strict order. That is, for any $b \geq 0$ in $\overline{\mathbb{R}}$ and any $a_1, a_2 \in \overline{\mathbb{R}}$, if $a_1 \cdot b < a_2 \cdot b$, then $a_1 < a_2$.

EReal.mul_le_mul_of_nonpos_right theorem

{a b c : EReal} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

Full source

lemma mul_le_mul_of_nonpos_right {a b c : EReal} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c := by
  rw [mul_comm a c, mul_comm b c, ← neg_le_neg_iff, ← neg_mul c b, ← neg_mul c a]
  rw [← neg_zero, EReal.le_neg] at hc
  exact mul_le_mul_of_nonneg_left h hc

Monotonicity of Right Multiplication by Nonpositive Extended Reals: $c \leq 0 \implies (b \leq a \to a \cdot c \leq b \cdot c)$

Informal description

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

EReal.coe_pow theorem

(x : ℝ) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n

Full source

@[simp, norm_cast]
theorem coe_pow (x : ℝ) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n :=
  map_pow (⟨⟨(↑), coe_one⟩, coe_mul⟩ : ℝℝ →* EReal) _ _

Coercion of Real Powers to Extended Reals: $\overline{x^n} = (\overline{x})^n$

Informal description

For any real number $x$ and natural number $n$, the extended real number obtained by coercing $x^n$ is equal to the $n$-th power of the extended real number obtained by coercing $x$, i.e., $\overline{x^n} = (\overline{x})^n$.

EReal.coe_ennreal_pow theorem

(x : ℝ≥0∞) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n

Full source

@[simp, norm_cast]
theorem coe_ennreal_pow (x : ℝ≥0∞) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n :=
  map_pow (⟨⟨(↑), coe_ennreal_one⟩, coe_ennreal_mul⟩ : ℝ≥0∞ℝ≥0∞ →* EReal) _ _

Power of Extended Non-Negative Real Number Preserves Casting

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any natural number $n \in \mathbb{N}$, the extended real number obtained by casting $x^n$ to $\overline{\mathbb{R}}$ is equal to the $n$-th power of the extended real number obtained by casting $x$ to $\overline{\mathbb{R}}$. In symbols, $\overline{x^n} = (\overline{x})^n$.

EReal.exists_nat_ge_mul theorem

{a : EReal} (ha : a ≠ ⊤) (n : ℕ) : ∃ m : ℕ, a * n ≤ m

Full source

lemma exists_nat_ge_mul {a : EReal} (ha : a ≠ ⊤) (n : ℕ) :
    ∃ m : ℕ, a * n ≤ m :=
  match a with
  | ⊤ => ha.irrefl.rec
  | ⊥ => ⟨0, Nat.cast_zero (R := EReal) ▸ mul_nonpos_iff.2 (.inr ⟨bot_le, n.cast_nonneg'⟩)⟩
  | (a : ℝ) => by
    obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)
    use m
    rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]

Existence of Natural Number Upper Bound for Extended Real Multiplication

Informal description

For any extended real number $a \neq \top$ and any natural number $n$, there exists a natural number $m$ such that $a \cdot n \leq m$.

EReal.min_neg_neg theorem

(x y : EReal) : min (-x) (-y) = -max x y

Full source

lemma min_neg_neg (x y : EReal) : min (-x) (-y) = -max x y := by
  rcases le_total x y with (h | h) <;> simp_all

Min-Max Duality under Negation in Extended Reals

Informal description

For any extended real numbers $x$ and $y$, the minimum of $-x$ and $-y$ equals the negation of the maximum of $x$ and $y$, i.e., $$\min(-x, -y) = -\max(x, y).$$

EReal.max_neg_neg theorem

(x y : EReal) : max (-x) (-y) = -min x y

Full source

lemma max_neg_neg (x y : EReal) : max (-x) (-y) = -min x y := by
  rcases le_total x y with (h | h) <;> simp_all

Max-Min Duality under Negation in Extended Reals

Informal description

For any extended real numbers $x$ and $y$, the maximum of $-x$ and $-y$ equals the negation of the minimum of $x$ and $y$, i.e., $$\max(-x, -y) = -\min(x, y).$$

EReal.inv definition

: EReal → EReal

Full source

/-- Multiplicative inverse of an `EReal`. We choose `0⁻¹ = 0` to guarantee several good properties,
for instance `(a * b)⁻¹ = a⁻¹ * b⁻¹`. -/
protected def inv : EReal → EReal
  | ⊥ => 0
  | ⊤ => 0
  | (x : ℝ) => (x⁻¹ : ℝ)

Inverse function on extended real numbers

Informal description

The multiplicative inverse function on extended real numbers, defined as: - $(\bot)^{-1} = 0$ - $(\top)^{-1} = 0$ - For a real number $x$, $(x)^{-1}$ is the usual real inverse $x^{-1}$ This definition ensures properties like $(ab)^{-1} = a^{-1}b^{-1}$ hold for all extended reals.

EReal.instInv instance

: Inv (EReal)

Full source

instance : Inv (EReal) := ⟨EReal.inv⟩

Inversion Operation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{\bot, \top\}$ have an inversion operation defined by: - $(\bot)^{-1} = 0$ - $(\top)^{-1} = 0$ - For $x \in \mathbb{R}$, $x^{-1}$ is the usual multiplicative inverse in $\mathbb{R}$

EReal.instDivInvMonoid instance

: DivInvMonoid EReal

Full source

noncomputable instance : DivInvMonoid EReal where inv := EReal.inv

Division Involutive Monoid Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a division involutive monoid, where the division and inversion operations are defined as follows: - The inverse of $\bot$ (negative infinity) is $0$ - The inverse of $\top$ (positive infinity) is $0$ - For a real number $x$, the inverse is the usual real inverse $x^{-1}$ This structure extends the commutative monoid with zero structure on $\overline{\mathbb{R}}$ by adding well-defined division and inversion operations.

EReal.inv_bot theorem

: (⊥ : EReal)⁻¹ = 0

Full source

@[simp]
lemma inv_bot : (⊥ : EReal)⁻¹ = 0 := rfl

Inverse of Negative Infinity in Extended Reals: $(-\infty)^{-1} = 0$

Informal description

The inverse of the extended real number $-\infty$ (denoted $\bot$) is $0$, i.e., $(-\infty)^{-1} = 0$.

EReal.inv_top theorem

: (⊤ : EReal)⁻¹ = 0

Full source

@[simp]
lemma inv_top : (⊤ : EReal)⁻¹ = 0 := rfl

Inverse of Positive Infinity in Extended Reals: $(+\infty)^{-1} = 0$

Informal description

The inverse of the extended real number $+\infty$ (denoted $\top$) is $0$, i.e., $(+\infty)^{-1} = 0$.

EReal.coe_inv theorem

(x : ℝ) : (x⁻¹ : ℝ) = (x : EReal)⁻¹

Full source

lemma coe_inv (x : ℝ) : (x⁻¹ : ℝ) = (x : EReal)⁻¹ := rfl

Compatibility of Real Inversion with Extended Real Inversion: $(x^{-1} : \mathbb{R}) = (x : \overline{\mathbb{R}})^{-1}$

Informal description

For any real number $x$, the inverse of $x$ in the extended real numbers $\overline{\mathbb{R}}$ is equal to the extended real number obtained by casting the usual real inverse of $x$ to $\overline{\mathbb{R}}$. In other words, $(x^{-1} : \mathbb{R}) = (x : \overline{\mathbb{R}})^{-1}$.

EReal.inv_zero theorem

: (0 : EReal)⁻¹ = 0

Full source

@[simp]
lemma inv_zero : (0 : EReal)⁻¹ = 0 := by
  change (0 : ℝ)⁻¹ = (0 : EReal)
  rw [GroupWithZero.inv_zero, coe_zero]

Inverse of Zero in Extended Reals: $0^{-1} = 0$

Informal description

The inverse of the extended real number $0$ is $0$, i.e., $0^{-1} = 0$ in $\overline{\mathbb{R}}$.

EReal.instDivInvOneMonoid instance

: DivInvOneMonoid EReal

Full source

noncomputable instance : DivInvOneMonoid EReal where
  inv_one := by nth_rw 1 [← coe_one, ← coe_inv 1, _root_.inv_one, coe_one]

Division Involutive Monoid with One Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a division involutive monoid with one, where the division and inversion operations are defined as follows: - The inverse of $0$ is $0$ - The inverse of $\bot$ (negative infinity) is $0$ - The inverse of $\top$ (positive infinity) is $0$ - For a real number $x$, the inverse is the usual real inverse $x^{-1}$ This structure extends the division involutive monoid structure on $\overline{\mathbb{R}}$ by adding a well-defined multiplicative identity element.

EReal.inv_neg theorem

(a : EReal) : (-a)⁻¹ = -a⁻¹

Full source

lemma inv_neg (a : EReal) : (-a)⁻¹ = -a⁻¹ := by
  induction a
  · rw [neg_bot, inv_top, inv_bot, neg_zero]
  · rw [← coe_inv _, ← coe_neg _⁻¹, ← coe_neg _, ← coe_inv (-_)]
    exact EReal.coe_eq_coe_iff.2 _root_.inv_neg
  · rw [neg_top, inv_bot, inv_top, neg_zero]

Inverse of Negation in Extended Reals: $(-a)^{-1} = -a^{-1}$

Informal description

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

EReal.inv_inv theorem

{a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : (a⁻¹)⁻¹ = a

Full source

lemma inv_inv {a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : (a⁻¹)⁻¹ = a := by
  rw [← coe_toReal h' h, ← coe_inv a.toReal, ← coe_inv a.toReal⁻¹, _root_.inv_inv a.toReal]

Double Inversion Identity for Finite Extended Real Numbers: $(a^{-1})^{-1} = a$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$ that is neither $-\infty$ ($\bot$) nor $+\infty$ ($\top$), the double inverse of $a$ equals $a$ itself, i.e., $(a^{-1})^{-1} = a$.

EReal.mul_inv theorem

(a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Full source

lemma mul_inv (a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
  induction a, b using EReal.induction₂_symm with
  | top_top | top_zero | top_bot | zero_bot | bot_bot => simp
  | @symm a b h => rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]; exact h
  | top_pos x x_pos => rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
  | top_neg x x_neg => rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
  | pos_bot x x_pos => rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
  | coe_coe x y => rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
  | neg_bot x x_neg => rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Inverse of Product Equals Product of Inverses in Extended Reals: $(ab)^{-1} = a^{-1}b^{-1}$

Informal description

For any extended real numbers $a$ and $b$ in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, the inverse of their product equals the product of their inverses, i.e., $(a \cdot b)^{-1} = a^{-1} \cdot b^{-1}$.

EReal.sign_mul_inv_abs theorem

(a : EReal) : (sign a) * (a.abs : EReal)⁻¹ = a⁻¹

Full source

lemma sign_mul_inv_abs (a : EReal) : (sign a) * (a.abs : EReal)⁻¹ = a⁻¹ := by
  induction a with
  | bot | top => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, ← inv_neg, abs_def a,
        coe_ennreal_ofReal, max_eq_left (abs_nonneg a), ← coe_neg |a|, abs_of_neg a_neg, neg_neg]
    · rw [coe_zero, sign_zero, SignType.coe_zero, abs_zero, coe_ennreal_zero, inv_zero, mul_zero]
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

Inverse Decomposition via Sign and Absolute Value in Extended Reals: $\text{sign}(a) \cdot |a|^{-1} = a^{-1}$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the product of the sign of $a$ and the inverse of the absolute value of $a$ (as an extended real) equals the inverse of $a$, i.e., $\text{sign}(a) \cdot (|a|)^{-1} = a^{-1}$.

EReal.sign_mul_inv_abs' theorem

(a : EReal) : (sign a) * ((a.abs⁻¹ : ℝ≥0∞) : EReal) = a⁻¹

Full source

lemma sign_mul_inv_abs' (a : EReal) : (sign a) * ((a.abs⁻¹ : ℝ≥0∞) : EReal) = a⁻¹ := by
  induction a with
  | bot | top  => simp
  | coe a =>
    rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)
    · rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
        max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a||a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
        ← _root_.inv_neg, neg_neg]
    · simp
    · rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
        ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
          max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]
      congr
      exact abs_of_pos a_pos

Sign-Absolute-Inverse Identity for Extended Real Numbers: $\text{sign}(a) \cdot |a|^{-1} = a^{-1}$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the product of the sign of $a$ and the inverse of the absolute value of $a$ (interpreted as an extended non-negative real number and then cast back to $\overline{\mathbb{R}}$) equals the inverse of $a$, i.e., \[ (\text{sign}\, a) \cdot \left( (|a|^{-1} : \mathbb{R}_{\geq 0} \cup \{\infty\}) : \overline{\mathbb{R}} \right) = a^{-1}. \]

EReal.bot_lt_inv theorem

(x : EReal) : ⊥ < x⁻¹

Full source

lemma bot_lt_inv (x : EReal) : ⊥ < x⁻¹ := by
  cases x with
  | bot => exact inv_bot ▸ bot_lt_zero
  | top => exact EReal.inv_top ▸ bot_lt_zero
  | coe x => exact (coe_inv x).symm ▸ bot_lt_coe (x⁻¹)

Inverse of Extended Real Number is Above Negative Infinity: $x^{-1} > -\infty$

Informal description

For any extended real number $x \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, the inverse $x^{-1}$ is strictly greater than $-\infty$.

EReal.inv_lt_top theorem

(x : EReal) : x⁻¹ < ⊤

Full source

lemma inv_lt_top (x : EReal) : x⁻¹ < ⊤ := by
  cases x with
  | bot => exact inv_bot ▸ zero_lt_top
  | top => exact EReal.inv_top ▸ zero_lt_top
  | coe x => exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

Inverse of Extended Real Number is Below Positive Infinity: $x^{-1} < +\infty$

Informal description

For any extended real number $x \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, the inverse $x^{-1}$ is strictly less than $+\infty$.

EReal.inv_nonneg_of_nonneg theorem

{a : EReal} (h : 0 ≤ a) : 0 ≤ a⁻¹

Full source

lemma inv_nonneg_of_nonneg {a : EReal} (h : 0 ≤ a) : 0 ≤ a⁻¹ := by
  cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h

Nonnegativity of Inverse for Nonnegative Extended Reals: $0 \leq a \Rightarrow 0 \leq a^{-1}$

Informal description

For any extended real number $a \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, if $0 \leq a$, then the inverse $a^{-1}$ is nonnegative, i.e., $0 \leq a^{-1}$.

EReal.inv_nonpos_of_nonpos theorem

{a : EReal} (h : a ≤ 0) : a⁻¹ ≤ 0

Full source

lemma inv_nonpos_of_nonpos {a : EReal} (h : a ≤ 0) : a⁻¹ ≤ 0 := by
  cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h

Inverse of Nonpositive Extended Real is Nonpositive

Informal description

For any extended real number $a \in \overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$, if $a \leq 0$, then its inverse $a^{-1}$ is also nonpositive, i.e., $a^{-1} \leq 0$.

EReal.inv_pos_of_pos_ne_top theorem

{a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹

Full source

lemma inv_pos_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹ := by
  lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_pos_of_pos h

Positivity of Inverse for Positive Extended Reals Not Equal to Infinity

Informal description

For any extended real number $a$ such that $0 < a$ and $a \neq +\infty$, the inverse $a^{-1}$ is strictly positive, i.e., $0 < a^{-1}$.

EReal.inv_neg_of_neg_ne_bot theorem

{a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ < 0

Full source

lemma inv_neg_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ < 0 := by
  lift a to ℝ using ⟨ne_top_of_lt h, h'⟩
  rw [← coe_inv a]; norm_cast at *; exact inv_lt_zero.2 h

Inverse of Negative Extended Real is Negative (excluding $-\infty$)

Informal description

For any extended real number $a$ such that $a < 0$ and $a \neq -\infty$, the inverse of $a$ satisfies $a^{-1} < 0$.

EReal.inv_strictAntiOn theorem

: StrictAntiOn (fun (x : EReal) => x⁻¹) (Ioi 0)

Full source

lemma inv_strictAntiOn : StrictAntiOn (fun (x : EReal) => x⁻¹) (Ioi 0) := by
  intro a a_0 b b_0 a_b
  simp only [mem_Ioi] at *
  lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩
  match b with
  | ⊤ => exact inv_top ▸ inv_pos_of_pos_ne_top a_0 (coe_ne_top a)
  | ⊥ => exact (not_lt_bot b_0).rec
  | (b : ℝ) =>
    rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
    exact _root_.inv_strictAntiOn (EReal.coe_pos.1 a_0) (EReal.coe_pos.1 b_0)
      (EReal.coe_lt_coe_iff.1 a_b)

Strict Antitonicity of Inversion on Positive Extended Reals: $x^{-1} < y^{-1}$ for $0 < x < y$

Informal description

The inversion function $x \mapsto x^{-1}$ is strictly antitone on the set of positive extended real numbers, i.e., for any $x, y \in (0, \infty) \cup \{\top\}$ with $x < y$, we have $y^{-1} < x^{-1}$.

EReal.div_eq_inv_mul theorem

(a b : EReal) : a / b = b⁻¹ * a

Full source

protected lemma div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a := EReal.mul_comm a b⁻¹

Division as Inverse Multiplication in Extended Real Numbers

Informal description

For any extended real numbers $a$ and $b$, the division $a / b$ is equal to the product of the inverse of $b$ and $a$, i.e., $a / b = b^{-1} \cdot a$.

EReal.coe_div theorem

(a b : ℝ) : (a / b : ℝ) = (a : EReal) / (b : EReal)

Full source

lemma coe_div (a b : ℝ) : (a / b : ℝ) = (a : EReal) / (b : EReal) := rfl

Embedding Preserves Division: $(a / b : \mathbb{R}) = (a : \overline{\mathbb{R}}) / (b : \overline{\mathbb{R}})$

Informal description

For any real numbers $a$ and $b$, the division $a / b$ in $\mathbb{R}$ is equal to the division of their embeddings in the extended real numbers $\overline{\mathbb{R}}$, i.e., $(a / b : \mathbb{R}) = (a : \overline{\mathbb{R}}) / (b : \overline{\mathbb{R}})$.

EReal.natCast_div_le theorem

(m n : ℕ) : (m / n : ℕ) ≤ (m : EReal) / (n : EReal)

Full source

theorem natCast_div_le (m n : ℕ) :
    (m / n : ℕ) ≤ (m : EReal) / (n : EReal) := by
  rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_div,
    EReal.coe_le_coe_iff]
  exact Nat.cast_div_le

Natural Division Embedding Inequality in Extended Reals: $(m / n : \mathbb{N}) \leq (m : \overline{\mathbb{R}}) / (n : \overline{\mathbb{R}})$

Informal description

For any natural numbers $m$ and $n$, the natural division $m / n$ (as a natural number) is less than or equal to the division of their embeddings in the extended real numbers $\overline{\mathbb{R}}$, i.e., $(m / n : \mathbb{N}) \leq (m : \overline{\mathbb{R}}) / (n : \overline{\mathbb{R}})$.

EReal.div_bot theorem

{a : EReal} : a / ⊥ = 0

Full source

@[simp]
lemma div_bot {a : EReal} : a / ⊥ = 0 := inv_bot ▸ mul_zero a

Division by Negative Infinity in Extended Reals: $a / (-\infty) = 0$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the division of $a$ by $-\infty$ (denoted $\bot$) equals $0$, i.e., $a / (-\infty) = 0$.

EReal.div_top theorem

{a : EReal} : a / ⊤ = 0

Full source

@[simp]
lemma div_top {a : EReal} : a / ⊤ = 0 := inv_top ▸ mul_zero a

Division by Positive Infinity in Extended Reals: $a / (+\infty) = 0$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the division of $a$ by $+\infty$ (denoted $\top$) equals $0$, i.e., $a / (+\infty) = 0$.

EReal.div_zero theorem

{a : EReal} : a / 0 = 0

Full source

@[simp]
lemma div_zero {a : EReal} : a / 0 = 0 := by
  change a * 0⁻¹ = 0
  rw [inv_zero, mul_zero a]

Division by Zero in Extended Reals: $a / 0 = 0$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the division of $a$ by $0$ equals $0$, i.e., $a / 0 = 0$.

EReal.zero_div theorem

{a : EReal} : 0 / a = 0

Full source

@[simp]
lemma zero_div {a : EReal} : 0 / a = 0 := zero_mul a⁻¹

Division of Zero by Any Extended Real Number is Zero

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$, the division of $0$ by $a$ equals $0$, i.e., $0 / a = 0$.

EReal.top_div_of_pos_ne_top theorem

{a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊤ / a = ⊤

Full source

lemma top_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊤ / a = ⊤ :=
  top_mul_of_pos (inv_pos_of_pos_ne_top h h')

Division of Infinity by Positive Extended Real Yields Infinity

Informal description

For any extended real number $a$ such that $0 < a$ and $a \neq +\infty$, the division of $+\infty$ by $a$ equals $+\infty$, i.e., $\frac{\top}{a} = \top$.

EReal.top_div_of_neg_ne_bot theorem

{a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊤ / a = ⊥

Full source

lemma top_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊤ / a = ⊥ :=
  top_mul_of_neg (inv_neg_of_neg_ne_bot h h')

Division of Positive Infinity by Negative Extended Real Yields Negative Infinity

Informal description

For any extended real number $a$ such that $a < 0$ and $a \neq -\infty$, the division of positive infinity $\top$ by $a$ equals negative infinity $\bot$, i.e., $\top / a = \bot$.

EReal.bot_div_of_pos_ne_top theorem

{a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊥ / a = ⊥

Full source

lemma bot_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊥ / a = ⊥ :=
  bot_mul_of_pos (inv_pos_of_pos_ne_top h h')

Negative Infinity Divided by Positive Extended Real Yields Negative Infinity

Informal description

For any extended real number $a$ such that $0 < a$ and $a \neq +\infty$, the division of $-\infty$ (denoted as $\bot$) by $a$ equals $-\infty$, i.e., $\bot / a = \bot$.

EReal.bot_div_of_neg_ne_bot theorem

{a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊥ / a = ⊤

Full source

lemma bot_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊥ / a = ⊤ :=
  bot_mul_of_neg (inv_neg_of_neg_ne_bot h h')

Division of Negative Infinity by Negative Extended Real Yields Positive Infinity: $-\infty / a = +\infty$ for $a < 0$, $a \neq -\infty$

Informal description

For any extended real number $a$ such that $a < 0$ and $a \neq -\infty$, the division of $-\infty$ (denoted $\bot$) by $a$ equals $+\infty$ (denoted $\top$), i.e., $-\infty / a = +\infty$.

EReal.div_self theorem

{a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1

Full source

lemma div_self {a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1 := by
  rw [← coe_toReal h₂ h₁] at h₃ ⊢
  rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]

Extended Real Division Identity: $a / a = 1$ for $a \neq \pm\infty, 0$

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$ that is neither $-\infty$ (denoted as $\bot$), nor $+\infty$ (denoted as $\top$), nor zero, the division of $a$ by itself equals $1$, i.e., $a / a = 1$.

EReal.mul_div theorem

(a b c : EReal) : a * (b / c) = (a * b) / c

Full source

lemma mul_div (a b c : EReal) : a * (b / c) = (a * b) / c := by
  change a * (b * c⁻¹) = (a * b) * c⁻¹
  rw [mul_assoc]

Multiplication-Division Associativity in Extended Real Numbers

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, the following equality holds: $$a \cdot \left(\frac{b}{c}\right) = \frac{a \cdot b}{c}$$

EReal.mul_div_right theorem

(a b c : EReal) : a / b * c = a * c / b

Full source

lemma mul_div_right (a b c : EReal) : a / b * c = a * c / b := by
  rw [mul_comm, EReal.mul_div, mul_comm]

Right Multiplication-Division Commutativity in Extended Real Numbers

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, the following equality holds: $$(a / b) \cdot c = (a \cdot c) / b$$

EReal.mul_div_left_comm theorem

(a b c : EReal) : a * (b / c) = b * (a / c)

Full source

lemma mul_div_left_comm (a b c : EReal) : a * (b / c) = b * (a / c) := by
  rw [mul_div a b c, mul_comm a b, ← mul_div b a c]

Left Commutativity of Multiplication and Division in Extended Real Numbers

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, the following equality holds: $$a \cdot \left(\frac{b}{c}\right) = b \cdot \left(\frac{a}{c}\right)$$

EReal.div_div theorem

(a b c : EReal) : a / b / c = a / (b * c)

Full source

lemma div_div (a b c : EReal) : a / b / c = a / (b * c) := by
  change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹
  rw [mul_assoc a b⁻¹, mul_inv]

Double Division Equals Division by Product in Extended Reals: $a / b / c = a / (b \cdot c)$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$, the double division $a / b / c$ is equal to $a / (b \cdot c)$.

EReal.div_mul_div_comm theorem

(a b c d : EReal) : a / b * (c / d) = a * c / (b * d)

Full source

lemma div_mul_div_comm (a b c d : EReal) : a / b * (c / d) = a * c / (b * d) := by
  rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

Commutativity of Division and Multiplication in Extended Reals: $(a/b)(c/d) = (ac)/(bd)$

Informal description

For any extended real numbers $a, b, c, d \in \overline{\mathbb{R}}$, the following equality holds: $$(a / b) \cdot (c / d) = (a \cdot c) / (b \cdot d)$$

EReal.div_mul_cancel theorem

(h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : a / b * b = a

Full source

lemma div_mul_cancel (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : a / b * b = a := by
  rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]

Division-Multiplication Cancellation in Extended Reals: $(a / b) \cdot b = a$ for $b \neq \pm\infty, 0$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}}$ where $b$ is neither $-\infty$ (denoted $\bot$), nor $+\infty$ (denoted $\top$), nor zero, the operation $(a / b) \cdot b$ equals $a$.

EReal.mul_div_cancel theorem

(h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a

Full source

lemma mul_div_cancel (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a := by
  rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

Multiplication-Division Cancellation in Extended Reals: $b \cdot (a / b) = a$ for $b \neq \pm\infty, 0$

Informal description

For any extended real numbers $a, b \in \overline{\mathbb{R}}$ where $b$ is neither $-\infty$ (denoted $\bot$), nor $+\infty$ (denoted $\top$), nor zero, the operation $b \cdot (a / b)$ equals $a$.

EReal.mul_div_mul_cancel theorem

(h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b

Full source

lemma mul_div_mul_cancel (h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b := by
  rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]

Cancellation of Multiplication in Extended Real Division: $(a \cdot c) / (b \cdot c) = a / b$ for $c \neq \pm\infty, 0$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$ with $c$ not equal to $-\infty$ ($\bot$), $+\infty$ ($\top$), or $0$, the following equality holds: $$(a \cdot c) / (b \cdot c) = a / b$$

EReal.div_eq_iff theorem

(hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : c / b = a ↔ c = a * b

Full source

lemma div_eq_iff (hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : c / b = a ↔ c = a * b := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
  · rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

Division-Multiplication Equivalence in Extended Reals: $c/b = a \leftrightarrow c = a \cdot b$ for $b \neq \pm\infty, 0$

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ with $b$ not equal to $-\infty$ ($\bot$), $+\infty$ ($\top$), or $0$, the equation $c / b = a$ holds if and only if $c = a \cdot b$.

EReal.monotone_div_right_of_nonneg theorem

(h : 0 ≤ b) : Monotone fun a ↦ a / b

Full source

lemma monotone_div_right_of_nonneg (h : 0 ≤ b) : Monotone fun a ↦ a / b :=
  fun _ _ h' ↦ mul_le_mul_of_nonneg_right h' (inv_nonneg_of_nonneg h)

Monotonicity of Right Division by Nonnegative Extended Reals: $0 \leq b \Rightarrow (a \mapsto a/b)$ is monotone

Informal description

For any extended real number $b \in \overline{\mathbb{R}}$ with $0 \leq b$, the function $a \mapsto a / b$ is monotone. That is, for any $a_1, a_2 \in \overline{\mathbb{R}}$ with $a_1 \leq a_2$, we have $a_1 / b \leq a_2 / b$.

EReal.div_le_div_right_of_nonneg theorem

(h : 0 ≤ c) (h' : a ≤ b) : a / c ≤ b / c

Full source

lemma div_le_div_right_of_nonneg (h : 0 ≤ c) (h' : a ≤ b) : a / c ≤ b / c :=
  monotone_div_right_of_nonneg h h'

Right Division Preserves Inequality for Nonnegative Extended Reals: $a \leq b \Rightarrow a/c \leq b/c$ when $0 \leq c$

Informal description

For any extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that $0 \leq c$ and $a \leq b$, we have $a / c \leq b / c$.

EReal.strictMono_div_right_of_pos theorem

(h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun a ↦ a / b

Full source

lemma strictMono_div_right_of_pos (h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun a ↦ a / b := by
  intro a a' a_lt_a'
  apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')
  intro hyp
  apply ne_of_lt a_lt_a'
  rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h), hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' (ne_of_gt h)]

Strict Monotonicity of Right Division by Positive Finite Extended Reals

Informal description

For any extended real number $b \in \overline{\mathbb{R}}$ such that $0 < b$ and $b \neq +\infty$, the function $a \mapsto a / b$ is strictly monotone. That is, for any $a_1, a_2 \in \overline{\mathbb{R}}$ with $a_1 < a_2$, we have $a_1 / b < a_2 / b$.

EReal.div_lt_div_right_of_pos theorem

(h₁ : 0 < c) (h₂ : c ≠ ⊤) (h₃ : a < b) : a / c < b / c

Full source

lemma div_lt_div_right_of_pos (h₁ : 0 < c) (h₂ : c ≠ ⊤) (h₃ : a < b) : a / c < b / c :=
  strictMono_div_right_of_pos h₁ h₂ h₃

Strict Inequality Preservation under Right Division by Positive Finite Extended Reals

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that $0 < c$, $c \neq +\infty$, and $a < b$, we have $a / c < b / c$.

EReal.antitone_div_right_of_nonpos theorem

(h : b ≤ 0) : Antitone fun a ↦ a / b

Full source

lemma antitone_div_right_of_nonpos (h : b ≤ 0) : Antitone fun a ↦ a / b := by
  intro a a' h'
  change a' * b⁻¹ ≤ a * b⁻¹
  rw [← neg_neg (a * b⁻¹), ← neg_neg (a' * b⁻¹), neg_le_neg_iff, mul_comm a b⁻¹, mul_comm a' b⁻¹,
    ← neg_mul b⁻¹ a, ← neg_mul b⁻¹ a', mul_comm (-b⁻¹) a, mul_comm (-b⁻¹) a', ← inv_neg b]
  have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]
  exact div_le_div_right_of_nonneg this h'

Antitonicity of Right Division by Nonpositive Extended Reals

Informal description

For any extended real number $b \in \overline{\mathbb{R}}$ such that $b \leq 0$, the function $a \mapsto a / b$ is antitone. That is, for any $a_1, a_2 \in \overline{\mathbb{R}}$ with $a_1 \leq a_2$, we have $a_2 / b \leq a_1 / b$.

EReal.div_le_div_right_of_nonpos theorem

(h : c ≤ 0) (h' : a ≤ b) : b / c ≤ a / c

Full source

lemma div_le_div_right_of_nonpos (h : c ≤ 0) (h' : a ≤ b) : b / c ≤ a / c :=
  antitone_div_right_of_nonpos h h'

Nonpositivity Reverses Division Inequality in Extended Reals

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that $c \leq 0$ and $a \leq b$, we have $b / c \leq a / c$.

EReal.strictAnti_div_right_of_neg theorem

(h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun a ↦ a / b

Full source

lemma strictAnti_div_right_of_neg (h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun a ↦ a / b := by
  intro a a' a_lt_a'
  simp only
  apply lt_of_le_of_ne <| div_le_div_right_of_nonpos (le_of_lt h) (le_of_lt a_lt_a')
  intro hyp
  apply ne_of_lt a_lt_a'
  rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]

Strict Antitonicity of Right Division by Negative Extended Reals

Informal description

For any extended real number $b \in \overline{\mathbb{R}}$ such that $b < 0$ and $b \neq -\infty$, the function $a \mapsto a / b$ is strictly antitone. That is, for any $a_1, a_2 \in \overline{\mathbb{R}}$ with $a_1 < a_2$, we have $a_2 / b < a_1 / b$.

EReal.div_lt_div_right_of_neg theorem

(h₁ : c < 0) (h₂ : c ≠ ⊥) (h₃ : a < b) : b / c < a / c

Full source

lemma div_lt_div_right_of_neg (h₁ : c < 0) (h₂ : c ≠ ⊥) (h₃ : a < b) : b / c < a / c :=
  strictAnti_div_right_of_neg h₁ h₂ h₃

Strict Reversal of Division Inequality for Negative Extended Reals: $b / c < a / c$ when $c < 0$, $c \neq -\infty$, and $a < b$

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ such that $c < 0$, $c \neq -\infty$, and $a < b$, it holds that $b / c < a / c$.

EReal.le_div_iff_mul_le theorem

(h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c

Full source

lemma le_div_iff_mul_le (h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c := by
  nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [mul_div b a b, mul_comm a b]
  exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Inequality Relating Division and Multiplication in Extended Reals: $a \leq c/b \leftrightarrow a \cdot b \leq c$ for $b > 0$, $b \neq +\infty$

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ with $b > 0$ and $b \neq +\infty$, the inequality $a \leq c / b$ holds if and only if $a \cdot b \leq c$.

EReal.div_le_iff_le_mul theorem

(h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c

Full source

lemma div_le_iff_le_mul (h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c := by
  nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [mul_div b c b, mul_comm b]
  exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Division-Multiplication Inequality for Extended Reals: $a / b \leq c \leftrightarrow a \leq b \cdot c$ when $b > 0$ and finite

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ with $b > 0$ and $b \neq +\infty$, the inequality $a / b \leq c$ holds if and only if $a \leq b \cdot c$.

EReal.lt_div_iff theorem

(h : 0 < b) (h' : b ≠ ⊤) : a < c / b ↔ a * b < c

Full source

lemma lt_div_iff (h : 0 < b) (h' : b ≠ ⊤) : a < c / b ↔ a * b < c := by
  nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [EReal.mul_div b a b, mul_comm a b]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

Inequality equivalence: $a < c/b \leftrightarrow a \cdot b < c$ for positive finite $b$

Informal description

For extended real numbers $a, b, c \in \overline{\mathbb{R}}$ with $0 < b$ and $b \neq +\infty$, the inequality $a < c / b$ holds if and only if $a \cdot b < c$.

EReal.div_lt_iff theorem

(h : 0 < c) (h' : c ≠ ⊤) : b / c < a ↔ b < a * c

Full source

lemma div_lt_iff (h : 0 < c) (h' : c ≠ ⊤) :  b / c < a ↔ b < a * c := by
  nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [EReal.mul_div c a c, mul_comm a c]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

Division-Multiplication Inequality for Positive Finite Extended Reals: $b/c < a \leftrightarrow b < a \cdot c$

Informal description

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

EReal.div_nonneg theorem

(h : 0 ≤ a) (h' : 0 ≤ b) : 0 ≤ a / b

Full source

lemma div_nonneg (h : 0 ≤ a) (h' : 0 ≤ b) : 0 ≤ a / b :=
  mul_nonneg h (inv_nonneg_of_nonneg h')

Nonnegativity of Quotient for Nonnegative Extended Reals

Informal description

For any extended real numbers $a$ and $b$ such that $0 \leq a$ and $0 \leq b$, the quotient $a / b$ is nonnegative, i.e., $0 \leq a / b$.

EReal.div_pos theorem

(ha : 0 < a) (hb : 0 < b) (hb' : b ≠ ⊤) : 0 < a / b

Full source

lemma div_pos (ha : 0 < a) (hb : 0 < b) (hb' : b ≠ ⊤) : 0 < a / b :=
  mul_pos ha (inv_pos_of_pos_ne_top hb hb')

Positivity of Quotient for Positive Extended Reals with Finite Denominator

Informal description

For any extended real numbers $a$ and $b$ such that $0 < a$, $0 < b$, and $b \neq +\infty$, the quotient $a / b$ is strictly positive, i.e., $0 < a / b$.

EReal.div_nonpos_of_nonpos_of_nonneg theorem

(h : a ≤ 0) (h' : 0 ≤ b) : a / b ≤ 0

Full source

lemma div_nonpos_of_nonpos_of_nonneg (h : a ≤ 0) (h' : 0 ≤ b) : a / b ≤ 0 :=
  mul_nonpos_of_nonpos_of_nonneg h (inv_nonneg_of_nonneg h')

Nonpositivity of Quotient for Nonpositive Numerator and Nonnegative Denominator in Extended Reals

Informal description

For any extended real numbers $a$ and $b$ such that $a \leq 0$ and $0 \leq b$, the quotient $a / b$ is nonpositive, i.e., $a / b \leq 0$.

EReal.div_nonpos_of_nonneg_of_nonpos theorem

(h : 0 ≤ a) (h' : b ≤ 0) : a / b ≤ 0

Full source

lemma div_nonpos_of_nonneg_of_nonpos (h : 0 ≤ a) (h' : b ≤ 0) : a / b ≤ 0 :=
  mul_nonpos_of_nonneg_of_nonpos h (inv_nonpos_of_nonpos h')

Nonpositivity of Quotient for Nonnegative Numerator and Nonpositive Denominator in Extended Reals

Informal description

For any extended real numbers $a$ and $b$ such that $a \geq 0$ and $b \leq 0$, the quotient $a / b$ is nonpositive, i.e., $a / b \leq 0$.

EReal.div_nonneg_of_nonpos_of_nonpos theorem

(h : a ≤ 0) (h' : b ≤ 0) : 0 ≤ a / b

Full source

lemma div_nonneg_of_nonpos_of_nonpos (h : a ≤ 0) (h' : b ≤ 0) : 0 ≤ a / b :=
  le_of_eq_of_le zero_div.symm (div_le_div_right_of_nonpos h' h)

Nonnegativity of Quotient for Nonpositive Numerator and Nonpositive Denominator in Extended Reals

Informal description

For any extended real numbers $a$ and $b$ such that $a \leq 0$ and $b \leq 0$, the quotient $a / b$ is nonnegative, i.e., $0 \leq a / b$.

EReal.le_mul_of_forall_lt theorem

(h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ 0 < b) (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

Full source

lemma le_mul_of_forall_lt (h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤a ≠ ⊤ ∨ 0 < b)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b := by
  refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
  obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd
  replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1
  replace h₂ : a' ≠ ⊤a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne
  obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd
  exact (h a' (mem_Ioo.1 aa').1 b' (mem_Ioo.1 bb').1).trans hd.le

Lower bound on extended real multiplication via upper approximations

Informal description

Let $a, b, c$ be extended real numbers. If either $0 < a$ or $b \neq \top$, and either $a \neq \top$ or $0 < b$, and for all $a' > a$ and $b' > b$ we have $c \leq a' \cdot b'$, then $c \leq a \cdot b$.

EReal.mul_le_of_forall_lt_of_nonneg theorem

(ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c) : a * b ≤ c

Full source

lemma mul_le_of_forall_lt_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c)
    (h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c) : a * b ≤ c := by
  refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_
  rcases lt_or_le d 0 with d0 | d0
  · exact d0.le.trans hc
  obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab
  obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab
  exact dab.le.trans (h a' aa' b' bb')

Upper bound on extended real multiplication via open intervals

Informal description

For extended real numbers $a, b, c$ with $0 \leq a$ and $0 \leq c$, if for all $a' \in (0, a)$ and $b' \in (0, b)$ we have $a' \cdot b' \leq c$, then $a \cdot b \leq c$.

EReal.div_right_distrib_of_nonneg theorem

(h : 0 ≤ a) (h' : 0 ≤ b) : (a + b) / c = a / c + b / c

Full source

lemma div_right_distrib_of_nonneg (h : 0 ≤ a) (h' : 0 ≤ b) :
    (a + b) / c = a / c + b / c :=
  EReal.right_distrib_of_nonneg h h'

Right Distributivity of Division 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 for division: $(a + b) / c = a / c + b / c$.

EReal.add_div_of_nonneg_right theorem

(h : 0 ≤ c) : (a + b) / c = a / c + b / c

Full source

lemma add_div_of_nonneg_right (h : 0 ≤ c) :
    (a + b) / c = a / c + b / c := by
  apply right_distrib_of_nonneg_of_ne_top (inv_nonneg_of_nonneg h) (inv_lt_top c).ne

Right Distributivity of Division over Addition for Nonnegative Extended Reals

Informal description

For any extended real numbers $a, b$ and any nonnegative extended real number $c \geq 0$, the following equality holds: $$(a + b) / c = a / c + b / c$$