Mathlib.Data.ENNReal.Inv

ENNReal.div_eq_inv_mul theorem

: a / b = b⁻¹ * a

Full source

protected theorem div_eq_inv_mul : a / b = b⁻¹ * a := by rw [div_eq_mul_inv, mul_comm]

Division as Inverse Multiplication in Extended Non-Negative Reals

Informal description

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

ENNReal.inv_zero theorem

: (0 : ℝ≥0∞)⁻¹ = ∞

Full source

@[simp] theorem inv_zero : (0 : ℝ≥0∞)⁻¹ = ∞ :=
  show sInf { b : ℝ≥0∞ | 1 ≤ 0 * b } = ∞ by simp

Inverse of Zero in Extended Non-Negative Reals: $0^{-1} = \infty$

Informal description

The multiplicative inverse of $0$ in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is $\infty$, i.e., $0^{-1} = \infty$.

ENNReal.inv_top theorem

: ∞⁻¹ = 0

Full source

@[simp] theorem inv_top : ∞∞⁻¹ = 0 :=
  bot_unique <| le_of_forall_gt_imp_ge_of_dense fun a (h : 0 < a) => sInf_le <| by
    simp [*, h.ne', top_mul]

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

Informal description

The multiplicative inverse of $\infty$ in the extended non-negative real numbers is $0$, i.e., $\infty^{-1} = 0$.

ENNReal.coe_inv_le theorem

: (↑r⁻¹ : ℝ≥0∞) ≤ (↑r)⁻¹

Full source

theorem coe_inv_le : (↑r⁻¹ : ℝ≥0∞) ≤ (↑r)⁻¹ :=
  le_sInf fun b (hb : 1 ≤ ↑r * b) =>
    coe_le_iff.2 <| by
      rintro b rfl
      apply NNReal.inv_le_of_le_mul
      rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

Inequality for Casted Inverses in Extended Nonnegative Reals: $\overline{r^{-1}} \leq (\overline{r})^{-1}$

Informal description

For any nonnegative real number $r$, the extended nonnegative real number obtained by casting $r^{-1}$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is less than or equal to the inverse of the cast of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{r^{-1}} \leq (\overline{r})^{-1}$ where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_inv theorem

(hr : r ≠ 0) : (↑r⁻¹ : ℝ≥0∞) = (↑r)⁻¹

Full source

@[simp, norm_cast]
theorem coe_inv (hr : r ≠ 0) : (↑r⁻¹ : ℝ≥0∞) = (↑r)⁻¹ :=
  coe_inv_le.antisymm <| sInf_le <| mem_setOf.2 <| by rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]

Equality of Casted Inverses in Extended Nonnegative Reals: $\overline{r^{-1}} = (\overline{r})^{-1}$ for $r \neq 0$

Informal description

For any nonzero nonnegative real number $r$, the extended nonnegative real number obtained by casting $r^{-1}$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the inverse of the cast of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{r^{-1}} = (\overline{r})^{-1}$ where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_inv_two theorem

: ((2⁻¹ : ℝ≥0) : ℝ≥0∞) = 2⁻¹

Full source

@[norm_cast]
theorem coe_inv_two : ((2⁻¹ : ℝ≥0) : ℝ≥0∞) = 2⁻¹ := by rw [coe_inv _root_.two_ne_zero, coe_two]

Equality of Casted Inverses for Two in Extended Nonnegative Reals: $\overline{2^{-1}} = 2^{-1}$

Informal description

The extended nonnegative real number obtained by casting the inverse of $2$ in $\mathbb{R}_{\geq 0}$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the inverse of $2$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{2^{-1}} = 2^{-1}$ where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_div theorem

(hr : r ≠ 0) : (↑(p / r) : ℝ≥0∞) = p / r

Full source

@[simp, norm_cast]
theorem coe_div (hr : r ≠ 0) : (↑(p / r) : ℝ≥0∞) = p / r := by
  rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]

Equality of Casted Division in Extended Nonnegative Reals: $\overline{p / r} = \overline{p} / \overline{r}$ for $r \neq 0$

Informal description

For any nonnegative real numbers $p$ and $r$ with $r \neq 0$, the extended nonnegative real number obtained by casting the quotient $p / r$ equals the quotient of the casts of $p$ and $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{p / r} = \overline{p} / \overline{r}$, where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_div_le theorem

: ↑(p / r) ≤ (p / r : ℝ≥0∞)

Full source

lemma coe_div_le : ↑(p / r) ≤ (p / r : ℝ≥0∞) := by
  simpa only [div_eq_mul_inv, coe_mul] using mul_le_mul_left' coe_inv_le _

Inequality for Casted Division in Extended Nonnegative Reals: $\overline{p / r} \leq \overline{p} / \overline{r}$

Informal description

For any nonnegative real numbers $p$ and $r$, the extended nonnegative real number obtained by casting the quotient $p / r$ is less than or equal to the quotient of the casts of $p$ and $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{p / r} \leq \overline{p} / \overline{r}$, where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.div_zero theorem

(h : a ≠ 0) : a / 0 = ∞

Full source

theorem div_zero (h : a ≠ 0) : a / 0 = ∞ := by simp [div_eq_mul_inv, h]

Division by Zero in Extended Non-Negative Reals: $a / 0 = \infty$ for $a \neq 0$

Informal description

For any nonzero extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the division of $a$ by $0$ equals $\infty$, i.e., $a / 0 = \infty$.

ENNReal.instDivInvOneMonoid instance

: DivInvOneMonoid ℝ≥0∞

Full source

instance : DivInvOneMonoid ℝ≥0∞ :=
  { inferInstanceAs (DivInvMonoid ℝ≥0∞) with
    inv_one := by simpa only [coe_inv one_ne_zero, coe_one] using coe_inj.2 inv_one }

Division Monoid Structure on Extended Non-Negative Reals

Informal description

The extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a division monoid with an inverse operation that satisfies $1 / 1 = 1$.

ENNReal.inv_pow theorem

: ∀ {a : ℝ≥0∞} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n

Full source

protected theorem inv_pow : ∀ {a : ℝ≥0∞} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n
  | _, 0 => by simp only [pow_zero, inv_one]
  | ⊤, n + 1 => by simp [top_pow]
  | (a : ℝ≥0), n + 1 => by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp [top_pow]
    · have := pow_ne_zero (n + 1) ha
      norm_cast
      rw [inv_pow]

Inverse of Power Equals Power of Inverse in Extended Non-Negative Reals: $(a^n)^{-1} = (a^{-1})^n$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any natural number $n$, the inverse of $a^n$ is equal to the $n$-th power of the inverse of $a$, i.e., $(a^n)^{-1} = (a^{-1})^n$.

ENNReal.mul_inv_cancel theorem

(h0 : a ≠ 0) (ht : a ≠ ∞) : a * a⁻¹ = 1

Full source

protected theorem mul_inv_cancel (h0 : a ≠ 0) (ht : a ≠ ∞) : a * a⁻¹ = 1 := by
  lift a to ℝ≥0 using ht
  norm_cast at h0; norm_cast
  exact mul_inv_cancel₀ h0

Multiplicative Inverse Property for Nonzero Finite Extended Non-Negative Reals: $a \cdot a^{-1} = 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the product of $a$ and its multiplicative inverse equals $1$, i.e., $a \cdot a^{-1} = 1$.

ENNReal.inv_mul_cancel theorem

(h0 : a ≠ 0) (ht : a ≠ ∞) : a⁻¹ * a = 1

Full source

protected theorem inv_mul_cancel (h0 : a ≠ 0) (ht : a ≠ ∞) : a⁻¹ * a = 1 :=
  mul_comm a a⁻¹ ▸ ENNReal.mul_inv_cancel h0 ht

Multiplicative Inverse Property for Nonzero Finite Extended Non-Negative Reals: $a^{-1} \cdot a = 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the product of the multiplicative inverse of $a$ and $a$ equals $1$, i.e., $a^{-1} \cdot a = 1$.

ENNReal.inv_mul_cancel_left' theorem

(ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a⁻¹ * (a * b) = b

Full source

/-- See `ENNReal.inv_mul_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma inv_mul_cancel_left' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) :
    a⁻¹ * (a * b) = b := by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  obtain rfl | ha := eq_or_ne a ⊤
  · simp_all
  · simp [← mul_assoc, ENNReal.inv_mul_cancel, *]

Cancellation Property for Extended Non-Negative Reals: $a^{-1} \cdot (a \cdot b) = b$ under Zero and Infinity Conditions

Informal description

For extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a = 0$ implies $b = 0$ and $a = \infty$ implies $b = 0$, then $a^{-1} \cdot (a \cdot b) = b$.

ENNReal.inv_mul_cancel_left theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : a⁻¹ * (a * b) = b

Full source

/-- See `ENNReal.inv_mul_cancel_left'` for a stronger version. -/
protected lemma inv_mul_cancel_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a⁻¹ * (a * b) = b :=
  ENNReal.inv_mul_cancel_left' (by simp [ha₀]) (by simp [ha])

Left Cancellation Property for Multiplication and Inverse in Extended Non-Negative Reals: $a^{-1} \cdot (a \cdot b) = b$ for nonzero finite $a$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the product of the multiplicative inverse of $a$ and $(a \cdot b)$ equals $b$, i.e., $a^{-1} \cdot (a \cdot b) = b$.

ENNReal.mul_inv_cancel_left' theorem

(ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (a⁻¹ * b) = b

Full source

/-- See `ENNReal.mul_inv_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma mul_inv_cancel_left' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) :
    a * (a⁻¹ * b) = b := by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  obtain rfl | ha := eq_or_ne a ⊤
  · simp_all
  · simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

Left Cancellation Property for Multiplication and Inverse in Extended Non-Negative Reals with Zero/Infinity Conditions

Informal description

For extended non-negative real numbers $a$ and $b$, if $a = 0$ implies $b = 0$ and $a = \infty$ implies $b = 0$, then $a \cdot (a^{-1} \cdot b) = b$.

ENNReal.mul_inv_cancel_left theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (a⁻¹ * b) = b

Full source

/-- See `ENNReal.mul_inv_cancel_left'` for a stronger version. -/
protected lemma mul_inv_cancel_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (a⁻¹ * b) = b :=
  ENNReal.mul_inv_cancel_left' (by simp [ha₀]) (by simp [ha])

Left Cancellation Property for Multiplication and Inverse in Extended Non-Negative Reals

Informal description

For extended non-negative real numbers $a$ and $b$, if $a$ is neither zero nor infinity, then $a \cdot (a^{-1} \cdot b) = b$.

ENNReal.mul_inv_cancel_right' theorem

(hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : a * b * b⁻¹ = a

Full source

/-- See `ENNReal.mul_inv_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected lemma mul_inv_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) :
    a * b * b⁻¹ = a := by
  obtain rfl | hb₀ := eq_or_ne b 0
  · simp_all
  obtain rfl | hb := eq_or_ne b ⊤
  · simp_all
  · simp [mul_assoc, ENNReal.mul_inv_cancel, *]

Cancellation of Multiplication and Inversion in Extended Non-Negative Reals with Zero and Infinity Conditions

Informal description

For extended non-negative real numbers $a$ and $b$, if $b = 0$ implies $a = 0$ and $b = \infty$ implies $a = 0$, then $a \cdot b \cdot b^{-1} = a$.

ENNReal.mul_inv_cancel_right theorem

(hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b * b⁻¹ = a

Full source

/-- See `ENNReal.mul_inv_cancel_right'` for a stronger version. -/
protected lemma mul_inv_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b * b⁻¹ = a :=
  ENNReal.mul_inv_cancel_right' (by simp [hb₀]) (by simp [hb])

Cancellation of Multiplication and Inversion in Extended Non-Negative Reals: $a \cdot b \cdot b^{-1} = a$ for $b \neq 0, \infty$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ where $b$ is neither zero nor infinity, it holds that $a \cdot b \cdot b^{-1} = a$.

ENNReal.inv_mul_cancel_right' theorem

(hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : a * b⁻¹ * b = a

Full source

/-- See `ENNReal.inv_mul_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected lemma inv_mul_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) :
    a * b⁻¹ * b = a := by
  obtain rfl | hb₀ := eq_or_ne b 0
  · simp_all
  obtain rfl | hb := eq_or_ne b ⊤
  · simp_all
  · simp [mul_assoc, ENNReal.inv_mul_cancel, *]

Generalized Multiplicative Inverse Property: $a \cdot b^{-1} \cdot b = a$ under Zero and Infinity Conditions

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b = 0$ implies $a = 0$ and $b = \infty$ implies $a = 0$, then $a \cdot b^{-1} \cdot b = a$.

ENNReal.inv_mul_cancel_right theorem

(hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b⁻¹ * b = a

Full source

/-- See `ENNReal.inv_mul_cancel_right'` for a stronger version. -/
protected lemma inv_mul_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b⁻¹ * b = a :=
  ENNReal.inv_mul_cancel_right' (by simp [hb₀]) (by simp [hb])

Multiplicative Inverse Property: $a \cdot b^{-1} \cdot b = a$ for Nonzero Finite $b$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $b \neq 0$ and $b \neq \infty$, the equality $a \cdot b^{-1} \cdot b = a$ holds.

ENNReal.mul_div_cancel_right' theorem

(hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) : a * b / b = a

Full source

/-- See `ENNReal.mul_div_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected lemma mul_div_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) :
    a * b / b = a := ENNReal.mul_inv_cancel_right' hb₀ hb

Generalized Division Cancellation: $a \cdot b / b = a$ under Zero and Infinity Conditions

Informal description

For extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b = 0$ implies $a = 0$ and $b = \infty$ implies $a = 0$, then $a \cdot b / b = a$.

ENNReal.mul_div_cancel_right theorem

(hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b / b = a

Full source

/-- See `ENNReal.mul_div_cancel_right'` for a stronger version. -/
protected lemma mul_div_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b / b = a :=
  ENNReal.mul_div_cancel_right' (by simp [hb₀]) (by simp [hb])

Division Cancellation: $a \cdot b / b = a$ for Nonzero Finite $b$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $b \neq 0$ and $b \neq \infty$, the equality $a \cdot b / b = a$ holds.

ENNReal.div_mul_cancel' theorem

(ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : b / a * a = b

Full source

/-- See `ENNReal.div_mul_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma div_mul_cancel' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : b / a * a = b :=
  ENNReal.inv_mul_cancel_right' ha₀ ha

Generalized Division-Multiplication Cancellation Property in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a = 0$ implies $b = 0$ and $a = \infty$ implies $b = 0$, then $(b / a) \cdot a = b$.

ENNReal.div_mul_cancel theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : b / a * a = b

Full source

/-- See `ENNReal.div_mul_cancel'` for a stronger version. -/
protected lemma div_mul_cancel (ha₀ : a ≠ 0) (ha : a ≠ ∞) : b / a * a = b :=
  ENNReal.div_mul_cancel' (by simp [ha₀]) (by simp [ha])

Division-Multiplication Cancellation in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the equality $(b / a) \cdot a = b$ holds.

ENNReal.mul_div_cancel' theorem

(ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (b / a) = b

Full source

/-- See `ENNReal.mul_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma mul_div_cancel' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (b / a) = b := by
  rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]

Generalized Multiplication-Division Cancellation in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a = 0$ implies $b = 0$ and $a = \infty$ implies $b = 0$, then $a \cdot (b / a) = b$.

ENNReal.mul_div_cancel theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (b / a) = b

Full source

/-- See `ENNReal.mul_div_cancel'` for a stronger version. -/
protected lemma mul_div_cancel (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (b / a) = b :=
  ENNReal.mul_div_cancel' (by simp [ha₀]) (by simp [ha])

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

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the equality $a \cdot (b / a) = b$ holds.

ENNReal.mul_comm_div theorem

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

Full source

protected theorem mul_comm_div : a / b * c = a * (c / b) := by
  simp only [div_eq_mul_inv, mul_left_comm, mul_comm, mul_assoc]

Commutativity of Division and Multiplication in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the following equality holds: \[ \frac{a}{b} \cdot c = a \cdot \left(\frac{c}{b}\right). \]

ENNReal.mul_div_right_comm theorem

: a * b / c = a / c * b

Full source

protected theorem mul_div_right_comm : a * b / c = a / c * b := by
  simp only [div_eq_mul_inv, mul_right_comm]

Right Commutativity of Division and Multiplication in Extended Non-Negative Reals: $\frac{ab}{c} = \frac{a}{c}b$

Informal description

For any extended non-negative real numbers $a, b, c$, the following equality holds: $$ \frac{a \cdot b}{c} = \frac{a}{c} \cdot b $$

ENNReal.instInvolutiveInv instance

: InvolutiveInv ℝ≥0∞

Full source

instance : InvolutiveInv ℝ≥0∞ where
  inv_inv a := by
    by_cases a = 0 <;> cases a <;> simp_all [none_eq_top, some_eq_coe, -coe_inv, (coe_inv _).symm]

Involutive Inversion on Extended Non-Negative Reals

Informal description

The extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have an involution given by the multiplicative inverse operation $x \mapsto x^{-1}$.

ENNReal.inv_eq_one theorem

: a⁻¹ = 1 ↔ a = 1

Full source

@[simp] protected lemma inv_eq_one : a⁻¹a⁻¹ = 1 ↔ a = 1 := by rw [← inv_inj, inv_inv, inv_one]

Inverse Equals One if and Only if Element Equals One in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ equals $1$ if and only if $a$ equals $1$, i.e., $a^{-1} = 1 \leftrightarrow a = 1$.

ENNReal.inv_eq_top theorem

: a⁻¹ = ∞ ↔ a = 0

Full source

@[simp] theorem inv_eq_top : a⁻¹a⁻¹ = ∞ ↔ a = 0 := inv_zero ▸ inv_inj

Inverse Equals Infinity if and Only if Element is Zero in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ equals infinity if and only if $a$ equals zero, i.e., $a^{-1} = \infty \leftrightarrow a = 0$.

ENNReal.inv_ne_top theorem

: a⁻¹ ≠ ∞ ↔ a ≠ 0

Full source

theorem inv_ne_top : a⁻¹a⁻¹ ≠ ∞a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp

Non-Zero Condition for Finite Inverse in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ is not equal to infinity if and only if $a$ is not equal to zero.

ENNReal.inv_lt_top theorem

{x : ℝ≥0∞} : x⁻¹ < ∞ ↔ 0 < x

Full source

@[simp]
theorem inv_lt_top {x : ℝ≥0∞} : x⁻¹x⁻¹ < ∞ ↔ 0 < x := by
  simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero]

Finite Inverse Condition for Positive Extended Non-Negative Reals

Informal description

For any extended non-negative real number $x$, the multiplicative inverse $x^{-1}$ is finite if and only if $x$ is positive, i.e., $x^{-1} < \infty \leftrightarrow 0 < x$.

ENNReal.div_lt_top theorem

{x y : ℝ≥0∞} (h1 : x ≠ ∞) (h2 : y ≠ 0) : x / y < ∞

Full source

theorem div_lt_top {x y : ℝ≥0∞} (h1 : x ≠ ∞) (h2 : y ≠ 0) : x / y < ∞ :=
  mul_lt_top h1.lt_top (inv_ne_top.mpr h2).lt_top

Finite Division Condition for Extended Non-Negative Reals: $x / y < \infty$ when $x \neq \infty$ and $y \neq 0$

Informal description

For any extended non-negative real numbers $x$ and $y$ such that $x \neq \infty$ and $y \neq 0$, the division $x / y$ is finite, i.e., $x / y < \infty$.

ENNReal.inv_eq_zero theorem

: a⁻¹ = 0 ↔ a = ∞

Full source

@[simp]
protected theorem inv_eq_zero : a⁻¹a⁻¹ = 0 ↔ a = ∞ :=
  inv_top ▸ inv_inj

Inverse Zero Condition: $a^{-1} = 0 \leftrightarrow a = \infty$

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ equals $0$ if and only if $a$ equals $\infty$, i.e., $a^{-1} = 0 \leftrightarrow a = \infty$.

ENNReal.inv_ne_zero theorem

: a⁻¹ ≠ 0 ↔ a ≠ ∞

Full source

protected theorem inv_ne_zero : a⁻¹a⁻¹ ≠ 0a⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp

Nonzero Inverse Condition for Extended Non-Negative Reals: $a^{-1} \neq 0 \leftrightarrow a \neq \infty$

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ is not equal to zero if and only if $a$ is not equal to infinity.

ENNReal.div_pos theorem

(ha : a ≠ 0) (hb : b ≠ ∞) : 0 < a / b

Full source

protected theorem div_pos (ha : a ≠ 0) (hb : b ≠ ∞) : 0 < a / b :=
  ENNReal.mul_pos ha <| ENNReal.inv_ne_zero.2 hb

Positivity of Division in Extended Non-Negative Reals: $0 < a / b$ when $a \neq 0$ and $b \neq \infty$

Informal description

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

ENNReal.inv_mul_le_iff theorem

{x y z : ℝ≥0∞} (h1 : x ≠ 0) (h2 : x ≠ ∞) : x⁻¹ * y ≤ z ↔ y ≤ x * z

Full source

protected theorem inv_mul_le_iff {x y z : ℝ≥0∞} (h1 : x ≠ 0) (h2 : x ≠ ∞) :
    x⁻¹x⁻¹ * y ≤ z ↔ y ≤ x * z := by
  rw [← mul_le_mul_left h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]

Inverse-Multiplication Inequality Equivalence for Extended Non-Negative Reals: $x^{-1}y \leq z \leftrightarrow y \leq xz$

Informal description

For any extended non-negative real numbers $x, y, z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$ and $x \neq \infty$, the inequality $x^{-1} \cdot y \leq z$ holds if and only if $y \leq x \cdot z$.

ENNReal.mul_inv_le_iff theorem

{x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) : x * y⁻¹ ≤ z ↔ x ≤ z * y

Full source

protected theorem mul_inv_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x * y⁻¹ ≤ z ↔ x ≤ z * y := by
  rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]

Multiplication-Inverse Inequality Equivalence for Extended Non-Negative Reals: $xy^{-1} \leq z \leftrightarrow x \leq zy$

Informal description

For any extended non-negative real numbers $x, y, z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $y \neq 0$ and $y \neq \infty$, the inequality $x \cdot y^{-1} \leq z$ holds if and only if $x \leq z \cdot y$.

ENNReal.div_le_iff theorem

{x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) : x / y ≤ z ↔ x ≤ z * y

Full source

protected theorem div_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x / y ≤ z ↔ x ≤ z * y := by
  rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]

Division Inequality Equivalence for Extended Non-Negative Reals: $x/y \leq z \leftrightarrow x \leq zy$

Informal description

For any extended non-negative real numbers $x, y, z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $y \neq 0$ and $y \neq \infty$, the inequality $x / y \leq z$ holds if and only if $x \leq z \cdot y$.

ENNReal.div_le_iff' theorem

{x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) : x / y ≤ z ↔ x ≤ y * z

Full source

protected theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x / y ≤ z ↔ x ≤ y * z := by
  rw [mul_comm, ENNReal.div_le_iff h1 h2]

Division Inequality Equivalence for Extended Non-Negative Reals: $x/y \leq z \leftrightarrow x \leq yz$

Informal description

For any extended non-negative real numbers $x, y, z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $y \neq 0$ and $y \neq \infty$, the inequality $x / y \leq z$ holds if and only if $x \leq y \cdot z$.

ENNReal.mul_inv theorem

{a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Full source

protected theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞a ≠ ∞ ∨ b ≠ 0) :
    (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
  induction' b with b
  · replace ha : a ≠ 0 := ha.neg_resolve_right rfl
    simp [ha]
  induction' a with a
  · replace hb : b ≠ 0 := coe_ne_zero.1 (hb.neg_resolve_left rfl)
    simp [hb]
  by_cases h'a : a = 0
  · simp only [h'a, top_mul, ENNReal.inv_zero, ENNReal.coe_ne_top, zero_mul, Ne,
      not_false_iff, ENNReal.coe_zero, ENNReal.inv_eq_zero]
  by_cases h'b : b = 0
  · simp only [h'b, ENNReal.inv_zero, ENNReal.coe_ne_top, mul_top, Ne, not_false_iff,
      mul_zero, ENNReal.coe_zero, ENNReal.inv_eq_zero]
  rw [← ENNReal.coe_mul, ← ENNReal.coe_inv, ← ENNReal.coe_inv h'a, ← ENNReal.coe_inv h'b, ←
    ENNReal.coe_mul, mul_inv_rev, mul_comm]
  simp [h'a, h'b]

Inverse of Product in Extended Non-Negative Reals: $(a \cdot b)^{-1} = a^{-1} \cdot b^{-1}$ under given conditions

Informal description

For any extended non-negative real numbers $a$ and $b$ such that either $a \neq 0$ or $b \neq \infty$, and either $a \neq \infty$ or $b \neq 0$, the inverse of their product equals the product of their inverses, i.e., $(a \cdot b)^{-1} = a^{-1} \cdot b^{-1}$.

ENNReal.inv_div theorem

{a b : ℝ≥0∞} (htop : b ≠ ∞ ∨ a ≠ ∞) (hzero : b ≠ 0 ∨ a ≠ 0) : (a / b)⁻¹ = b / a

Full source

protected theorem inv_div {a b : ℝ≥0∞} (htop : b ≠ ∞b ≠ ∞ ∨ a ≠ ∞) (hzero : b ≠ 0b ≠ 0 ∨ a ≠ 0) :
    (a / b)⁻¹ = b / a := by
  rw [← ENNReal.inv_ne_zero] at htop
  rw [← ENNReal.inv_ne_top] at hzero
  rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

Inverse of Quotient in Extended Non-Negative Reals: $(a / b)^{-1} = b / a$ under given conditions

Informal description

For any extended non-negative real numbers $a$ and $b$ such that either $b \neq \infty$ or $a \neq \infty$, and either $b \neq 0$ or $a \neq 0$, the inverse of the quotient $a / b$ is equal to the quotient $b / a$, i.e., $(a / b)^{-1} = b / a$.

ENNReal.mul_div_mul_left theorem

(a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) : c * a / (c * b) = a / b

Full source

protected theorem mul_div_mul_left (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) :
    c * a / (c * b) = a / b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inl hc) (Or.inl hc'), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', one_mul]

Cancellation of Multiplication in Division for Extended Non-Negative Reals: $\frac{c \cdot a}{c \cdot b} = \frac{a}{b}$ under $c \neq 0, \infty$

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $c \neq 0$ and $c \neq \infty$, the following equality holds: \[ \frac{c \cdot a}{c \cdot b} = \frac{a}{b}. \]

ENNReal.mul_div_mul_right theorem

(a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) : a * c / (b * c) = a / b

Full source

protected theorem mul_div_mul_right (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) :
    a * c / (b * c) = a / b := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', mul_one]

Cancellation of Common Factor in Division of Extended Non-Negative Reals: $\frac{a \cdot c}{b \cdot c} = \frac{a}{b}$

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $c \neq 0$ and $c \neq \infty$, the equality $\frac{a \cdot c}{b \cdot c} = \frac{a}{b}$ holds.

ENNReal.sub_div theorem

(h : 0 < b → b < a → c ≠ 0) : (a - b) / c = a / c - b / c

Full source

protected theorem sub_div (h : 0 < b → b < a → c ≠ 0) : (a - b) / c = a / c - b / c := by
  simp_rw [div_eq_mul_inv]
  exact ENNReal.sub_mul (by simpa using h)

Subtraction and Division Identity for Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a$, $b$, and $c$, if the condition $0 < b \to b < a \to c \neq 0$ holds, then the equality $(a - b) / c = a / c - b / c$ is satisfied.

ENNReal.inv_pos theorem

: 0 < a⁻¹ ↔ a ≠ ∞

Full source

@[simp]
protected theorem inv_pos : 0 < a⁻¹ ↔ a ≠ ∞ :=
  pos_iff_ne_zero.trans ENNReal.inv_ne_zero

Positivity of Inverse in Extended Non-Negative Reals: $0 < a^{-1} \leftrightarrow a \neq \infty$

Informal description

For any extended non-negative real number $a$, the multiplicative inverse $a^{-1}$ is strictly positive if and only if $a$ is not equal to infinity.

ENNReal.inv_strictAnti theorem

: StrictAnti (Inv.inv : ℝ≥0∞ → ℝ≥0∞)

Full source

theorem inv_strictAnti : StrictAnti (Inv.inv : ℝ≥0∞ → ℝ≥0∞) := by
  intro a b h
  lift a to ℝ≥0 using h.ne_top
  induction b; · simp
  rw [coe_lt_coe] at h
  rcases eq_or_ne a 0 with (rfl | ha); · simp [h]
  rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
  exact NNReal.inv_lt_inv ha h

Strict Antitonicity of Inversion in Extended Non-Negative Reals

Informal description

The multiplicative inversion function $x \mapsto x^{-1}$ is strictly antitone on the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$. That is, for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b$ then $b^{-1} < a^{-1}$.

ENNReal.inv_lt_inv theorem

: a⁻¹ < b⁻¹ ↔ b < a

Full source

@[simp]
protected theorem inv_lt_inv : a⁻¹a⁻¹ < b⁻¹ ↔ b < a :=
  inv_strictAnti.lt_iff_lt

Inverse Inequality in Extended Non-Negative Reals: $a^{-1} < b^{-1} \leftrightarrow b < a$

Informal description

For any extended non-negative real numbers $a$ and $b$, the inequality $a^{-1} < b^{-1}$ holds if and only if $b < a$.

ENNReal.inv_lt_iff_inv_lt theorem

: a⁻¹ < b ↔ b⁻¹ < a

Full source

theorem inv_lt_iff_inv_lt : a⁻¹a⁻¹ < b ↔ b⁻¹ < a := by
  simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

Inversion Inequality Equivalence: $a^{-1} < b \leftrightarrow b^{-1} < a$

Informal description

For any extended non-negative real numbers $a$ and $b$, the inequality $a^{-1} < b$ holds if and only if $b^{-1} < a$.

ENNReal.lt_inv_iff_lt_inv theorem

: a < b⁻¹ ↔ b < a⁻¹

Full source

theorem lt_inv_iff_lt_inv : a < b⁻¹ ↔ b < a⁻¹ := by
  simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b

Inequality Equivalence under Inversion in Extended Non-Negative Reals: $a < b^{-1} \leftrightarrow b < a^{-1}$

Informal description

For any extended non-negative real numbers $a$ and $b$, the inequality $a < b^{-1}$ holds if and only if $b < a^{-1}$.

ENNReal.inv_le_inv theorem

: a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Full source

@[simp]
protected theorem inv_le_inv : a⁻¹a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
  inv_strictAnti.le_iff_le

Inversion Reverses Order in Extended Non-Negative Reals: $a^{-1} \leq b^{-1} \leftrightarrow b \leq a$

Informal description

For any extended non-negative real numbers $a$ and $b$, the inequality $a^{-1} \leq b^{-1}$ holds if and only if $b \leq a$.

ENNReal.inv_le_iff_inv_le theorem

: a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Full source

theorem inv_le_iff_inv_le : a⁻¹a⁻¹ ≤ b ↔ b⁻¹ ≤ a := by
  simpa only [inv_inv] using @ENNReal.inv_le_inv a b⁻¹

Inversion Order Equivalence in Extended Non-Negative Reals: $a^{-1} \leq b \leftrightarrow b^{-1} \leq a$

Informal description

For any extended non-negative real numbers $a$ and $b$, the inequality $a^{-1} \leq b$ holds if and only if $b^{-1} \leq a$.

ENNReal.le_inv_iff_le_inv theorem

: a ≤ b⁻¹ ↔ b ≤ a⁻¹

Full source

theorem le_inv_iff_le_inv : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := by
  simpa only [inv_inv] using @ENNReal.inv_le_inv a⁻¹ b

Order Reversal via Inversion in Extended Non-Negative Reals: $a \leq b^{-1} \leftrightarrow b \leq a^{-1}$

Informal description

For any extended non-negative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a \leq b^{-1}$ holds if and only if $b \leq a^{-1}$.

ENNReal.inv_le_inv' theorem

(h : a ≤ b) : b⁻¹ ≤ a⁻¹

Full source

@[gcongr] protected theorem inv_le_inv' (h : a ≤ b) : b⁻¹ ≤ a⁻¹ :=
  ENNReal.inv_strictAnti.antitone h

Antitonicity of Inversion in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b$, then the multiplicative inverses satisfy $b^{-1} \leq a^{-1}$.

ENNReal.inv_lt_inv' theorem

(h : a < b) : b⁻¹ < a⁻¹

Full source

@[gcongr] protected theorem inv_lt_inv' (h : a < b) : b⁻¹ < a⁻¹ := ENNReal.inv_strictAnti h

Strict Antitonicity of Inversion in Extended Non-Negative Reals: $a < b \Rightarrow b^{-1} < a^{-1}$

Informal description

For any extended non-negative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b$, then their multiplicative inverses satisfy $b^{-1} < a^{-1}$.

ENNReal.inv_le_one theorem

: a⁻¹ ≤ 1 ↔ 1 ≤ a

Full source

@[simp]
protected theorem inv_le_one : a⁻¹a⁻¹ ≤ 1 ↔ 1 ≤ a := by rw [inv_le_iff_inv_le, inv_one]

Inversion Inequality: $a^{-1} \leq 1 \leftrightarrow 1 \leq a$ in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$, the inequality $a^{-1} \leq 1$ holds if and only if $1 \leq a$.

ENNReal.one_le_inv theorem

: 1 ≤ a⁻¹ ↔ a ≤ 1

Full source

protected theorem one_le_inv : 1 ≤ a⁻¹ ↔ a ≤ 1 := by rw [le_inv_iff_le_inv, inv_one]

Inversion Reverses Order for Extended Non-Negative Reals: $1 \leq a^{-1} \leftrightarrow a \leq 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $1 \leq a^{-1}$ holds if and only if $a \leq 1$.

ENNReal.inv_lt_one theorem

: a⁻¹ < 1 ↔ 1 < a

Full source

@[simp]
protected theorem inv_lt_one : a⁻¹a⁻¹ < 1 ↔ 1 < a := by rw [inv_lt_iff_inv_lt, inv_one]

Inversion Inequality: $a^{-1} < 1 \leftrightarrow 1 < a$

Informal description

For any extended non-negative real number $a$, the inequality $a^{-1} < 1$ holds if and only if $1 < a$.

ENNReal.one_lt_inv theorem

: 1 < a⁻¹ ↔ a < 1

Full source

@[simp]
protected theorem one_lt_inv : 1 < a⁻¹ ↔ a < 1 := by rw [lt_inv_iff_lt_inv, inv_one]

Inequality between One and Inverse in Extended Non-Negative Reals: $1 < a^{-1} \leftrightarrow a < 1$

Informal description

For any extended non-negative real number $a$, the inequality $1 < a^{-1}$ holds if and only if $a < 1$.

OrderIso.invENNReal definition

: ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ

Full source

/-- The inverse map `fun x ↦ x⁻¹` is an order isomorphism between `ℝ≥0∞` and its `OrderDual` -/
@[simps! apply]
def _root_.OrderIso.invENNReal : ℝ≥0∞ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ where
  map_rel_iff' := ENNReal.inv_le_inv
  toEquiv := (Equiv.inv ℝ≥0∞).trans OrderDual.toDual

Order isomorphism of inversion on extended non-negative reals

Informal description

The map $x \mapsto x^{-1}$ is an order isomorphism between the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and its order dual, where the order is reversed. This means that for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, we have $a^{-1} \leq b^{-1}$ if and only if $b \leq a$.

OrderIso.invENNReal_symm_apply theorem

(a : ℝ≥0∞ᵒᵈ) : OrderIso.invENNReal.symm a = (OrderDual.ofDual a)⁻¹

Full source

@[simp]
theorem _root_.OrderIso.invENNReal_symm_apply (a : ℝ≥0∞ℝ≥0∞ᵒᵈ) :
    OrderIso.invENNReal.symm a = (OrderDual.ofDual a)⁻¹ :=
  rfl

Symmetric Application of Inversion Order Isomorphism on Extended Non-Negative Reals: $\text{invENNReal.symm}(a) = (\text{ofDual}(a))^{-1}$

Informal description

For any element $a$ in the order dual of the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the symmetric application of the order isomorphism `invENNReal` satisfies $\text{invENNReal.symm}(a) = (\text{ofDual}(a))^{-1}$.

ENNReal.div_top theorem

: a / ∞ = 0

Full source

@[simp] theorem div_top : a / ∞ = 0 := by rw [div_eq_mul_inv, inv_top, mul_zero]

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

Informal description

For any extended non-negative real number $a$, the division of $a$ by $\infty$ is equal to $0$, i.e., $a / \infty = 0$.

ENNReal.top_div theorem

: ∞ / a = if a = ∞ then 0 else ∞

Full source

theorem top_div : ∞ / a = if a = ∞ then 0 else ∞ := by simp [div_eq_mul_inv, top_mul']

Division of Infinity in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$, the division of $\infty$ by $a$ is defined as: \[ \infty / a = \begin{cases} 0 & \text{if } a = \infty, \\ \infty & \text{otherwise.} \end{cases} \]

ENNReal.top_div_of_ne_top theorem

(h : a ≠ ∞) : ∞ / a = ∞

Full source

theorem top_div_of_ne_top (h : a ≠ ∞) : ∞ / a = ∞ := by simp [top_div, h]

Division of Infinity by Finite Extended Non-Negative Real

Informal description

For any extended non-negative real number $a$ such that $a \neq \infty$, the division of $\infty$ by $a$ equals $\infty$, i.e., $\infty / a = \infty$.

ENNReal.top_div_coe theorem

: ∞ / p = ∞

Full source

@[simp] theorem top_div_coe : ∞ / p = ∞ := top_div_of_ne_top coe_ne_top

Division of Infinity by Finite Non-Negative Real Yields Infinity

Informal description

For any extended non-negative real number $p$ (i.e., $p \in \mathbb{R}_{\geq 0}$), the division of $\infty$ by $p$ equals $\infty$, i.e., $\infty / p = \infty$.

ENNReal.top_div_of_lt_top theorem

(h : a < ∞) : ∞ / a = ∞

Full source

theorem top_div_of_lt_top (h : a < ∞) : ∞ / a = ∞ := top_div_of_ne_top h.ne

Division of Infinity by Finite Extended Non-Negative Real Yields Infinity

Informal description

For any extended non-negative real number $a$ such that $a < \infty$, the division of $\infty$ by $a$ equals $\infty$, i.e., $\infty / a = \infty$.

ENNReal.zero_div theorem

: 0 / a = 0

Full source

@[simp] protected theorem zero_div : 0 / a = 0 := zero_mul a⁻¹

Division of Zero by Any Extended Non-Negative Real Number is Zero

Informal description

For any extended non-negative real number $a$, the division of $0$ by $a$ equals $0$, i.e., $0 / a = 0$.

ENNReal.div_eq_top theorem

: a / b = ∞ ↔ a ≠ 0 ∧ b = 0 ∨ a = ∞ ∧ b ≠ ∞

Full source

theorem div_eq_top : a / b = ∞ ↔ a ≠ 0 ∧ b = 0 ∨ a = ∞ ∧ b ≠ ∞ := by
  simp [div_eq_mul_inv, ENNReal.mul_eq_top]

Characterization of Extended Non-Negative Real Division Equaling Infinity

Informal description

For extended non-negative real numbers $a$ and $b$, the division $a / b$ equals infinity ($\infty$) if and only if either: 1. $a$ is non-zero and $b$ is zero, or 2. $a$ is infinity and $b$ is not infinity.

ENNReal.le_div_iff_mul_le theorem

(h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) : a ≤ c / b ↔ a * b ≤ c

Full source

protected theorem le_div_iff_mul_le (h0 : b ≠ 0b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞b ≠ ∞ ∨ c ≠ ∞) :
    a ≤ c / b ↔ a * b ≤ c := by
  induction' b with b
  · lift c to ℝ≥0 using ht.neg_resolve_left rfl
    rw [div_top, nonpos_iff_eq_zero]
    rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
  rcases eq_or_ne b 0 with (rfl | hb)
  · have hc : c ≠ 0 := h0.neg_resolve_left rfl
    simp [div_zero hc]
  · rw [← coe_ne_zero] at hb
    rw [← ENNReal.mul_le_mul_right hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

Inequality Characterization: $a \leq c / b \leftrightarrow a \cdot b \leq c$ in Extended Non-Negative Reals

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that either $b \neq 0$ or $c \neq 0$, and either $b \neq \infty$ or $c \neq \infty$, the inequality $a \leq c / b$ holds if and only if $a \cdot b \leq c$.

ENNReal.div_le_iff_le_mul theorem

(hb0 : b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞ ∨ c ≠ 0) : a / b ≤ c ↔ a ≤ c * b

Full source

protected theorem div_le_iff_le_mul (hb0 : b ≠ 0b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞b ≠ ∞ ∨ c ≠ 0) :
    a / b ≤ c ↔ a ≤ c * b := by
  suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]
  refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm <;> simpa

Division-Multiplication Inequality in Extended Non-Negative Reals: $a / b \leq c \leftrightarrow a \leq c \cdot b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that either $b \neq 0$ or $c \neq \infty$, and either $b \neq \infty$ or $c \neq 0$, the inequality $a / b \leq c$ holds if and only if $a \leq c \cdot b$.

ENNReal.lt_div_iff_mul_lt theorem

(hb0 : b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞ ∨ c ≠ 0) : c < a / b ↔ c * b < a

Full source

protected theorem lt_div_iff_mul_lt (hb0 : b ≠ 0b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞b ≠ ∞ ∨ c ≠ 0) :
    c < a / b ↔ c * b < a :=
  lt_iff_lt_of_le_iff_le (ENNReal.div_le_iff_le_mul hb0 hbt)

Strict Division-Multiplication Inequality in Extended Non-Negative Reals: $c < a / b \leftrightarrow c \cdot b < a$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that either $b \neq 0$ or $c \neq \infty$, and either $b \neq \infty$ or $c \neq 0$, the strict inequality $c < a / b$ holds if and only if $c \cdot b < a$.

ENNReal.div_le_of_le_mul theorem

(h : a ≤ b * c) : a / c ≤ b

Full source

theorem div_le_of_le_mul (h : a ≤ b * c) : a / c ≤ b := by
  by_cases h0 : c = 0
  · have : a = 0 := by simpa [h0] using h
    simp [*]
  by_cases hinf : c = ∞; · simp [hinf]
  exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

Division Inequality from Multiplication in Extended Non-Negative Reals: $a \leq b \cdot c \Rightarrow a / c \leq b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b \cdot c$, then $a / c \leq b$.

ENNReal.div_le_of_le_mul' theorem

(h : a ≤ b * c) : a / b ≤ c

Full source

theorem div_le_of_le_mul' (h : a ≤ b * c) : a / b ≤ c :=
  div_le_of_le_mul <| mul_comm b c ▸ h

Division Inequality from Multiplication in Extended Non-Negative Reals (Symmetric Version)

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b \cdot c$, then $a / b \leq c$.

ENNReal.div_self_le_one theorem

: a / a ≤ 1

Full source

@[simp] protected theorem div_self_le_one : a / a ≤ 1 := div_le_of_le_mul <| by rw [one_mul]

Self-division inequality in extended non-negative reals: $a / a \leq 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the division of $a$ by itself is less than or equal to $1$, i.e., $a / a \leq 1$.

ENNReal.mul_inv_le_one theorem

(a : ℝ≥0∞) : a * a⁻¹ ≤ 1

Full source

@[simp] protected lemma mul_inv_le_one (a : ℝ≥0∞) : a * a⁻¹ ≤ 1 := ENNReal.div_self_le_one

Product-Inverse Inequality in Extended Non-Negative Reals: $a \cdot a^{-1} \leq 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of $a$ and its multiplicative inverse $a^{-1}$ is less than or equal to $1$, i.e., $a \cdot a^{-1} \leq 1$.

ENNReal.inv_mul_le_one theorem

(a : ℝ≥0∞) : a⁻¹ * a ≤ 1

Full source

@[simp] protected lemma inv_mul_le_one (a : ℝ≥0∞) : a⁻¹ * a ≤ 1 := by simp [mul_comm]

Inverse-product inequality in extended non-negative reals: $a^{-1} \cdot a \leq 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of its multiplicative inverse $a^{-1}$ and $a$ itself is less than or equal to $1$, i.e., $a^{-1} \cdot a \leq 1$.

ENNReal.mul_inv_ne_top theorem

(a : ℝ≥0∞) : a * a⁻¹ ≠ ⊤

Full source

@[simp] lemma mul_inv_ne_top (a : ℝ≥0∞) : a * a⁻¹ ≠ ⊤ :=
  ne_top_of_le_ne_top one_ne_top a.mul_inv_le_one

Non-infinity of Product-Inverse in Extended Non-Negative Reals: $a \cdot a^{-1} \neq \infty$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of $a$ and its multiplicative inverse $a^{-1}$ is not equal to $\infty$, i.e., $a \cdot a^{-1} \neq \infty$.

ENNReal.inv_mul_ne_top theorem

(a : ℝ≥0∞) : a⁻¹ * a ≠ ⊤

Full source

@[simp] lemma inv_mul_ne_top (a : ℝ≥0∞) : a⁻¹a⁻¹ * a ≠ ⊤ := by simp [mul_comm]

Non-infinity of inverse-product in extended non-negative reals

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of its multiplicative inverse $a^{-1}$ and $a$ itself is not equal to $\infty$, i.e., $a^{-1} \cdot a \neq \infty$.

ENNReal.mul_le_of_le_div theorem

(h : a ≤ b / c) : a * c ≤ b

Full source

theorem mul_le_of_le_div (h : a ≤ b / c) : a * c ≤ b := by
  rw [← inv_inv c]
  exact div_le_of_le_mul h

Multiplication Inequality from Division in Extended Non-Negative Reals: $a \leq b / c \Rightarrow a \cdot c \leq b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b / c$, then $a \cdot c \leq b$.

ENNReal.mul_le_of_le_div' theorem

(h : a ≤ b / c) : c * a ≤ b

Full source

theorem mul_le_of_le_div' (h : a ≤ b / c) : c * a ≤ b :=
  mul_comm a c ▸ mul_le_of_le_div h

Multiplication Inequality from Division in Extended Non-Negative Reals (Commutative Version): $a \leq b / c \Rightarrow c \cdot a \leq b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b / c$, then $c \cdot a \leq b$.

ENNReal.div_lt_iff theorem

(h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) : c / b < a ↔ c < a * b

Full source

protected theorem div_lt_iff (h0 : b ≠ 0b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞b ≠ ∞ ∨ c ≠ ∞) : c / b < a ↔ c < a * b :=
  lt_iff_lt_of_le_iff_le <| ENNReal.le_div_iff_mul_le h0 ht

Inequality Characterization: $c / b < a \leftrightarrow c < a \cdot b$ in Extended Non-Negative Reals

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that either $b \neq 0$ or $c \neq 0$, and either $b \neq \infty$ or $c \neq \infty$, the inequality $c / b < a$ holds if and only if $c < a \cdot b$.

ENNReal.mul_lt_of_lt_div theorem

(h : a < b / c) : a * c < b

Full source

theorem mul_lt_of_lt_div (h : a < b / c) : a * c < b := by
  contrapose! h
  exact ENNReal.div_le_of_le_mul h

Multiplication Inequality from Division in Extended Non-Negative Reals: $a < b / c \Rightarrow a \cdot c < b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b / c$, then $a \cdot c < b$.

ENNReal.mul_lt_of_lt_div' theorem

(h : a < b / c) : c * a < b

Full source

theorem mul_lt_of_lt_div' (h : a < b / c) : c * a < b :=
  mul_comm a c ▸ mul_lt_of_lt_div h

Multiplication Inequality from Division in Extended Non-Negative Reals (Commutative Version): $a < b / c \Rightarrow c \cdot a < b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b / c$, then $c \cdot a < b$.

ENNReal.div_lt_of_lt_mul theorem

(h : a < b * c) : a / c < b

Full source

theorem div_lt_of_lt_mul (h : a < b * c) : a / c < b :=
  mul_lt_of_lt_div <| by rwa [div_eq_mul_inv, inv_inv]

Division Inequality from Multiplication in Extended Non-Negative Reals: $a < b \cdot c \Rightarrow a / c < b$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b \cdot c$, then $a / c < b$.

ENNReal.div_lt_of_lt_mul' theorem

(h : a < b * c) : a / b < c

Full source

theorem div_lt_of_lt_mul' (h : a < b * c) : a / b < c :=
  div_lt_of_lt_mul <| by rwa [mul_comm]

Division Inequality from Multiplication in Extended Non-Negative Reals (Symmetric Version): $a < b \cdot c \Rightarrow a / b < c$

Informal description

For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b \cdot c$, then $a / b < c$.

ENNReal.inv_le_iff_le_mul theorem

(h₁ : b = ∞ → a ≠ 0) (h₂ : a = ∞ → b ≠ 0) : a⁻¹ ≤ b ↔ 1 ≤ a * b

Full source

theorem inv_le_iff_le_mul (h₁ : b = ∞ → a ≠ 0) (h₂ : a = ∞ → b ≠ 0) : a⁻¹a⁻¹ ≤ b ↔ 1 ≤ a * b := by
  rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
  exacts [or_not_of_imp h₁, not_or_of_imp h₂]

Inverse-Multiplication Inequality in Extended Non-Negative Reals: $a^{-1} \leq b \leftrightarrow 1 \leq a \cdot b$

Informal description

For extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that if $b = \infty$ then $a \neq 0$, and if $a = \infty$ then $b \neq 0$, the inequality $a^{-1} \leq b$ holds if and only if $1 \leq a \cdot b$.

ENNReal.le_inv_iff_mul_le theorem

: a ≤ b⁻¹ ↔ a * b ≤ 1

Full source

@[simp 900]
theorem le_inv_iff_mul_le : a ≤ b⁻¹ ↔ a * b ≤ 1 := by
  rw [← one_div, ENNReal.le_div_iff_mul_le] <;>
    · right
      simp

Inverse Inequality Characterization: $a \leq b^{-1} \leftrightarrow a \cdot b \leq 1$ in Extended Non-Negative Reals

Informal description

For extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a \leq b^{-1}$ holds if and only if $a \cdot b \leq 1$.

ENNReal.div_le_div theorem

(hab : a ≤ b) (hdc : d ≤ c) : a / c ≤ b / d

Full source

@[gcongr] protected theorem div_le_div (hab : a ≤ b) (hdc : d ≤ c) : a / c ≤ b / d :=
  div_eq_mul_inv b d ▸ div_eq_mul_inv a c ▸ mul_le_mul' hab (ENNReal.inv_le_inv.mpr hdc)

Division Preserves Order in Extended Non-Negative Reals: $\frac{a}{c} \leq \frac{b}{d}$ under $a \leq b$ and $d \leq c$

Informal description

For any extended non-negative real numbers $a, b, c, d$ such that $a \leq b$ and $d \leq c$, the inequality $\frac{a}{c} \leq \frac{b}{d}$ holds.

ENNReal.div_le_div_left theorem

(h : a ≤ b) (c : ℝ≥0∞) : c / b ≤ c / a

Full source

@[gcongr] protected theorem div_le_div_left (h : a ≤ b) (c : ℝ≥0∞) : c / b ≤ c / a :=
  ENNReal.div_le_div le_rfl h

Left Division Preserves Order in Extended Non-Negative Reals: $\frac{c}{b} \leq \frac{c}{a}$ under $a \leq b$

Informal description

For any extended non-negative real numbers $a, b, c$ such that $a \leq b$, the inequality $\frac{c}{b} \leq \frac{c}{a}$ holds.

ENNReal.div_le_div_right theorem

(h : a ≤ b) (c : ℝ≥0∞) : a / c ≤ b / c

Full source

@[gcongr] protected theorem div_le_div_right (h : a ≤ b) (c : ℝ≥0∞) : a / c ≤ b / c :=
  ENNReal.div_le_div h le_rfl

Right Division Preserves Order in Extended Non-Negative Reals: $\frac{a}{c} \leq \frac{b}{c}$ under $a \leq b$

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \leq b$, the inequality $\frac{a}{c} \leq \frac{b}{c}$ holds.

ENNReal.mul_le_iff_le_inv theorem

{a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : r * a ≤ b ↔ a ≤ r⁻¹ * b

Full source

theorem mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : r * a ≤ b ↔ a ≤ r⁻¹ * b := by
  rw [← @ENNReal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]

Multiplication-Inequality Equivalence for Extended Non-Negative Reals: $r \cdot a \leq b \leftrightarrow a \leq r^{-1} \cdot b$

Informal description

For any extended non-negative real numbers $a, b, r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $r \neq 0$ and $r \neq \infty$, the inequality $r \cdot a \leq b$ holds if and only if $a \leq r^{-1} \cdot b$.

ENNReal.le_of_forall_nnreal_lt theorem

{x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y

Full source

theorem le_of_forall_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r < x → ↑r ≤ y) : x ≤ y := by
  refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
  lift r to ℝ≥0 using ne_top_of_lt hr
  exact h r hr

Extended Non-Negative Real Ordering via Non-Negative Real Comparisons

Informal description

For any extended non-negative real numbers $x$ and $y$, if for every non-negative real number $r$ the condition $r < x$ implies $r \leq y$, then $x \leq y$.

ENNReal.le_of_forall_pos_nnreal_lt theorem

{x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, 0 < r → ↑r < x → ↑r ≤ y) : x ≤ y

Full source

theorem le_of_forall_pos_nnreal_lt {x y : ℝ≥0∞} (h : ∀ r : ℝ≥0, 0 < r → ↑r < x → ↑r ≤ y) : x ≤ y :=
  le_of_forall_nnreal_lt fun r hr =>
    (zero_le r).eq_or_lt.elim (fun h => h ▸ zero_le _) fun h0 => h r h0 hr

Extended Non-Negative Real Ordering via Positive Non-Negative Real Comparisons

Informal description

For any extended non-negative real numbers $x$ and $y$, if for every positive non-negative real number $r$ the conditions $0 < r$ and $r < x$ imply $r \leq y$, then $x \leq y$.

ENNReal.add_div theorem

: (a + b) / c = a / c + b / c

Full source

protected theorem add_div : (a + b) / c = a / c + b / c :=
  right_distrib a b c⁻¹

Distributivity of Division over Addition in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a$, $b$, and $c$, the division of their sum by $c$ equals the sum of their individual divisions by $c$, i.e., $(a + b) / c = a / c + b / c$.

ENNReal.div_add_div_same theorem

{a b c : ℝ≥0∞} : a / c + b / c = (a + b) / c

Full source

protected theorem div_add_div_same {a b c : ℝ≥0∞} : a / c + b / c = (a + b) / c :=
  ENNReal.add_div.symm

Additivity of Division in Extended Non-Negative Reals: $a/c + b/c = (a+b)/c$

Informal description

For any extended non-negative real numbers $a$, $b$, and $c$, the sum of their individual divisions by $c$ equals the division of their sum by $c$, i.e., $a / c + b / c = (a + b) / c$.

ENNReal.div_self theorem

(h0 : a ≠ 0) (hI : a ≠ ∞) : a / a = 1

Full source

protected theorem div_self (h0 : a ≠ 0) (hI : a ≠ ∞) : a / a = 1 :=
  ENNReal.mul_inv_cancel h0 hI

Division Identity for Nonzero Finite Extended Non-Negative Reals: $a/a = 1$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the division of $a$ by itself equals $1$, i.e., $a / a = 1$.

ENNReal.mul_div_le theorem

: a * (b / a) ≤ b

Full source

theorem mul_div_le : a * (b / a) ≤ b :=
  mul_le_of_le_div' le_rfl

Upper Bound for Multiplication by Division in Extended Non-Negative Reals: $a \cdot (b/a) \leq b$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a \cdot (b / a) \leq b$ holds.

ENNReal.div_eq_div_iff theorem

(ha : a ≠ 0) (ha' : a ≠ ∞) (hb : b ≠ 0) (hb' : b ≠ ∞) : c / b = d / a ↔ a * c = b * d

Full source

protected theorem div_eq_div_iff (ha : a ≠ 0) (ha' : a ≠ ∞) (hb : b ≠ 0) (hb' : b ≠ ∞) :
    c / b = d / a ↔ a * c = b * d := by
  rw [eq_div_iff ha ha']
  conv_rhs => rw [eq_comm]
  rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]

Equivalence of Division and Cross-Multiplication in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b, c, d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$, $a \neq \infty$, $b \neq 0$, and $b \neq \infty$, the equality $\frac{c}{b} = \frac{d}{a}$ holds if and only if $a \cdot c = b \cdot d$.

ENNReal.div_eq_one_iff theorem

{a b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb₁ : b ≠ ∞) : a / b = 1 ↔ a = b

Full source

theorem div_eq_one_iff {a b : ℝ≥0∞} (hb₀ : b ≠ 0) (hb₁ : b ≠ ∞) : a / b = 1 ↔ a = b :=
  ⟨fun h => by rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one], fun h =>
    h.symm ▸ ENNReal.div_self hb₀ hb₁⟩

Division Equals One iff Equality for Nonzero Finite Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $b \neq 0$ and $b \neq \infty$, the division $a / b$ equals $1$ if and only if $a = b$.

ENNReal.inv_two_add_inv_two theorem

: (2 : ℝ≥0∞)⁻¹ + 2⁻¹ = 1

Full source

theorem inv_two_add_inv_two : (2 : ℝ≥0∞)⁻¹ + 2⁻¹ = 1 := by
  rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]

Sum of Halves in Extended Non-Negative Reals: $\frac{1}{2} + \frac{1}{2} = 1$

Informal description

The sum of the reciprocals of $2$ in the extended non-negative real numbers equals $1$, i.e., $\frac{1}{2} + \frac{1}{2} = 1$.

ENNReal.inv_three_add_inv_three theorem

: (3 : ℝ≥0∞)⁻¹ + 3⁻¹ + 3⁻¹ = 1

Full source

theorem inv_three_add_inv_three : (3 : ℝ≥0∞)⁻¹ + 3⁻¹ + 3⁻¹ = 1 := by
  rw [← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top]
  ring

Sum of Thirds in Extended Non-Negative Reals: $\frac{1}{3} + \frac{1}{3} + \frac{1}{3} = 1$

Informal description

The sum of three copies of the reciprocal of $3$ in the extended non-negative real numbers equals $1$, i.e., $\frac{1}{3} + \frac{1}{3} + \frac{1}{3} = 1$.

ENNReal.add_halves theorem

(a : ℝ≥0∞) : a / 2 + a / 2 = a

Full source

@[simp]
protected theorem add_halves (a : ℝ≥0∞) : a / 2 + a / 2 = a := by
  rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]

Additive Halving Identity in Extended Non-Negative Reals: $\frac{a}{2} + \frac{a}{2} = a$

Informal description

For any extended non-negative real number $a$, the sum of $a$ divided by 2 and itself equals $a$, i.e., $\frac{a}{2} + \frac{a}{2} = a$.

ENNReal.add_thirds theorem

(a : ℝ≥0∞) : a / 3 + a / 3 + a / 3 = a

Full source

@[simp]
theorem add_thirds (a : ℝ≥0∞) : a / 3 + a / 3 + a / 3 = a := by
  rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]

Additive Thirds Identity in Extended Non-Negative Reals: $\frac{a}{3} + \frac{a}{3} + \frac{a}{3} = a$

Informal description

For any extended non-negative real number $a$, the sum of three equal parts of $a$ divided by 3 equals $a$, i.e., $\frac{a}{3} + \frac{a}{3} + \frac{a}{3} = a$.

ENNReal.div_eq_zero_iff theorem

: a / b = 0 ↔ a = 0 ∨ b = ∞

Full source

@[simp] theorem div_eq_zero_iff : a / b = 0 ↔ a = 0 ∨ b = ∞ := by simp [div_eq_mul_inv]

Division Zero Criterion in Extended Non-Negative Reals: $a / b = 0 \leftrightarrow (a = 0 \lor b = \infty)$

Informal description

For any extended non-negative real numbers $a$ and $b$, the division $a / b$ equals zero if and only if either $a = 0$ or $b = \infty$.

ENNReal.div_pos_iff theorem

: 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Full source

@[simp] theorem div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞ := by simp [pos_iff_ne_zero, not_or]

Positivity Criterion for Division in Extended Non-Negative Reals: $0 < a / b \leftrightarrow (a \neq 0 \land b \neq \infty)$

Informal description

For any extended non-negative real numbers $a$ and $b$, the division $a / b$ is strictly positive if and only if $a \neq 0$ and $b \neq \infty$. In other words, $0 < a / b \leftrightarrow (a \neq 0 \land b \neq \infty)$.

ENNReal.div_ne_zero theorem

: a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Full source

protected lemma div_ne_zero : a / b ≠ 0a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞ := by
  rw [← pos_iff_ne_zero, div_pos_iff]

Nonzero Division Criterion in Extended Non-Negative Reals: $a / b \neq 0 \leftrightarrow (a \neq 0 \land b \neq \infty)$

Informal description

For any extended non-negative real numbers $a$ and $b$, the division $a / b$ is nonzero if and only if $a \neq 0$ and $b \neq \infty$. In other words, $a / b \neq 0 \leftrightarrow (a \neq 0 \land b \neq \infty)$.

ENNReal.div_mul theorem

(a : ℝ≥0∞) (h0 : b ≠ 0 ∨ c ≠ 0) (htop : b ≠ ∞ ∨ c ≠ ∞) : a / b * c = a / (b / c)

Full source

protected lemma div_mul (a : ℝ≥0∞) (h0 : b ≠ 0b ≠ 0 ∨ c ≠ 0) (htop : b ≠ ∞b ≠ ∞ ∨ c ≠ ∞) :
    a / b * c = a / (b / c) := by
  simp only [div_eq_mul_inv]
  rw [ENNReal.mul_inv, inv_inv]
  · ring
  · simpa
  · simpa

Division-Multiplication Identity in Extended Non-Negative Reals: $(a / b) \cdot c = a / (b / c)$ under given conditions

Informal description

For any extended non-negative real numbers $a, b, c$ such that either $b \neq 0$ or $c \neq 0$, and either $b \neq \infty$ or $c \neq \infty$, the following equality holds: \[ (a / b) \cdot c = a / (b / c). \]

ENNReal.mul_div_mul_comm theorem

(hc : c ≠ 0 ∨ d ≠ ∞) (hd : c ≠ ∞ ∨ d ≠ 0) : a * b / (c * d) = a / c * (b / d)

Full source

protected lemma mul_div_mul_comm (hc : c ≠ 0c ≠ 0 ∨ d ≠ ∞) (hd : c ≠ ∞c ≠ ∞ ∨ d ≠ 0) :
    a * b / (c * d) = a / c * (b / d) := by
  simp only [div_eq_mul_inv, ENNReal.mul_inv hc hd]
  ring

Commutative Property of Multiplication and Division in Extended Non-Negative Reals: $\frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d}$ under given conditions

Informal description

For any extended non-negative real numbers $a, b, c, d$ such that either $c \neq 0$ or $d \neq \infty$, and either $c \neq \infty$ or $d \neq 0$, the following equality holds: $$ \frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d} $$

