ENNReal.inv_pow
theorem ENNReal.inv_pow : ∀ {a : ENNReal} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n
This theorem states that for every extended nonnegative real number `a` and for every natural number `n`, the reciprocal (or inverse) of `a` raised to the `n`th power is equal to `n` powers of the reciprocal of `a`. In other words, taking the reciprocal and raising to the `n`th power commute with each other. This can be expressed in mathematical notation by saying that for all $a \in [0, \infty)$ and $n \in \mathbb{N}$, $(a^n)^{-1} = (a^{-1})^n$.
More concisely: For all $a \in (0, \infty)$ and $n \in \mathbb{N}$, $(a^n)^{-1} = (a^{-1})^n$ (i.e., the reciprocal of a number raised to the power n is equal to n-th power of its reciprocal).
|
ENNReal.div_mul_cancel
theorem ENNReal.div_mul_cancel : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → b / a * a = b
This theorem states that for any two extended nonnegative real numbers `a` and `b`, where `a` is neither zero nor infinity, the operation of dividing `b` by `a`, then multiplying the result by `a`, will yield `b` back. In mathematical terms, this theorem asserts that for `a` and `b` in the set of extended nonnegative real numbers (typically denoted as [0, ∞]), if `a` is not zero and `a` is not infinity, then `(b / a) * a = b`. This is akin to the mathematical principle that division and multiplication are inverse operations for non-zero and non-infinite numbers.
More concisely: For any extended nonnegative real numbers `a` and `b` with `a \neq 0 \neq \infty`, `(b / a) * a = b`.
|
ENNReal.coe_div
theorem ENNReal.coe_div : ∀ {r p : NNReal}, r ≠ 0 → ↑(p / r) = ↑p / ↑r
This theorem states that for any two non-negative real numbers `r` and `p`, as long as `r` is not zero, the operation of first dividing `p` by `r` and then taking the real number associated to the result is the same as first taking the real numbers associated to `p` and `r`, then performing the division. In other words, the process of division in the set of non-negative real numbers is compatible with the embedding of this set into the real numbers.
More concisely: For any non-zero real number `r` and non-negative real numbers `p`, the operation `(p : ℝ) / r` equal to `(real_of_num p) / real_of_num r` in the real numbers.
|
Mathlib.Data.ENNReal.Inv._auxLemma.10
theorem Mathlib.Data.ENNReal.Inv._auxLemma.10 : ∀ {a : ENNReal}, (a⁻¹ = 0) = (a = ⊤)
This theorem states that for every extended nonnegative real number `a`, the inverse of `a` is zero if and only if `a` is infinity. In other words, within the context of extended nonnegative real numbers, only infinity has a reciprocal of zero, and conversely, any extended nonnegative real number whose reciprocal is zero must be infinity.
More concisely: For every extended nonnegative real number `a`, `a^(-1) = 0` if and only if `a = ∞`.
|
ENNReal.inv_ne_top
theorem ENNReal.inv_ne_top : ∀ {a : ENNReal}, a⁻¹ ≠ ⊤ ↔ a ≠ 0
This theorem states that for any extended nonnegative real number `a`, the reciprocal of `a` is not infinity if and only if `a` is not zero. In other words, only zero has infinity as its reciprocal in the set of extended nonnegative real numbers.
More concisely: The reciprocal of a non-zero extended real number is finite.
|
ENNReal.mul_div_cancel'
theorem ENNReal.mul_div_cancel' : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * (b / a) = b
This theorem states that for any two extended nonnegative real numbers `a` and `b`, given that `a` is neither zero nor infinity, the multiplication of `a` and the division of `b` by `a` results in `b`. In mathematical terms, this corresponds to the identity `a * (b / a) = b` for `a` in the extended nonnegative real numbers that are neither zero nor infinity.
More concisely: For nonzero extended nonnegative real numbers `a` and `b`, `a * (b / a) = b`.
|
Mathlib.Data.ENNReal.Inv._auxLemma.1
theorem Mathlib.Data.ENNReal.Inv._auxLemma.1 : ∀ {r : NNReal}, r ≠ 0 → (↑r)⁻¹ = ↑r⁻¹
This theorem states that for any nonnegative real number `r` (denoted as `NNReal` in Lean 4), if `r` is not equal to 0, then the inverse of the coerced `r` (i.e., interpreting `r` as a real number) is equal to the coercion of the inverse of `r`. In mathematical terms, if we denote the operation of coercion as ↑, this theorem can be written as: for all `r` in nonnegative real numbers, if `r` is not equal to 0, then (↑r)⁻¹ = ↑(r⁻¹).
More concisely: For any non-zero non-negative real number `r`, the coerced inverse of `r` equals the inverse of the coerced `r`. In Lean notation: `(NNReal.coerce r).inv = NNReal.coerce (0 < r → r⁻¹)` where `⁻¹` denotes the inverse operation on real numbers.
|
ENNReal.inv_top
theorem ENNReal.inv_top : ⊤⁻¹ = 0
This theorem states that the inverse of positive infinity (denoted by ⊤) in the extended non-negative real number system equals zero. In other words, if you take the reciprocal of positive infinity, you get zero. This is consistent with the intuition that dividing any finite number by infinity results in zero.
More concisely: In the extended non-negative real numbers, ⊤^(-1) = 0.
|
ENNReal.inv_zero
theorem ENNReal.inv_zero : 0⁻¹ = ⊤
This theorem states that the reciprocal (or 'inverse') of zero in the extended non-negative real numbers is positive infinity. In other words, when you take 1 divided by 0 in the set of extended non-negative real numbers (which includes positive real numbers, zero, and positive infinity), you get positive infinity. This convention is often used in mathematical analysis to handle certain types of limits and operations.
More concisely: In the extended non-negative real numbers, 0^-1 = +∞.
|
ENNReal.coe_inv
theorem ENNReal.coe_inv : ∀ {r : NNReal}, r ≠ 0 → ↑r⁻¹ = (↑r)⁻¹
This theorem states that for any nonnegative real number `r` (represented as `NNReal`), if `r` is not equal to zero, then the inverse of the coerced `r` (i.e., `r` treated as an extended nonnegative real number, denoted by `↑r⁻¹`) is equal to the inverse of the coercion of `r` (denoted by `(↑r)⁻¹`). In simpler terms, when we inverse a nonnegative real number, it doesn't matter if we convert it to an extended nonnegative real number before or after taking the inverse; both processes yield the same result.
More concisely: For any nonzero `r` in `NNReal`, `↑r⁻¹ = (↑r)⁻¹`.
|
Mathlib.Data.ENNReal.Inv._auxLemma.5
theorem Mathlib.Data.ENNReal.Inv._auxLemma.5 : ∀ {a : ENNReal}, (a⁻¹ = ⊤) = (a = 0)
This theorem states that for all extended nonnegative real numbers 'a', 'a' inverted is equal to infinity if and only if 'a' is equal to zero. In other words, the reciprocal of any extended nonnegative real number is infinity exactly when the original number is zero.
More concisely: For all extended nonnegative real numbers $a$, $a^{-1} = \infty$ if and only if $a = 0$.
|
Mathlib.Data.ENNReal.Inv._auxLemma.13
theorem Mathlib.Data.ENNReal.Inv._auxLemma.13 : ∀ {a : ENNReal}, (0 < a⁻¹) = (a ≠ ⊤)
This theorem states that for every extended nonnegative real number `a`, the reciprocal of `a` is greater than zero if and only if `a` is not equal to infinity. In mathematical terms, for all `a` in extended nonnegative real numbers (usually denoted [0, ∞]), `0 < 1/a` if and only if `a ≠ ∞`.
More concisely: The reciprocal of a non-negative extended real number `a` is positive if and only if `a` is finite.
|
ENNReal.div_le_iff_le_mul
theorem ENNReal.div_le_iff_le_mul : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ ⊤ → b ≠ ⊤ ∨ c ≠ 0 → (a / b ≤ c ↔ a ≤ c * b) := by
sorry
This theorem states that for any extended nonnegative real numbers `a`, `b`, and `c`, given that either `b` is not zero or `c` is not infinity, and either `b` is not infinity or `c` is not zero, then the inequality `a / b ≤ c` is equivalent to `a ≤ c * b`. In other words, you can swap the division and multiplication in the inequality under these conditions. This theorem is crucial in measure theory and other mathematical fields, and it helps to manipulate inequalities involving extended nonnegative real numbers.
More concisely: For extended nonnegative real numbers `a`, `b`, and `c`, if `b` is nonzero and `c` is finite, or `b` is finite and `c` is nonzero, then `a / b ≤ c` is equivalent to `a ≤ c * b`.
|
ENNReal.mul_le_of_le_div'
theorem ENNReal.mul_le_of_le_div' : ∀ {a b c : ENNReal}, a ≤ b / c → c * a ≤ b
This theorem states that for all extended nonnegative real numbers `a`, `b`, and `c`, if `a` is less than or equal to the quotient of `b` divided by `c`, then the product of `c` and `a` is less than or equal to `b`. This essentially represents the property of order preservation under multiplication and division in the context of extended nonnegative real numbers.
More concisely: For all extended nonnegative real numbers `a`, `b`, and `c`, if `a ≤ b / c`, then `ac ≤ b`.
|
ENNReal.div_eq_inv_mul
theorem ENNReal.div_eq_inv_mul : ∀ {a b : ENNReal}, a / b = b⁻¹ * a
This theorem states that for all extended nonnegative real numbers `a` and `b`, the division of `a` by `b` is equivalent to the multiplication of the inverse of `b` and `a`. In mathematical terms, for any `a, b ∈ [0, ∞]`, the equation `a / b = b⁻¹ * a` holds true. This theorem expresses a fundamental property of division, namely that it can be represented as multiplication by the reciprocal.
More concisely: For all extended nonnegative real numbers `a` and `b`, `a / b = b⁻¹ * a`.
|
ENNReal.add_halves
theorem ENNReal.add_halves : ∀ (a : ENNReal), a / 2 + a / 2 = a
This theorem states that for every extended nonnegative real number `a`, the sum of half of `a` and half of `a` is equal to `a` itself. In other words, it confirms the basic arithmetic property that splitting a number into two equal halves and then adding these halves together results in the original number. This is usually denoted in mathematical notation as: for every $a \in [0, ∞]$, we have $a/2 + a/2 = a$.
More concisely: For every extended nonnegative real number `a`, the sum of `a` divided by 2 twice is equal to `a` itself. Or, in mathematical notation: ∀ (a : ℝ≥0∞), a / 2 + a / 2 = a.
|
ENNReal.zero_div
theorem ENNReal.zero_div : ∀ {a : ENNReal}, 0 / a = 0
This theorem states that for any extended nonnegative real number `a`, the result of dividing zero by `a` is zero. This result holds true for all values of `a` in the extended nonnegative real numbers, including the special case where `a` is infinity.
More concisely: For any extended nonnegative real number `a`, 0 / `a` = 0.
|
ENNReal.le_div_iff_mul_le
theorem ENNReal.le_div_iff_mul_le : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ 0 → b ≠ ⊤ ∨ c ≠ ⊤ → (a ≤ c / b ↔ a * b ≤ c) := by
sorry
The theorem `ENNReal.le_div_iff_mul_le` states that for all extended nonnegative real numbers `a`, `b`, and `c`, under the conditions that `b` is not zero or `c` is not zero, and `b` is not infinity or `c` is not infinity, then `a` is less than or equal to `c` divided by `b` if and only if `a` multiplied by `b` is less than or equal to `c`. This theorem is a common property in elementary algebra, often used in manipulations involving inequalities and divisions.
More concisely: For all extended nonnegative real numbers a, b, and c with b ≠ 0 ∧ c ≠ 0 ∧ b ≠ ∞ ∧ c ≠ ∞, a ≤ c / b if and only if a * b ≤ c.
|
ENNReal.inv_le_inv
theorem ENNReal.inv_le_inv : ∀ {a b : ENNReal}, a⁻¹ ≤ b⁻¹ ↔ b ≤ a
This theorem states that for any two extended nonnegative real numbers `a` and `b`, the inverse of `a` is less than or equal to the inverse of `b` if and only if `b` is less than or equal to `a`. Here, the extended nonnegative real numbers are denoted as ENNReal, which includes all nonnegative real numbers along with positive infinity. The notion of inverses and inequalities for this set is extended from the standard definitions for nonnegative real numbers.
More concisely: For any extended nonnegative real numbers `a` and `b`, `1/a <= 1/b` if and only if `a >= b`.
|
ENNReal.inv_strictAnti
theorem ENNReal.inv_strictAnti : StrictAnti Inv.inv
The theorem `ENNReal.inv_strictAnti` states that the inversion function (represented by `Inv.inv`) is strictly antitone. In mathematical terms, if we have two elements `a` and `b` such that `a < b`, then the inverse of `b` is less than the inverse of `a`. This property is called strict anti-monotonicity.
More concisely: For all `a` and `b` in the non-negative real numbers with `a < b`, we have `Inv.inv b < Inv.inv a`.
|
ENNReal.le_of_forall_nnreal_lt
theorem ENNReal.le_of_forall_nnreal_lt : ∀ {x y : ENNReal}, (∀ (r : NNReal), ↑r < x → ↑r ≤ y) → x ≤ y
The theorem `ENNReal.le_of_forall_nnreal_lt` states that for all extended nonnegative real numbers `x` and `y`, if for every nonnegative real number `r`, `r` is less than `x` implies that `r` is less than or equal to `y`, then `x` is less than or equal to `y`. In other words, if `x` is always greater than any given nonnegative real number that `y` is not less than, then `x` is at least as large as `y`.
More concisely: If for all nonnegative real numbers r, r < x implies r <= y, then x <= y.
|
ENNReal.div_le_div
theorem ENNReal.div_le_div : ∀ {a b c d : ENNReal}, a ≤ b → d ≤ c → a / c ≤ b / d
This theorem states that for any four extended nonnegative real numbers `a`, `b`, `c`, and `d`, if `a` is less than or equal to `b` and `d` is less than or equal to `c`, then the division of `a` by `c` is less than or equal to the division of `b` by `d`. In mathematical notation, this is equivalent to saying that if $a \leq b$ and $d \leq c$, then $\frac{a}{c} \leq \frac{b}{d}$.
More concisely: If $a \leq b$ and $c > 0$ with $d > 0$, then $\frac{a}{c} \leq \frac{b}{d}$.
|
ENNReal.div_le_of_le_mul
theorem ENNReal.div_le_of_le_mul : ∀ {a b c : ENNReal}, a ≤ b * c → a / c ≤ b
This theorem states that for all extended nonnegative real numbers `a`, `b`, and `c`, if `a` is less than or equal to the product of `b` and `c`, then the quotient of `a` and `c` is less than or equal to `b`. In mathematical notation, this can be written as: given $a, b, c \in [0, \infty]$ (extended nonnegative real numbers), if $a \leq b \cdot c$, then $\frac{a}{c} \leq b$.
More concisely: For all extended nonnegative real numbers $a$, $b$, and $c$, if $a \leq b \cdot c$, then $\frac{a}{c} \leq b$.
|
ENNReal.inv_mul_cancel
theorem ENNReal.inv_mul_cancel : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a⁻¹ * a = 1
The theorem `ENNReal.inv_mul_cancel` states that for all extended nonnegative real numbers `a`, where `a` is neither zero nor `∞`, the product of the multiplicative inverse of `a` and `a` itself is equal to 1. This is a property of division in standard real numbers being extended to the extended nonnegative real numbers. In mathematical terms, for any `a` in [0, ∞) excluding 0 and ∞, `a⁻¹ * a = 1`.
More concisely: For all extended nonnegative real numbers $a$ different from zero and infinity, $a^{-1} \cdot a = 1$.
|
Mathlib.Data.ENNReal.Inv._auxLemma.21
theorem Mathlib.Data.ENNReal.Inv._auxLemma.21 : ∀ {a b : ENNReal}, (a / b = 0) = (a = 0 ∨ b = ⊤)
The theorem `Mathlib.Data.ENNReal.Inv._auxLemma.21` states that for all extended nonnegative real numbers `a` and `b`, the fraction `a / b` equals zero if and only if `a` equals zero or `b` equals positive infinity. Here, `ENNReal` represents the extended nonnegative real numbers, typically denoted as [0, ∞], and `⊤` represents positive infinity.
More concisely: For all extended nonnegative real numbers `a` and `b`, `a / b = 0` if and only if `a = 0` or `b = ∞`.
|
ENNReal.add_div
theorem ENNReal.add_div : ∀ {a b c : ENNReal}, (a + b) / c = a / c + b / c
This theorem states that for any three extended nonnegative real numbers `a`, `b`, and `c`, the division of the sum of `a` and `b` by `c` is equal to the sum of the division of `a` by `c` and the division of `b` by `c`. In mathematical terms, this theorem is expressing the property $(a + b) / c = a / c + b / c$ for extended nonnegative real numbers, which is a common property in the field of real numbers.
More concisely: For extended nonnegative real numbers `a`, `b`, and `c`, the quotient of their sum by `c` equals the sum of their individual quotients by `c`. That is, $(a + b) / c = a / c + b / c$.
|
ENNReal.mul_lt_of_lt_div
theorem ENNReal.mul_lt_of_lt_div : ∀ {a b c : ENNReal}, a < b / c → a * c < b
This theorem states that for all extended nonnegative real numbers `a`, `b`, and `c`, if `a` is less than the quotient of `b` divided by `c`, then the product of `a` and `c` is less than `b`. In mathematical terms, if $a < \frac{b}{c}$, then $ac < b$. This theorem is applicable in the context of extended nonnegative real numbers, commonly used as the codomain of a measure.
More concisely: For all extended nonnegative real numbers $a$, $b$, and $c$, if $a < \frac{b}{c}$, then $ac < b$.
|
ENNReal.div_top
theorem ENNReal.div_top : ∀ {a : ENNReal}, a / ⊤ = 0
The theorem `ENNReal.div_top` states that for any extended nonnegative real number `a`, the division of `a` by positive infinity (`⊤`) is equal to zero. This aligns with the mathematical concept that any real number divided by infinity approaches zero.
More concisely: For any extended nonnegative real number `a`, `a / ⊤ = 0`.
|
ENNReal.div_self
theorem ENNReal.div_self : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a / a = 1
This theorem states that for any extended nonnegative real number `a`, as long as `a` is neither 0 nor infinity (denoted by `⊤`), the result of dividing `a` by itself is always 1. In other words, any nonzero, finite extended nonnegative real number divided by itself equals 1. This is a Lean 4 formalisation of the familiar algebraic property $\frac{a}{a} = 1$ for any non-zero real number `a`.
More concisely: Any nonzero extended nonnegative real number `a` satisfies `a / a = 1`.
|
ENNReal.inv_lt_inv
theorem ENNReal.inv_lt_inv : ∀ {a b : ENNReal}, a⁻¹ < b⁻¹ ↔ b < a
This theorem states that for any two extended nonnegative real numbers `a` and `b`, the inverse of `a` is less than the inverse of `b` if and only if `b` is less than `a`. The extended nonnegative real numbers are a representation of the range from zero to infinity, typically used as the codomain of a measure. The theorem essentially describes how the ordering relationship changes when taking inverses in this extended number system.
More concisely: For extended nonnegative real numbers `a` and `b`, `1/a < 1/b` if and only if `a < b`.
|
ENNReal.eq_top_of_forall_nnreal_le
theorem ENNReal.eq_top_of_forall_nnreal_le : ∀ {x : ENNReal}, (∀ (r : NNReal), ↑r ≤ x) → x = ⊤
The theorem `ENNReal.eq_top_of_forall_nnreal_le` states that for every extended nonnegative real number `x`, if all nonnegative real numbers `r` are less than or equal to `x`, then `x` is equal to infinity (∞). This applies to the scenario where `x` is an 'upper bound' for all nonnegative real numbers, and in such a case, `x` must be infinity.
More concisely: If every non-negative real number is less than or equal to an extended non-negative real number `x`, then `x` equals infinity.
|
ENNReal.inv_pos
theorem ENNReal.inv_pos : ∀ {a : ENNReal}, 0 < a⁻¹ ↔ a ≠ ⊤
The theorem `ENNReal.inv_pos` states that for every extended nonnegative real number `a`, the inverse of `a` is greater than 0 if and only if `a` is not infinity. Here `ENNReal` represents the set of extended nonnegative real numbers, which comprises all nonnegative real numbers plus the element infinity. The symbol `⁻¹` denotes the multiplicative inverse, `0 < a⁻¹` means that the inverse of `a` is positive, and `a ≠ ⊤` means that `a` is not equal to infinity.
More concisely: For every extended nonnegative real number `a`, the multiplicative inverse `a⁻¹` is positive if and only if `a` is finite.
|
ENNReal.div_lt_top
theorem ENNReal.div_lt_top : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ 0 → x / y < ⊤
This theorem states that for any two extended nonnegative real numbers `x` and `y`, if `x` is not infinity and `y` is not zero, then the result of `x / y` is finite, i.e., it is less than infinity. In other words, as long as you're not dividing an infinite number by a finite one, the result of division in the extended nonnegative real numbers will stay finite.
More concisely: For any extended nonnegative real numbers `x` and `y` with `y ≠ 0`, the quotient `x / y` is a finite nonnegative real number.
|
ENNReal.mul_inv_cancel
theorem ENNReal.mul_inv_cancel : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * a⁻¹ = 1
This theorem states that for any element `a` from the set of extended nonnegative real numbers (usually denoted as [0, ∞]), provided `a` is neither zero nor infinity, the result of multiplying `a` by its inverse (`a⁻¹`) is equal to 1. In mathematical terms, this theorem is expressing the property that every nonzero, non-infinite element in the set of extended nonnegative real numbers has a multiplicative inverse.
More concisely: For all nonzero and finite extended nonnegative real numbers `a`, `a * a⁻¹ = 1`.
|
ENNReal.inv_ne_zero
theorem ENNReal.inv_ne_zero : ∀ {a : ENNReal}, a⁻¹ ≠ 0 ↔ a ≠ ⊤
The theorem `ENNReal.inv_ne_zero` says that for all extended nonnegative real numbers `a`, the inverse of `a` is not equal to zero if and only if `a` is not equal to positive infinity. In other words, the only situation where the inverse of an extended nonnegative real number would be zero is if the original number was positive infinity.
More concisely: The extended nonnegative real number `a` has a multiplicative inverse equal to zero if and only if `a` is not positive infinity.
|