ENNReal.half_pos theorem

(h : a ≠ 0) : 0 < a / 2

Full source

protected theorem half_pos (h : a ≠ 0) : 0 < a / 2 :=
  ENNReal.div_pos h ofNat_ne_top

Positivity of Half in Extended Non-Negative Reals: $0 < a / 2$ when $a \neq 0$

Informal description

For any extended non-negative real number $a \neq 0$, the division $a / 2$ is strictly positive, i.e., $0 < a / 2$.

ENNReal.one_half_lt_one theorem

: (2⁻¹ : ℝ≥0∞) < 1

Full source

protected theorem one_half_lt_one : (2⁻¹ : ℝ≥0∞) < 1 :=
  ENNReal.inv_lt_one.2 <| one_lt_two

Inequality for Half in Extended Non-Negative Reals: $\frac{1}{2} < 1$

Informal description

The extended non-negative real number $2^{-1}$ is strictly less than $1$, i.e., $\frac{1}{2} < 1$.

ENNReal.half_lt_self theorem

(hz : a ≠ 0) (ht : a ≠ ∞) : a / 2 < a

Full source

protected theorem half_lt_self (hz : a ≠ 0) (ht : a ≠ ∞) : a / 2 < a := by
  lift a to ℝ≥0 using ht
  rw [coe_ne_zero] at hz
  rw [← coe_two, ← coe_div, coe_lt_coe]
  exacts [NNReal.half_lt_self hz, two_ne_zero' _]

Strict Inequality for Halves in Extended Non-Negative Reals: $a / 2 < a$ when $0 < a < \infty$

Informal description

For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, the inequality $a / 2 < a$ holds.

ENNReal.half_le_self theorem

: a / 2 ≤ a

Full source

protected theorem half_le_self : a / 2 ≤ a :=
  le_add_self.trans_eq <| ENNReal.add_halves _

Non-Strict Inequality for Halves in Extended Non-Negative Reals: $a / 2 \leq a$

Informal description

For any extended non-negative real number $a$, the inequality $a / 2 \leq a$ holds.

ENNReal.sub_half theorem

(h : a ≠ ∞) : a - a / 2 = a / 2

Full source

theorem sub_half (h : a ≠ ∞) : a - a / 2 = a / 2 := ENNReal.sub_eq_of_eq_add' h a.add_halves.symm

Subtraction of Half Identity in Extended Non-Negative Reals: $a - \frac{a}{2} = \frac{a}{2}$ for $a \neq \infty$

Informal description

For any extended non-negative real number $a \neq \infty$, the difference $a - \frac{a}{2}$ equals $\frac{a}{2}$.

ENNReal.one_sub_inv_two theorem

: (1 : ℝ≥0∞) - 2⁻¹ = 2⁻¹

Full source

@[simp]
theorem one_sub_inv_two : (1 : ℝ≥0∞) - 2⁻¹ = 2⁻¹ := by
  rw [← one_div, sub_half one_ne_top]

Subtraction Identity for One and Half in Extended Non-Negative Reals: $1 - \frac{1}{2} = \frac{1}{2}$

Informal description

For the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, we have the identity $1 - \frac{1}{2} = \frac{1}{2}$.

ENNReal.mul_le_of_forall_lt theorem

{a b c : ℝ≥0∞} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c

Full source

lemma mul_le_of_forall_lt {a b c : ℝ≥0∞} (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_mul_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
  exact le_trans hd.le <| h _ ha' _ hb'

Product Inequality in Extended Non-Negative Reals via Pointwise Bounds

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if for all $a' < a$ and $b' < b$ we have $a' \cdot b' \leq c$, then $a \cdot b \leq c$.

ENNReal.le_mul_of_forall_lt theorem

 {a b c : ℝ≥0∞} (h₁ : a ≠ 0 ∨ b ≠ ∞) (h₂ : a ≠ ∞ ∨ b ≠ 0) (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

Full source

lemma le_mul_of_forall_lt {a b c : ℝ≥0∞} (h₁ : a ≠ 0a ≠ 0 ∨ b ≠ ∞) (h₂ : a ≠ ∞a ≠ ∞ ∨ b ≠ 0)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b := by
  rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]
  exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

Lower Bound on Product via Pointwise Bounds in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that either $a \neq 0$ or $b \neq \infty$, and either $a \neq \infty$ or $b \neq 0$, if for all $a' > a$ and $b' > b$ we have $c \leq a' \cdot b'$, then $c \leq a \cdot b$.

ENNReal.orderIsoIicOneBirational definition

: ℝ≥0∞ ≃o Iic (1 : ℝ≥0∞)

Full source

/-- The birational order isomorphism between `ℝ≥0∞` and the unit interval `Set.Iic (1 : ℝ≥0∞)`. -/
@[simps! apply_coe]
def orderIsoIicOneBirational : ℝ≥0∞ℝ≥0∞ ≃o Iic (1 : ℝ≥0∞) := by
  refine StrictMono.orderIsoOfRightInverse
    (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩)
    (fun x y hxy => ?_) (fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_
  · simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]
  · have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
    simp only [inv_inv, Subtype.coe_mk, tsub_add_cancel_of_le this]

Birational order isomorphism between extended non-negative reals and the unit interval

Informal description

The birational order isomorphism between the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and the unit interval $(-\infty, 1] \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$ is given by the map $x \mapsto (x^{-1} + 1)^{-1}$, with inverse $y \mapsto (y^{-1} - 1)^{-1}$.

ENNReal.orderIsoIicOneBirational_symm_apply theorem

(x : Iic (1 : ℝ≥0∞)) : orderIsoIicOneBirational.symm x = (x.1⁻¹ - 1)⁻¹

Full source

@[simp]
theorem orderIsoIicOneBirational_symm_apply (x : Iic (1 : ℝ≥0∞)) :
    orderIsoIicOneBirational.symm x = (x.1⁻¹ - 1)⁻¹ :=
  rfl

Inverse Formula for Birational Order Isomorphism on $(-\infty, 1]$

Informal description

For any element $x$ in the interval $(-\infty, 1] \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inverse of the birational order isomorphism $\text{orderIsoIicOneBirational}$ evaluated at $x$ is given by $(x^{-1} - 1)^{-1}$.

ENNReal.orderIsoIicCoe definition

(a : ℝ≥0) : Iic (a : ℝ≥0∞) ≃o Iic a

Full source

/-- Order isomorphism between an initial interval in `ℝ≥0∞` and an initial interval in `ℝ≥0`. -/
@[simps! apply_coe]
def orderIsoIicCoe (a : ℝ≥0) : IicIic (a : ℝ≥0∞) ≃o Iic a :=
  OrderIso.symm
    { toFun := fun x => ⟨x, coe_le_coe.2 x.2⟩
      invFun := fun x => ⟨ENNReal.toNNReal x, coe_le_coe.1 <| coe_toNNReal_le_self.trans x.2⟩
      left_inv := fun _ => Subtype.ext <| toNNReal_coe _
      right_inv := fun x => Subtype.ext <| coe_toNNReal (ne_top_of_le_ne_top coe_ne_top x.2)
      map_rel_iff' := fun {_ _} => by
        simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, coe_le_coe, Subtype.coe_le_coe] }

Order isomorphism between intervals in extended and non-negative reals

Informal description

For any non-negative real number $ a $, there is an order isomorphism between the left-infinite right-closed interval $ (-\infty, a] $ in the extended non-negative real numbers $ \mathbb{R}_{\geq 0} \cup \{\infty\} $ and the corresponding interval $ (-\infty, a] $ in the non-negative real numbers $ \mathbb{R}_{\geq 0} $. The isomorphism is given by the identity map, restricted to the appropriate subsets.

ENNReal.orderIsoIicCoe_symm_apply_coe theorem

(a : ℝ≥0) (b : Iic a) : ((orderIsoIicCoe a).symm b : ℝ≥0∞) = b

Full source

@[simp]
theorem orderIsoIicCoe_symm_apply_coe (a : ℝ≥0) (b : Iic a) :
    ((orderIsoIicCoe a).symm b : ℝ≥0∞) = b :=
  rfl

Inverse of Order Isomorphism Preserves Elements in $(-\infty, a]$

Informal description

For any non-negative real number $a$ and any element $b$ in the interval $(-\infty, a] \subseteq \mathbb{R}_{\geq 0}$, the image of $b$ under the inverse of the order isomorphism $\text{orderIsoIicCoe}\, a$ is equal to $b$ when viewed as an element of the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.orderIsoUnitIntervalBirational definition

: ℝ≥0∞ ≃o Icc (0 : ℝ) 1

Full source

/-- An order isomorphism between the extended nonnegative real numbers and the unit interval. -/
def orderIsoUnitIntervalBirational : ℝ≥0∞ℝ≥0∞ ≃o Icc (0 : ℝ) 1 :=
  orderIsoIicOneBirational.trans <| (orderIsoIicCoe 1).trans <| (NNReal.orderIsoIccZeroCoe 1).symm

Birational order isomorphism between extended non-negative reals and the unit interval

Informal description

The order isomorphism between the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and the closed unit interval $[0, 1] \subseteq \mathbb{R}$ is given by the composition of three isomorphisms: 1. The birational isomorphism $\mathbb{R}_{\geq 0} \cup \{\infty\} \simeq_o (-\infty, 1] \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$ defined by $x \mapsto (x^{-1} + 1)^{-1}$, 2. The identity isomorphism $(-\infty, 1] \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\} \simeq_o (-\infty, 1] \subseteq \mathbb{R}_{\geq 0}$, 3. The inverse of the isomorphism $[0, 1] \subseteq \mathbb{R}_{\geq 0} \simeq_o (-\infty, 1] \subseteq \mathbb{R}_{\geq 0}$.

ENNReal.orderIsoUnitIntervalBirational_apply_coe theorem

(x : ℝ≥0∞) : (orderIsoUnitIntervalBirational x : ℝ) = (x⁻¹ + 1)⁻¹.toReal

Full source

@[simp]
theorem orderIsoUnitIntervalBirational_apply_coe (x : ℝ≥0∞) :
    (orderIsoUnitIntervalBirational x : ℝ) = (x⁻¹ + 1)⁻¹.toReal :=
  rfl

Image of Extended Non-Negative Real under Birational Order Isomorphism to Unit Interval

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image of $x$ under the order isomorphism $\text{orderIsoUnitIntervalBirational}$ is equal to the real number obtained by applying the transformation $(x^{-1} + 1)^{-1}$ and then converting the result to a real number via the $\text{toReal}$ function.

ENNReal.exists_inv_nat_lt theorem

{a : ℝ≥0∞} (h : a ≠ 0) : ∃ n : ℕ, (n : ℝ≥0∞)⁻¹ < a

Full source

theorem exists_inv_nat_lt {a : ℝ≥0∞} (h : a ≠ 0) : ∃ n : ℕ, (n : ℝ≥0∞)⁻¹ < a :=
  inv_inv a ▸ by simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]

Existence of Natural Number with Inverse Less Than Given Nonzero Extended Non-Negative Real

Informal description

For any nonzero extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a natural number $n$ such that the multiplicative inverse of $n$ (considered as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$) is strictly less than $a$.

ENNReal.exists_nat_pos_mul_gt theorem

(ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n > 0, b < (n : ℕ) * a

Full source

theorem exists_nat_pos_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n > 0, b < (n : ℕ) * a :=
  let ⟨n, hn⟩ := ENNReal.exists_nat_gt (div_lt_top hb ha).ne
  ⟨n, Nat.cast_pos.1 ((zero_le _).trans_lt hn), by
    rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]⟩

Existence of Positive Natural Multiple Exceeding Given Extended Non-Negative Real

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq 0$ and $b \neq \infty$, there exists a positive natural number $n$ such that $b < n \cdot a$.

ENNReal.exists_nat_mul_gt theorem

(ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n : ℕ, b < n * a

Full source

theorem exists_nat_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n : ℕ, b < n * a :=
  (exists_nat_pos_mul_gt ha hb).imp fun _ => And.right

Existence of Natural Multiple Exceeding Given Extended Non-Negative Real

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq 0$ and $b \neq \infty$, there exists a natural number $n$ such that $b < n \cdot a$.

ENNReal.exists_nat_pos_inv_mul_lt theorem

(ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ((n : ℕ) : ℝ≥0∞)⁻¹ * a < b

Full source

theorem exists_nat_pos_inv_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) :
    ∃ n > 0, ((n : ℕ) : ℝ≥0∞)⁻¹ * a < b := by
  rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
  use n, npos
  rw [← ENNReal.div_eq_inv_mul]
  exact div_lt_of_lt_mul' hn

Existence of Positive Natural Scaling Factor for Extended Non-Negative Reals: $\frac{a}{n} < b$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq \infty$ and $b \neq 0$, there exists a positive natural number $n$ such that $\frac{a}{n} < b$.

ENNReal.exists_nnreal_pos_mul_lt theorem

(ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ↑(n : ℝ≥0) * a < b

Full source

theorem exists_nnreal_pos_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ↑(n : ℝ≥0) * a < b := by
  rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩
  use (n : ℝ≥0)⁻¹
  simp [*, npos.ne', zero_lt_one]

Existence of Positive Real Scaling Factor for Extended Non-Negative Reals: $n \cdot a < b$

Informal description

For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq \infty$ and $b \neq 0$, there exists a positive real number $n \in \mathbb{R}_{>0}$ such that $n \cdot a < b$.

ENNReal.exists_inv_two_pow_lt theorem

(ha : a ≠ 0) : ∃ n : ℕ, 2⁻¹ ^ n < a

Full source

theorem exists_inv_two_pow_lt (ha : a ≠ 0) : ∃ n : ℕ, 2⁻¹ ^ n < a := by
  rcases exists_inv_nat_lt ha with ⟨n, hn⟩
  refine ⟨n, lt_trans ?_ hn⟩
  rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]
  norm_cast
  exact n.lt_two_pow_self

Existence of Power of Half Less Than Any Nonzero Extended Non-Negative Real

Informal description

For any nonzero extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a natural number $n$ such that $(2^{-1})^n < a$.

ENNReal.coe_zpow theorem

(hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ≥0∞) ^ n

Full source

@[simp, norm_cast]
theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ≥0∞) ^ n := by
  rcases n with n | n
  · simp only [Int.ofNat_eq_coe, coe_pow, zpow_natCast]
  · have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
    simp only [zpow_negSucc, coe_inv this, coe_pow]

Power Preservation under Casting: $\overline{r^n} = (\overline{r})^n$ for $r \neq 0$ and $n \in \mathbb{Z}$

Informal description

For any nonzero nonnegative real number $r$ and any integer $n$, the extended nonnegative real number obtained by casting $r^n$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the $n$-th power of the cast of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\overline{r^n} = (\overline{r})^n$, where $\overline{\cdot}$ denotes the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.zpow_pos theorem

(ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n

Full source

theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n := by
  cases n
  · simpa using ENNReal.pow_pos ha.bot_lt _
  · simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, not_false, ENNReal.inv_pos, false_and,
      not_false_eq_true]

Positivity of Integer Powers in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, and for any integer $n$, the $n$-th power of $a$ is strictly positive, i.e., $0 < a^n$.

ENNReal.zpow_lt_top theorem

(ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : a ^ n < ∞

Full source

theorem zpow_lt_top (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : a ^ n < ∞ := by
  cases n
  · simpa using ENNReal.pow_lt_top h'a.lt_top
  · simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]

Nonzero Finite Extended Reals Have Finite Integer Powers: $a^n < \infty$ for $a \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$ and $n \in \mathbb{Z}$

Informal description

For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, and for any integer $n$, the power $a^n$ is strictly less than $\infty$.

ENNReal.exists_mem_Ico_zpow theorem

 {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) : ∃ n : ℤ, x ∈ Ico (y ^ n) (y ^ (n + 1))

Full source

theorem exists_mem_Ico_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) :
    ∃ n : ℤ, x ∈ Ico (y ^ n) (y ^ (n + 1)) := by
  lift x to ℝ≥0 using h'x
  lift y to ℝ≥0 using h'y
  have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
  obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) := by
    refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
  refine ⟨n, ?_, ?_⟩
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

Existence of Integer Power Interval for Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $x$ and $y$ such that $x \neq 0$, $x \neq \infty$, $1 < y$, and $y \neq \infty$, there exists an integer $n$ such that $x$ lies in the interval $[y^n, y^{n+1})$.

ENNReal.exists_mem_Ioc_zpow theorem

 {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) : ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1))

Full source

theorem exists_mem_Ioc_zpow {x y : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (hy : 1 < y) (h'y : y ≠ ⊤) :
    ∃ n : ℤ, x ∈ Ioc (y ^ n) (y ^ (n + 1)) := by
  lift x to ℝ≥0 using h'x
  lift y to ℝ≥0 using h'y
  have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
  obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) := by
    refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
  refine ⟨n, ?_, ?_⟩
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

Existence of Integer Power Interval for Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $x$ and $y$ such that $x \neq 0$, $x \neq \infty$, $1 < y$, and $y \neq \infty$, there exists an integer $n$ such that $x$ lies in the left-open right-closed interval $(y^n, y^{n+1}]$.

ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow theorem

 {y : ℝ≥0∞} (hy : 1 < y) (h'y : y ≠ ⊤) : Ioo (0 : ℝ≥0∞) (∞ : ℝ≥0∞) = ⋃ n : ℤ, Ico (y ^ n) (y ^ (n + 1))

Full source

theorem Ioo_zero_top_eq_iUnion_Ico_zpow {y : ℝ≥0∞} (hy : 1 < y) (h'y : y ≠ ⊤) :
    Ioo (0 : ℝ≥0∞) (∞ : ℝ≥0∞) = ⋃ n : ℤ, Ico (y ^ n) (y ^ (n + 1)) := by
  ext x
  simp only [mem_iUnion, mem_Ioo, mem_Ico]
  constructor
  · rintro ⟨hx, h'x⟩
    exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y
  · rintro ⟨n, hn, h'n⟩
    constructor
    · apply lt_of_lt_of_le _ hn
      exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _
    · apply lt_trans h'n _
      exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

Decomposition of $(0, \infty)$ in Extended Non-Negative Reals as Union of Power Intervals

Informal description

For any extended non-negative real number $y$ such that $1 < y < \infty$, the open interval $(0, \infty)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the union of the intervals $[y^n, y^{n+1})$ for all integers $n \in \mathbb{Z}$.

ENNReal.zpow_le_of_le theorem

{x : ℝ≥0∞} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : x ^ a ≤ x ^ b

Full source

@[gcongr]
theorem zpow_le_of_le {x : ℝ≥0∞} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : x ^ a ≤ x ^ b := by
  obtain a | a := a <;> obtain b | b := b
  · simp only [Int.ofNat_eq_coe, zpow_natCast]
    exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)
  · apply absurd h (not_le_of_gt _)
    exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.ofNat_nonneg _)
  · simp only [zpow_negSucc, Int.ofNat_eq_coe, zpow_natCast]
    refine (ENNReal.inv_le_one.2 ?_).trans ?_ <;> exact one_le_pow_of_one_le' hx _
  · simp only [zpow_negSucc, ENNReal.inv_le_inv]
    apply pow_right_mono₀ hx
    simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using h

Monotonicity of Integer Powers for $x \geq 1$ in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $x \geq 1$ and integers $a \leq b$, the inequality $x^a \leq x^b$ holds.

ENNReal.monotone_zpow theorem

{x : ℝ≥0∞} (hx : 1 ≤ x) : Monotone ((x ^ ·) : ℤ → ℝ≥0∞)

Full source

theorem monotone_zpow {x : ℝ≥0∞} (hx : 1 ≤ x) : Monotone ((x ^ ·) : ℤ → ℝ≥0∞) := fun _ _ h =>
  zpow_le_of_le hx h

Monotonicity of Integer Powers for $x \geq 1$ in Extended Non-Negative Reals

Informal description

For any extended non-negative real number $x \geq 1$, the function $n \mapsto x^n$ is monotone increasing in the integer exponent $n \in \mathbb{Z}$.

ENNReal.zpow_add theorem

{x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m n : ℤ) : x ^ (m + n) = x ^ m * x ^ n

Full source

protected theorem zpow_add {x : ℝ≥0∞} (hx : x ≠ 0) (h'x : x ≠ ∞) (m n : ℤ) :
    x ^ (m + n) = x ^ m * x ^ n := by
  lift x to ℝ≥0 using h'x
  replace hx : x ≠ 0 := by simpa only [Ne, coe_eq_zero] using hx
  simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]

Power Law for Extended Non-Negative Reals: $x^{m+n} = x^m \cdot x^n$

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$ and $x \neq \infty$, and for any integers $m, n \in \mathbb{Z}$, the following equality holds: $$x^{m + n} = x^m \cdot x^n.$$

ENNReal.zpow_neg theorem

{x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m : ℤ) : x ^ (-m) = (x ^ m)⁻¹

Full source

protected theorem zpow_neg {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m : ℤ) :
    x ^ (-m) = (x ^ m)⁻¹ :=
  ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add x_ne_zero x_ne_top])

Negative Power Law for Extended Non-Negative Reals: $x^{-m} = (x^m)^{-1}$

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$ and $x \neq \infty$, and for any integer $m \in \mathbb{Z}$, the following equality holds: $$x^{-m} = (x^m)^{-1}.$$

ENNReal.zpow_sub theorem

{x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) : x ^ (m - n) = (x ^ m) * (x ^ n)⁻¹

Full source

protected theorem zpow_sub {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) :
    x ^ (m - n) = (x ^ m) * (x ^ n)⁻¹ := by
  rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg x_ne_zero x_ne_top n]

Subtraction Power Law for Extended Non-Negative Reals: $x^{m-n} = x^m \cdot (x^n)^{-1}$

Informal description

For any extended non-negative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq 0$ and $x \neq \infty$, and for any integers $m, n \in \mathbb{Z}$, the following equality holds: $$x^{m - n} = x^m \cdot (x^n)^{-1}.$$

ENNReal.iSup_eq_zero theorem

: ⨆ i, f i = 0 ↔ ∀ i, f i = 0

Full source

@[simp] lemma iSup_eq_zero : ⨆ i, f i⨆ i, f i = 0 ↔ ∀ i, f i = 0 := iSup_eq_bot

Supremum of Extended Non-Negative Reals is Zero if and only if All Terms are Zero

Informal description

For a family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the supremum $\bigsqcup_i f_i$ is equal to $0$ if and only if $f_i = 0$ for every index $i$.

ENNReal.iSup_zero theorem

: ⨆ _ : ι, (0 : ℝ≥0∞) = 0

Full source

@[simp] lemma iSup_zero : ⨆ _ : ι, (0 : ℝ≥0∞) = 0 := by simp

Supremum of Zero Family in Extended Non-Negative Reals is Zero

Informal description

For any index set $\iota$, the supremum of the constant family $(0)_{i \in \iota}$ in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to $0$, i.e., $\bigsqcup_{i \in \iota} 0 = 0$.

ENNReal.iSup_natCast theorem

: ⨆ n : ℕ, (n : ℝ≥0∞) = ∞

Full source

lemma iSup_natCast : ⨆ n : ℕ, (n : ℝ≥0∞) = ∞ :=
  (iSup_eq_top _).2 fun _b hb => ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 hb)

Supremum of Natural Numbers in Extended Non-Negative Reals is Infinity

Informal description

The supremum of the sequence of extended non-negative real numbers obtained by casting natural numbers to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is infinity, i.e., $\bigsqcup_{n \in \mathbb{N}} n = \infty$.

ENNReal.iSup_lt_eq_self theorem

(a : ℝ≥0∞) : ⨆ b, ⨆ _ : b < a, b = a

Full source

@[simp] lemma iSup_lt_eq_self (a : ℝ≥0∞) : ⨆ b, ⨆ _ : b < a, b = a := by
  refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_
  refine le_of_forall_lt fun c hca ↦ ?_
  obtain ⟨d, hcd, hdb⟩ := exists_between hca
  exact hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

Supremum of Strictly Bounded Elements in Extended Non-Negative Reals Equals Itself

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the supremum of all $b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $b < a$ is equal to $a$ itself. In other words, $\sup \{b \mid b < a\} = a$.

ENNReal.isUnit_iff theorem

: IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Full source

lemma isUnit_iff : IsUnitIsUnit a ↔ a ≠ 0 ∧ a ≠ ∞ := by
  refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
    fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩
  obtain ⟨u, rfl⟩ := ha
  rintro hu
  have := congr($hu * u⁻¹)
  norm_cast at this
  simp [mul_inv_cancel] at this

Characterization of Units in Extended Non-Negative Reals: $a$ is a unit $\iff$ $a \neq 0$ and $a \neq \infty$

Informal description

An extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ is a unit if and only if $a \neq 0$ and $a \neq \infty$.

ENNReal.mulLeftOrderIso definition

(a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ ≃o ℝ≥0∞

Full source

/-- Left multiplication by a nonzero finite `a` as an order isomorphism. -/
@[simps! toEquiv apply symm_apply]
def mulLeftOrderIso (a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ℝ≥0∞ ≃o ℝ≥0∞ where
  toEquiv := ha.unit.mulLeft
  map_rel_iff' := by simp [ENNReal.mul_le_mul_left, ha.ne_zero, (isUnit_iff.1 ha).2]

Order isomorphism of left multiplication by a nonzero finite extended non-negative real

Informal description

For any nonzero finite extended non-negative real number $ a $ (i.e., $ a \neq 0 $ and $ a \neq \infty $), the function $ x \mapsto a \cdot x $ is an order isomorphism on $ \mathbb{R}_{\geq 0} \cup \{\infty\} $. This means it is a bijective function that preserves the order relation in both directions: for any $ x, y $, $ x \leq y $ if and only if $ a \cdot x \leq a \cdot y $.

ENNReal.mulRightOrderIso definition

(a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ ≃o ℝ≥0∞

Full source

/-- Right multiplication by a nonzero finite `a` as an order isomorphism. -/
@[simps! toEquiv apply symm_apply]
def mulRightOrderIso (a : ℝ≥0∞) (ha : IsUnit a) : ℝ≥0∞ℝ≥0∞ ≃o ℝ≥0∞ where
  toEquiv := ha.unit.mulRight
  map_rel_iff' := by simp [ENNReal.mul_le_mul_right, ha.ne_zero, (isUnit_iff.1 ha).2]

Right multiplication order isomorphism by a nonzero finite extended non-negative real

Informal description

For any nonzero finite extended non-negative real number $ a $, the right multiplication map $ x \mapsto x \cdot a $ is an order isomorphism on $ \mathbb{R}_{\geq 0} \cup \{\infty\} $.

ENNReal.mul_iSup theorem

(a : ℝ≥0∞) (f : ι → ℝ≥0∞) : a * ⨆ i, f i = ⨆ i, a * f i

Full source

lemma mul_iSup (a : ℝ≥0∞) (f : ι → ℝ≥0∞) : a * ⨆ i, f i = ⨆ i, a * f i := by
  by_cases hf : ∀ i, f i = 0
  · simp [hf]
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  obtain rfl | ha := eq_or_ne a ∞
  · obtain ⟨i, hi⟩ := not_forall.1 hf
    simpa [iSup_eq_zero.not.2 hf, eq_comm (a := ⊤)]
      using le_iSup_of_le (f := fun i => ⊤ * f i) i (top_mul hi).ge
  · exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

Multiplication Distributes over Supremum in Extended Non-Negative Reals: $a \cdot \bigsqcup_i f_i = \bigsqcup_i (a \cdot f_i)$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the product of $a$ with the supremum of the family equals the supremum of the products: \[ a \cdot \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (a \cdot f_i). \]

ENNReal.iSup_mul theorem

(f : ι → ℝ≥0∞) (a : ℝ≥0∞) : (⨆ i, f i) * a = ⨆ i, f i * a

Full source

lemma iSup_mul (f : ι → ℝ≥0∞) (a : ℝ≥0∞) : (⨆ i, f i) * a = ⨆ i, f i * a := by
  simp [mul_comm, mul_iSup]

Supremum Multiplicative Property in Extended Non-Negative Reals: $(\bigsqcup_i f_i) \cdot a = \bigsqcup_i (f_i \cdot a)$

Informal description

For any family of extended non-negative real numbers $(f_i)_{i \in \iota}$ and any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of the supremum of the family with $a$ equals the supremum of the products: \[ \left( \bigsqcup_{i} f_i \right) \cdot a = \bigsqcup_{i} (f_i \cdot a). \]

ENNReal.mul_sSup theorem

{a : ℝ≥0∞} : a * sSup s = ⨆ b ∈ s, a * b

Full source

lemma mul_sSup {a : ℝ≥0∞} : a * sSup s = ⨆ b ∈ s, a * b := by
  simp only [sSup_eq_iSup, mul_iSup]

Multiplication Distributes over Supremum in Extended Non-Negative Reals: $a \cdot \sup s = \sup_{b \in s} (a \cdot b)$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any set $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of $a$ with the supremum of $s$ equals the supremum of the products of $a$ with each element in $s$: \[ a \cdot \sup s = \sup_{b \in s} (a \cdot b). \]

ENNReal.sSup_mul theorem

{a : ℝ≥0∞} : sSup s * a = ⨆ b ∈ s, b * a

Full source

lemma sSup_mul {a : ℝ≥0∞} : sSup s * a = ⨆ b ∈ s, b * a := by
  simp only [sSup_eq_iSup, iSup_mul]

Supremum Multiplicative Property in Extended Non-Negative Reals: $\sup s \cdot a = \sup_{b \in s} (b \cdot a)$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any set $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product of the supremum of $s$ with $a$ equals the supremum of the products of each element in $s$ with $a$: \[ \sup s \cdot a = \sup_{b \in s} (b \cdot a). \]

ENNReal.iSup_div theorem

(f : ι → ℝ≥0∞) (a : ℝ≥0∞) : iSup f / a = ⨆ i, f i / a

Full source

lemma iSup_div (f : ι → ℝ≥0∞) (a : ℝ≥0∞) : iSup f / a = ⨆ i, f i / a := iSup_mul ..

Supremum Division Property in Extended Non-Negative Reals: $(\bigsqcup_i f_i) / a = \bigsqcup_i (f_i / a)$

Informal description

For any family of extended non-negative real numbers $(f_i)_{i \in \iota}$ and any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the supremum of the family divided by $a$ equals the supremum of the divisions: \[ \left( \bigsqcup_{i} f_i \right) / a = \bigsqcup_{i} (f_i / a). \]

ENNReal.sSup_div theorem

(s : Set ℝ≥0∞) (a : ℝ≥0∞) : sSup s / a = ⨆ b ∈ s, b / a

Full source

lemma sSup_div (s : Set ℝ≥0∞) (a : ℝ≥0∞) : sSup s / a = ⨆ b ∈ s, b / a := sSup_mul ..

Supremum Division Property in Extended Non-Negative Reals: $\sup s / a = \sup_{b \in s} (b / a)$

Informal description

For any set $s$ of extended non-negative real numbers and any extended non-negative real number $a$, the supremum of $s$ divided by $a$ equals the supremum of the division of each element in $s$ by $a$: \[ \sup s / a = \sup_{b \in s} (b / a). \]

ENNReal.mul_iInf' theorem

 (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) : a * ⨅ i, f i = ⨅ i, a * f i

Full source

/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.mul_iInf_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.mul_iInf` for the special case assuming `Nonempty ι`. -/
lemma mul_iInf' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
    a * ⨅ i, f i = ⨅ i, a * f i := by
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp [h₀ rfl]
  obtain rfl | ha := eq_or_ne a ∞
  · obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)
    · rw [(iInf_eq_bot _).2, (iInf_eq_bot _).2, bot_eq_zero, mul_zero] <;>
        exact fun _ _↦ ⟨i, by simpa [hi]⟩
    · rw [top_mul (mt (hinfty rfl) hf), eq_comm, iInf_eq_top]
      exact fun i ↦ top_mul fun hi ↦ hf ⟨i, hi⟩
  · exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _

Distributivity of multiplication over infimum in extended non-negative reals under general conditions

Informal description

Let $a$ be an extended non-negative real number and $\{f_i\}_{i \in \iota}$ be a family of extended non-negative real numbers. Suppose that: 1. If $a = \infty$, then either $\bigsqcap_i f_i \neq 0$ or there exists some $i$ with $f_i = 0$. 2. If $a = 0$, then the index set $\iota$ is nonempty. Then the following equality holds: $$ a \cdot \left(\bigsqcap_{i \in \iota} f_i\right) = \bigsqcap_{i \in \iota} (a \cdot f_i). $$

ENNReal.iInf_mul' theorem

 (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) : (⨅ i, f i) * a = ⨅ i, f i * a

Full source

/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.iInf_mul_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_mul` for the special case assuming `Nonempty ι`. -/
lemma iInf_mul' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
    (⨅ i, f i) * a = ⨅ i, f i * a := by simpa only [mul_comm a] using mul_iInf' hinfty h₀

Distributivity of infimum multiplication in extended non-negative reals under general conditions

Informal description

Let $a$ be an extended non-negative real number and $\{f_i\}_{i \in \iota}$ be a family of extended non-negative real numbers. Suppose that: 1. If $a = \infty$, then either $\bigsqcap_i f_i \neq 0$ or there exists some $i$ with $f_i = 0$. 2. If $a = 0$, then the index set $\iota$ is nonempty. Then the following equality holds: $$ \left(\bigsqcap_{i \in \iota} f_i\right) \cdot a = \bigsqcap_{i \in \iota} (f_i \cdot a). $$

ENNReal.mul_iInf_of_ne theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * ⨅ i, f i = ⨅ i, a * f i

Full source

/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.mul_iInf'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`, and `ENNReal`. -/
lemma mul_iInf_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * ⨅ i, f i = ⨅ i, a * f i :=
  mul_iInf' (by simp [ha]) (by simp [ha₀])

Distributivity of multiplication over infimum in extended non-negative reals for $a \neq 0, \infty$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, and for any family of extended non-negative real numbers $\{f_i\}_{i \in \iota}$, the following equality holds: $$ a \cdot \left(\bigsqcap_{i \in \iota} f_i\right) = \bigsqcap_{i \in \iota} (a \cdot f_i). $$

ENNReal.iInf_mul_of_ne theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) * a = ⨅ i, f i * a

Full source

/-- If `a ≠ 0` and `a ≠ ∞`, then right multiplication by `a` maps infimum to infimum.

See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul` for another special case that
assumes `Nonempty ι` but does not require `a ≠ 0`. -/
lemma iInf_mul_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) * a = ⨅ i, f i * a :=
  iInf_mul' (by simp [ha]) (by simp [ha₀])

Right multiplication preserves infimum in extended non-negative reals for $a \neq 0, \infty$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, and for any family of extended non-negative real numbers $\{f_i\}_{i \in \iota}$, the following equality holds: $$ \left(\bigsqcap_{i \in \iota} f_i\right) \cdot a = \bigsqcap_{i \in \iota} (f_i \cdot a). $$

ENNReal.mul_iInf theorem

[Nonempty ι] (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) : a * ⨅ i, f i = ⨅ i, a * f i

Full source

/-- See `ENNReal.mul_iInf'` for the general case, and `ENNReal.mul_iInf_of_ne` for another special
case that assumes `a ≠ 0` but does not require `Nonempty ι`. -/
lemma mul_iInf [Nonempty ι] (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) :
    a * ⨅ i, f i = ⨅ i, a * f i := mul_iInf' hinfty fun _ ↦ ‹Nonempty ι›

Distributivity of multiplication over infimum in extended non-negative reals for nonempty index sets

Informal description

Let $\{f_i\}_{i \in \iota}$ be a nonempty family of extended non-negative real numbers and let $a$ be an extended non-negative real number. If $a = \infty$ implies that either $\inf_i f_i \neq 0$ or there exists some $i$ with $f_i = 0$, then the following equality holds: $$ a \cdot \left(\inf_{i \in \iota} f_i\right) = \inf_{i \in \iota} (a \cdot f_i). $$

ENNReal.iInf_mul theorem

[Nonempty ι] (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) : (⨅ i, f i) * a = ⨅ i, f i * a

Full source

/-- See `ENNReal.iInf_mul'` for the general case, and `ENNReal.iInf_mul_of_ne` for another special
case that assumes `a ≠ 0` but does not require `Nonempty ι`. -/
lemma iInf_mul [Nonempty ι] (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) :
    (⨅ i, f i) * a = ⨅ i, f i * a := iInf_mul' hinfty fun _ ↦ ‹Nonempty ι›

Distributivity of infimum multiplication in extended non-negative reals for nonempty index sets

Informal description

Let $\{f_i\}_{i \in \iota}$ be a nonempty family of extended non-negative real numbers and let $a$ be an extended non-negative real number. If $a = \infty$ implies that either $\inf_i f_i \neq 0$ or there exists some $i$ with $f_i = 0$, then the following equality holds: $$ \left(\inf_{i \in \iota} f_i\right) \cdot a = \inf_{i \in \iota} (f_i \cdot a). $$

ENNReal.iInf_div' theorem

 (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = ∞ → Nonempty ι) : (⨅ i, f i) / a = ⨅ i, f i / a

Full source

/-- Very general version for distributivity of division over an infimum.

See `ENNReal.iInf_div_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_div` for the special case assuming `Nonempty ι`. -/
lemma iInf_div' (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = ∞ → Nonempty ι) :
    (⨅ i, f i) / a = ⨅ i, f i / a := iInf_mul' (by simpa) (by simpa)

Distributivity of Division over Infimum in Extended Non-Negative Reals under General Conditions

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of extended non-negative real numbers and let $a$ be an extended non-negative real number. Suppose that: 1. If $a = 0$, then either $\bigsqcap_i f_i \neq 0$ or there exists some $i$ with $f_i = 0$. 2. If $a = \infty$, then the index set $\iota$ is nonempty. Then the following equality holds: $$ \frac{\bigsqcap_{i \in \iota} f_i}{a} = \bigsqcap_{i \in \iota} \left(\frac{f_i}{a}\right). $$

ENNReal.iInf_div_of_ne theorem

(ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) / a = ⨅ i, f i / a

Full source

/-- If `a ≠ 0` and `a ≠ ∞`, then division by `a` maps infimum to infimum.

See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div` for another special case that
assumes `Nonempty ι` but does not require `a ≠ ∞`. -/
lemma iInf_div_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) / a = ⨅ i, f i / a :=
  iInf_div' (by simp [ha₀]) (by simp [ha])

Distributivity of Division over Infimum in Extended Non-Negative Reals for Nonzero Finite Values

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of extended non-negative real numbers and let $a$ be an extended non-negative real number such that $a \neq 0$ and $a \neq \infty$. Then the following equality holds: $$ \frac{\bigsqcap_{i \in \iota} f_i}{a} = \bigsqcap_{i \in \iota} \left(\frac{f_i}{a}\right). $$

ENNReal.iInf_div theorem

[Nonempty ι] (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) : (⨅ i, f i) / a = ⨅ i, f i / a

Full source

/-- See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div_of_ne` for another special
case that assumes `a ≠ ∞` but does not require `Nonempty ι`. -/
lemma iInf_div [Nonempty ι] (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) :
    (⨅ i, f i) / a = ⨅ i, f i / a := iInf_div' hinfty fun _ ↦ ‹Nonempty ι›

Distributivity of Division over Infimum in Extended Non-Negative Reals for Nonempty Families

Informal description

Let $\{f_i\}_{i \in \iota}$ be a nonempty family of extended non-negative real numbers and let $a$ be an extended non-negative real number. Suppose that if $a = 0$ and $\bigsqcap_i f_i = 0$, then there exists some index $i$ such that $f_i = 0$. Then the following equality holds: $$ \frac{\bigsqcap_{i \in \iota} f_i}{a} = \bigsqcap_{i \in \iota} \left(\frac{f_i}{a}\right). $$

ENNReal.inv_iInf theorem

(f : ι → ℝ≥0∞) : (⨅ i, f i)⁻¹ = ⨆ i, (f i)⁻¹

Full source

lemma inv_iInf (f : ι → ℝ≥0∞) : (⨅ i, f i)⁻¹ = ⨆ i, (f i)⁻¹ := OrderIso.invENNReal.map_iInf _

Inverse of Infimum Equals Supremum of Inverses in Extended Non-Negative Reals

Informal description

For any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the multiplicative inverse of their infimum equals the supremum of their multiplicative inverses. That is, \[ \left(\bigwedge_{i} f_i\right)^{-1} = \bigvee_{i} f_i^{-1}. \]

ENNReal.inv_iSup theorem

(f : ι → ℝ≥0∞) : (⨆ i, f i)⁻¹ = ⨅ i, (f i)⁻¹

Full source

lemma inv_iSup (f : ι → ℝ≥0∞) : (⨆ i, f i)⁻¹ = ⨅ i, (f i)⁻¹ := OrderIso.invENNReal.map_iSup _

Inverse of Supremum Equals Infimum of Inverses in Extended Non-Negative Reals

Informal description

For any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the multiplicative inverse of their supremum equals the infimum of their multiplicative inverses, i.e., $$ \left(\bigsqcup_{i} f_i\right)^{-1} = \bigsqcap_{i} f_i^{-1}. $$

ENNReal.inv_sInf theorem

(s : Set ℝ≥0∞) : (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Full source

lemma inv_sInf (s : Set ℝ≥0∞) : (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹ := by simp [sInf_eq_iInf, inv_iInf]

Inverse of Infimum Equals Supremum of Inverses in Extended Non-Negative Reals

Informal description

For any set $s$ of extended non-negative real numbers, the multiplicative inverse of the infimum of $s$ equals the supremum of the multiplicative inverses of the elements in $s$. That is, \[ (\inf s)^{-1} = \sup_{a \in s} a^{-1}. \]

ENNReal.inv_sSup theorem

(s : Set ℝ≥0∞) : (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

Full source

lemma inv_sSup (s : Set ℝ≥0∞) : (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹ := by simp [sSup_eq_iSup, inv_iSup]

Inverse of Supremum Equals Infimum of Inverses for Extended Non-Negative Reals

Informal description

For any set $s$ of extended non-negative real numbers, the multiplicative inverse of its supremum equals the infimum of the multiplicative inverses of its elements, i.e., $$ \left(\sup s\right)^{-1} = \inf_{a \in s} a^{-1}. $$

ENNReal.le_iInf_mul theorem

{ι : Type*} (u v : ι → ℝ≥0∞) : (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i

Full source

lemma le_iInf_mul {ι : Type*} (u v : ι → ℝ≥0∞) :
    (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i :=
  le_iInf fun i ↦ mul_le_mul' (iInf_le u i) (iInf_le v i)

Infimum-Multiplication Inequality in Extended Non-Negative Reals

Informal description

For any indexed families of extended non-negative real numbers $(u_i)_{i \in \iota}$ and $(v_i)_{i \in \iota}$, the product of their infima is less than or equal to the infimum of their pointwise products, i.e., $$ \left(\bigwedge_i u_i\right) \cdot \left(\bigwedge_i v_i\right) \leq \bigwedge_i (u_i \cdot v_i). $$

ENNReal.iSup_mul_le theorem

{ι : Type*} {u v : ι → ℝ≥0∞} : ⨆ i, u i * v i ≤ (⨆ i, u i) * ⨆ i, v i

Full source

lemma iSup_mul_le {ι : Type*} {u v : ι → ℝ≥0∞} :
    ⨆ i, u i * v i ≤ (⨆ i, u i) * ⨆ i, v i :=
  iSup_le fun i ↦ mul_le_mul' (le_iSup u i) (le_iSup v i)

Supremum-Multiplication Inequality in Extended Non-Negative Reals

Informal description

For any indexed families of extended non-negative real numbers $(u_i)_{i \in \iota}$ and $(v_i)_{i \in \iota}$, the supremum of their pointwise products is less than or equal to the product of their suprema, i.e., $$ \bigvee_i (u_i \cdot v_i) \leq \left(\bigvee_i u_i\right) \cdot \left(\bigvee_i v_i\right). $$

ENNReal.add_iSup theorem

[Nonempty ι] (f : ι → ℝ≥0∞) : a + ⨆ i, f i = ⨆ i, a + f i

Full source

lemma add_iSup [Nonempty ι] (f : ι → ℝ≥0∞) : a + ⨆ i, f i = ⨆ i, a + f i := by
  obtain rfl | ha := eq_or_ne a ∞
  · simp
  refine le_antisymm ?_ <| iSup_le fun i ↦ add_le_add_left (le_iSup ..) _
  refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_
  exact iSup_le fun i ↦ ENNReal.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Additivity of Supremum in Extended Non-Negative Reals

Informal description

For any nonempty index set $\iota$ and any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of a fixed extended non-negative real number $a$ and the supremum of the family equals the supremum of the family obtained by adding $a$ to each $f_i$, i.e., $$ a + \bigvee_{i \in \iota} f_i = \bigvee_{i \in \iota} (a + f_i). $$

ENNReal.iSup_add theorem

[Nonempty ι] (f : ι → ℝ≥0∞) : (⨆ i, f i) + a = ⨆ i, f i + a

Full source

lemma iSup_add [Nonempty ι] (f : ι → ℝ≥0∞) : (⨆ i, f i) + a = ⨆ i, f i + a := by
  simp [add_comm, add_iSup]

Right Additivity of Supremum in Extended Non-Negative Reals

Informal description

For any nonempty index set $\iota$ and any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of the supremum of the family and a fixed extended non-negative real number $a$ equals the supremum of the family obtained by adding $a$ to each $f_i$, i.e., $$ \left(\bigvee_{i \in \iota} f_i\right) + a = \bigvee_{i \in \iota} (f_i + a). $$

ENNReal.add_biSup' theorem

{p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) : a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i

Full source

lemma add_biSup' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) :
    a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i := by
  haveI : Nonempty {i // p i} := nonempty_subtype.2 h
  simp only [iSup_subtype', add_iSup]

Additivity of Supremum over Predicate in Extended Non-Negative Reals

Informal description

For any predicate $p$ on an index set $\iota$ such that there exists an $i$ with $p(i)$, and for any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of a fixed extended non-negative real number $a$ and the supremum of the subfamily $(f_i)_{i \in \iota, p(i)}$ equals the supremum of the subfamily obtained by adding $a$ to each $f_i$ in the subfamily, i.e., $$ a + \bigvee_{\substack{i \in \iota \\ p(i)}} f_i = \bigvee_{\substack{i \in \iota \\ p(i)}} (a + f_i). $$

ENNReal.biSup_add' theorem

 {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) : (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a

Full source

lemma biSup_add' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) :
    (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a := by simp only [add_comm, add_biSup' h]

Right Additivity of Bounded Supremum in Extended Non-Negative Reals

Informal description

For any predicate $p$ on an index set $\iota$ such that there exists an $i$ with $p(i)$, and for any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of the supremum of the subfamily $(f_i)_{i \in \iota, p(i)}$ and a fixed extended non-negative real number $a$ equals the supremum of the subfamily obtained by adding $a$ to each $f_i$ in the subfamily, i.e., $$ \left(\bigvee_{\substack{i \in \iota \\ p(i)}} f_i\right) + a = \bigvee_{\substack{i \in \iota \\ p(i)}} (f_i + a). $$

ENNReal.add_biSup theorem

{ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℝ≥0∞) : a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

Full source

lemma add_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℝ≥0∞) :
    a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i := add_biSup' hs _

Additivity of Supremum over Nonempty Set in Extended Non-Negative Reals

Informal description

For any nonempty set $s$ of indices and any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of a fixed extended non-negative real number $a$ and the supremum of $(f_i)_{i \in s}$ equals the supremum of the family $(a + f_i)_{i \in s}$. In other words, $$ a + \bigvee_{i \in s} f_i = \bigvee_{i \in s} (a + f_i). $$

ENNReal.biSup_add theorem

{ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℝ≥0∞) : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

Full source

lemma biSup_add {ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℝ≥0∞) :
    (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a := biSup_add' hs _

Right Additivity of Supremum over Nonempty Set in Extended Non-Negative Reals

Informal description

For any nonempty set $s$ of indices and any family of extended non-negative real numbers $(f_i)_{i \in \iota}$, the sum of the supremum of $(f_i)_{i \in s}$ and a fixed extended non-negative real number $a$ equals the supremum of the family $(f_i + a)_{i \in s}$. In other words, $$ \left(\bigvee_{i \in s} f_i\right) + a = \bigvee_{i \in s} (f_i + a). $$

ENNReal.add_sSup theorem

(hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b

Full source

lemma add_sSup (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b := by
  rw [sSup_eq_iSup, add_biSup hs]

Additivity of Supremum over Nonempty Set in Extended Non-Negative Reals

Informal description

For any nonempty set $s$ of extended non-negative real numbers and any extended non-negative real number $a$, the sum of $a$ and the supremum of $s$ equals the supremum of the set $\{a + b \mid b \in s\}$. In other words, $$ a + \sup s = \sup_{b \in s} (a + b). $$

ENNReal.sSup_add theorem

(hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

Full source

lemma sSup_add (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a := by
  rw [sSup_eq_iSup, biSup_add hs]

Right Additivity of Supremum over Nonempty Set in Extended Non-Negative Reals

Informal description

For any nonempty set $s$ of extended non-negative real numbers and any extended non-negative real number $a$, the sum of the supremum of $s$ and $a$ equals the supremum of the set $\{b + a \mid b \in s\}$. In other words, $$ \sup s + a = \sup_{b \in s} (b + a). $$

ENNReal.iSup_add_iSup_le theorem

[Nonempty ι] [Nonempty κ] {g : κ → ℝ≥0∞} (h : ∀ i j, f i + g j ≤ a) : iSup f + iSup g ≤ a

Full source

lemma iSup_add_iSup_le [Nonempty ι] [Nonempty κ] {g : κ → ℝ≥0∞} (h : ∀ i j, f i + g j ≤ a) :
    iSup f + iSup g ≤ a := by simp_rw [iSup_add, add_iSup]; exact iSup₂_le h

Supremum Sum Inequality in Extended Non-Negative Reals

Informal description

For any nonempty index sets $\iota$ and $\kappa$, and any families of extended non-negative real numbers $(f_i)_{i \in \iota}$ and $(g_j)_{j \in \kappa}$, if for all $i \in \iota$ and $j \in \kappa$ the sum $f_i + g_j$ is bounded above by $a$, then the sum of the suprema satisfies $\bigvee_{i \in \iota} f_i + \bigvee_{j \in \kappa} g_j \leq a$.

ENNReal.biSup_add_biSup_le' theorem

 {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j) {g : κ → ℝ≥0∞}
  (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) : (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a

Full source

lemma biSup_add_biSup_le' {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j)
    {g : κ → ℝ≥0∞} (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) :
    (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a := by
  simp_rw [biSup_add' hp, add_biSup' hq]
  exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Bounded Supremum Sum Inequality in Extended Non-Negative Reals

Informal description

Let $\iota$ and $\kappa$ be index sets with predicates $p : \iota \to \mathrm{Prop}$ and $q : \kappa \to \mathrm{Prop}$ such that there exist $i \in \iota$ with $p(i)$ and $j \in \kappa$ with $q(j)$. For any families of extended non-negative real numbers $(f_i)_{i \in \iota}$ and $(g_j)_{j \in \kappa}$, if for all $i$ with $p(i)$ and all $j$ with $q(j)$ we have $f_i + g_j \leq a$, then: $$ \left(\bigvee_{\substack{i \in \iota \\ p(i)}} f_i\right) + \left(\bigvee_{\substack{j \in \kappa \\ q(j)}} g_j\right) \leq a. $$

ENNReal.biSup_add_biSup_le theorem

 {ι κ : Type*} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty) {f : ι → ℝ≥0∞} {g : κ → ℝ≥0∞} {a : ℝ≥0∞}
  (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) : (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a

Full source

lemma biSup_add_biSup_le {ι κ : Type*} {s : Set ι} {t : Set κ} (hs : s.Nonempty) (ht : t.Nonempty)
    {f : ι → ℝ≥0∞} {g : κ → ℝ≥0∞} {a : ℝ≥0∞} (h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a) :
    (⨆ i ∈ s, f i) + ⨆ j ∈ t, g j ≤ a := biSup_add_biSup_le' hs ht h

Bounded Supremum Sum Inequality for Nonempty Sets in Extended Non-Negative Reals

Informal description

Let $\iota$ and $\kappa$ be types, and let $s \subseteq \iota$ and $t \subseteq \kappa$ be nonempty sets. For any families of extended non-negative real numbers $(f_i)_{i \in \iota}$ and $(g_j)_{j \in \kappa}$, if for all $i \in s$ and $j \in t$ the sum $f_i + g_j$ is bounded above by $a$, then the sum of the suprema satisfies: \[ \left(\bigvee_{i \in s} f_i\right) + \left(\bigvee_{j \in t} g_j\right) \leq a. \]

ENNReal.iSup_add_iSup theorem

(h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i

Full source

lemma iSup_add_iSup (h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i := by
  cases isEmpty_or_nonempty ι
  · simp only [iSup_of_empty, bot_eq_zero, zero_add]
  · refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
    refine iSup_add_iSup_le fun i j => ?_
    rcases h i j with ⟨k, hk⟩
    exact le_iSup_of_le k hk

Supremum Sum Equality in Extended Non-Negative Reals

Informal description

For any indexed families of extended non-negative real numbers $(f_i)_{i \in \iota}$ and $(g_j)_{j \in \kappa}$, if for every $i$ and $j$ there exists some $k$ such that $f_i + g_j \leq f_k + g_k$, then the sum of the suprema equals the supremum of the sums, i.e., \[ \bigvee_{i} f_i + \bigvee_{j} g_j = \bigvee_{k} (f_k + g_k). \]

ENNReal.iSup_add_iSup_of_monotone theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℝ≥0∞} (hf : Monotone f) (hg : Monotone g) :
  iSup f + iSup g = ⨆ a, f a + g a

Full source

lemma iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℝ≥0∞}
    (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
  iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules

Supremum Sum Equality for Monotone Functions in Extended Non-Negative Reals

Informal description

Let $\iota$ be a preorder that is directed with respect to the relation $\leq$, and let $f, g : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ be monotone functions. Then the sum of their suprema equals the supremum of their pointwise sums, i.e., \[ \sup_{i} f(i) + \sup_{j} g(j) = \sup_{k} (f(k) + g(k)). \]

ENNReal.le_iInf_mul_iInf theorem

 {g : κ → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞) (ha : ∀ i j, a ≤ f i * g j) : a ≤ (⨅ i, f i) * ⨅ j, g j

Full source

lemma le_iInf_mul_iInf {g : κ → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞)
    (ha : ∀ i j, a ≤ f i * g j) : a ≤ (⨅ i, f i) * ⨅ j, g j := by
  rw [← iInf_ne_top_subtype]
  have := nonempty_subtype.2 hf
  have := hg.nonempty
  replace hg : ⨅ j, g j⨅ j, g j ≠ ∞ := by simpa using hg
  rw [iInf_mul fun h ↦ (hg h).elim, le_iInf_iff]
  rintro ⟨i, hi⟩
  simpa [mul_iInf fun h ↦ (hi h).elim] using ha i

Lower Bound on Product of Infima in Extended Non-Negative Reals

Informal description

Let $\{f_i\}_{i \in \iota}$ and $\{g_j\}_{j \in \kappa}$ be families of extended non-negative real numbers such that there exists some $i$ with $f_i \neq \infty$ and some $j$ with $g_j \neq \infty$. If for all $i$ and $j$ we have $a \leq f_i \cdot g_j$, then $a \leq \left(\inf_i f_i\right) \cdot \left(\inf_j g_j\right)$.

ENNReal.iInf_mul_iInf theorem

 {f g : ι → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞) (h : ∀ i j, ∃ k, f k * g k ≤ f i * g j) :
  (⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i

Full source

lemma iInf_mul_iInf {f g : ι → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞)
    (h : ∀ i j, ∃ k, f k * g k ≤ f i * g j) : (⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i := by
  refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
    (le_iInf_mul_iInf hf hg fun i j ↦ ?_)
  obtain ⟨k, hk⟩ := h i j
  exact iInf_le_of_le k hk

Product of Infima Equals Infimum of Products in Extended Non-Negative Reals

Informal description

Let $\{f_i\}_{i \in \iota}$ and $\{g_i\}_{i \in \iota}$ be families of extended non-negative real numbers such that there exists some $i$ with $f_i \neq \infty$ and some $j$ with $g_j \neq \infty$. If for all $i$ and $j$ there exists $k$ such that $f_k \cdot g_k \leq f_i \cdot g_j$, then the product of the infima equals the infimum of the pointwise products: \[ \left(\inf_i f_i\right) \cdot \left(\inf_i g_i\right) = \inf_i (f_i \cdot g_i). \]

ENNReal.smul_iSup theorem

 {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (f : ι → ℝ≥0∞) (c : R) : c • ⨆ i, f i = ⨆ i, c • f i

Full source

lemma smul_iSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (f : ι → ℝ≥0∞) (c : R) :
    c • ⨆ i, f i = ⨆ i, c • f i := by
  simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

Scalar Multiplication Distributes over Supremum in Extended Non-Negative Reals: $c \cdot \bigsqcup_i f_i = \bigsqcup_i (c \cdot f_i)$

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on $\mathbb{R}_{\geq 0} \cup \{\infty\}$ that is compatible with the multiplication on $\mathbb{R}_{\geq 0} \cup \{\infty\}$ (i.e., $[IsScalarTower\, R\, \mathbb{R}_{\geq 0} \cup \{\infty\}\, \mathbb{R}_{\geq 0} \cup \{\infty\}]$ holds). For any family $(f_i)_{i \in \iota}$ of extended non-negative real numbers and any scalar $c \in R$, the scalar multiplication distributes over the supremum: \[ c \cdot \left( \bigsqcup_{i} f_i \right) = \bigsqcup_{i} (c \cdot f_i). \]

ENNReal.smul_sSup theorem

 {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (s : Set ℝ≥0∞) (c : R) : c • sSup s = ⨆ a ∈ s, c • a

Full source

lemma smul_sSup {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (s : Set ℝ≥0∞) (c : R) :
    c • sSup s = ⨆ a ∈ s, c • a := by
  simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]

Scalar Multiplication Distributes over Supremum in Extended Non-Negative Reals: $c \cdot \sup s = \sup_{a \in s} (c \cdot a)$

Informal description

Let $R$ be a type with a scalar multiplication operation on $\mathbb{R}_{\geq 0} \cup \{\infty\}$ that forms a scalar tower with $\mathbb{R}_{\geq 0} \cup \{\infty\}$. For any set $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any scalar $c \in R$, the scalar multiplication of $c$ with the supremum of $s$ equals the supremum of the scalar multiples of elements in $s$: \[ c \cdot \sup s = \sup_{a \in s} (c \cdot a). \]

ENNReal.sub_iSup theorem

[Nonempty ι] (ha : a ≠ ∞) : a - ⨆ i, f i = ⨅ i, a - f i

Full source

lemma sub_iSup [Nonempty ι] (ha : a ≠ ∞) : a - ⨆ i, f i = ⨅ i, a - f i := by
  obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)
  · rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, (iInf_eq_bot _).2, bot_eq_zero]
    exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
  simp_rw [not_exists, not_lt] at h
  refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_
  rw [← sub_sub_cancel ha (h _)]
  exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

Subtraction of Supremum Equals Infimum of Differences in Extended Non-Negative Reals

Informal description

For a nonempty index set $\iota$ and an extended non-negative real number $a \neq \infty$, the difference between $a$ and the supremum of a family of extended non-negative real numbers $(f_i)_{i \in \iota}$ is equal to the infimum of the family $(a - f_i)_{i \in \iota}$. That is, $$ a - \sup_{i \in \iota} f_i = \inf_{i \in \iota} (a - f_i). $$

ENNReal.exists_lt_add_of_lt_add theorem

{x y z : ℝ≥0∞} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) : ∃ y' < y, ∃ z' < z, x < y' + z'

Full source

lemma exists_lt_add_of_lt_add {x y z : ℝ≥0∞} (h : x < y + z) (hy : y ≠ 0) (hz : z ≠ 0) :
    ∃ y' < y, ∃ z' < z, x < y' + z' := by
  contrapose! h
  simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

Existence of Strictly Smaller Addends in Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $x, y, z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x < y + z$ and $y, z \neq 0$, there exist $y' < y$ and $z' < z$ such that $x < y' + z'$.

ENNReal.ofReal_inv_of_pos theorem

{x : ℝ} (hx : 0 < x) : ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹

Full source

theorem ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) : ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹ := by
  rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]

Inverse Preservation of `ofReal` for Positive Reals: $\text{ofReal}(x^{-1}) = (\text{ofReal}(x))^{-1}$ when $x > 0$

Informal description

For any positive real number $x > 0$, the extended nonnegative real number obtained by applying the `ofReal` function to $x^{-1}$ equals the inverse of the extended nonnegative real number obtained by applying `ofReal` to $x$, i.e., $\text{ofReal}(x^{-1}) = (\text{ofReal}(x))^{-1}$.

ENNReal.ofReal_div_of_pos theorem

{x y : ℝ} (hy : 0 < y) : ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Full source

theorem ofReal_div_of_pos {x y : ℝ} (hy : 0 < y) :
    ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y := by
  rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]

Division Preservation of `ofReal` for Positive Denominator: $\text{ofReal}(x/y) = \text{ofReal}(x) / \text{ofReal}(y)$ when $y > 0$

Informal description

For any real numbers $x$ and $y$ with $y > 0$, the extended nonnegative real number obtained by applying the `ofReal` function to the quotient $x / y$ is equal to the quotient of the `ofReal` images of $x$ and $y$, i.e., \[ \text{ofReal}(x / y) = \text{ofReal}(x) / \text{ofReal}(y). \]

ENNReal.toNNReal_inv theorem

(a : ℝ≥0∞) : a⁻¹.toNNReal = a.toNNReal⁻¹

Full source

@[simp] theorem toNNReal_inv (a : ℝ≥0∞) : a⁻¹.toNNReal = a.toNNReal⁻¹ := by
  induction' a with a; · simp
  rcases eq_or_ne a 0 with (rfl | ha); · simp
  rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

Inverse Preservation of Non-Negative Real Part: $\text{toNNReal}(a^{-1}) = (\text{toNNReal}(a))^{-1}$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the non-negative real part of its multiplicative inverse $a^{-1}$ equals the multiplicative inverse of the non-negative real part of $a$, i.e., $\text{toNNReal}(a^{-1}) = (\text{toNNReal}(a))^{-1}$.

ENNReal.toNNReal_div theorem

(a b : ℝ≥0∞) : (a / b).toNNReal = a.toNNReal / b.toNNReal

Full source

@[simp] theorem toNNReal_div (a b : ℝ≥0∞) : (a / b).toNNReal = a.toNNReal / b.toNNReal := by
  rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]

Quotient Preservation of Non-Negative Real Part for Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a$ and $b$, the non-negative real part of their quotient equals the quotient of their non-negative real parts, i.e., \[ \text{toNNReal}(a / b) = \text{toNNReal}(a) / \text{toNNReal}(b). \]

ENNReal.toReal_inv theorem

(a : ℝ≥0∞) : a⁻¹.toReal = a.toReal⁻¹

Full source

@[simp] theorem toReal_inv (a : ℝ≥0∞) : a⁻¹.toReal = a.toReal⁻¹ := by
  simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]

Inverse Preservation of Real Part: $\text{toReal}(a^{-1}) = (\text{toReal}(a))^{-1}$

Informal description

For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part of its multiplicative inverse $a^{-1}$ equals the multiplicative inverse of the real part of $a$, i.e., $\text{toReal}(a^{-1}) = (\text{toReal}(a))^{-1}$.

ENNReal.toReal_div theorem

(a b : ℝ≥0∞) : (a / b).toReal = a.toReal / b.toReal

Full source

@[simp] theorem toReal_div (a b : ℝ≥0∞) : (a / b).toReal = a.toReal / b.toReal := by
  rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]

Quotient Preservation of Real Conversion for Extended Non-Negative Reals

Informal description

For any extended non-negative real numbers $a$ and $b$, the real-valued conversion of their quotient equals the quotient of their real-valued conversions, i.e., \[ \text{toReal}(a / b) = \text{toReal}(a) / \text{toReal}(b). \]

Main results