Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.3
theorem Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.3 :
∀ (x : NNReal) (y z : ℝ), (x ^ y) ^ z = x ^ (y * z)
The theorem `Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.3` states that for any nonnegative real number `x` and any real numbers `y` and `z`, the power of `x` raised to `y` to the power of `z` is the same as `x` to the power of the product of `y` and `z`. That is, $(x^y)^z = x^{y*z}$ for $x\geq 0$ and any real numbers $y$ and $z$. Here, `NNReal` stands for the set of nonnegative real numbers.
More concisely: For any non-negative real number $x$ and real numbers $y$ and $z$, $(x^y)^z = x^{y\cdot z}$.
|
NNReal.rpow_one
theorem NNReal.rpow_one : ∀ (x : NNReal), x ^ 1 = x
This theorem states that for every nonnegative real number `x`, raising `x` to the power of 1 is equal to `x` itself. In mathematical notation, this would be expressed as ∀x ∈ NNReal, x^1 = x. This means that the power function with exponent 1 is the identity function on the set of nonnegative real numbers.
More concisely: For all non-negative real numbers x, x^1 = x. (The power function with exponent 1 is the identity function on non-negative real numbers.)
|
NNReal.le_rpow_one_div_iff
theorem NNReal.le_rpow_one_div_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ≤ y ^ (1 / z) ↔ x ^ z ≤ y)
This theorem states that for any two nonnegative real numbers `x` and `y`, and any real number `z` that is greater than zero, `x` is less than or equal to `y` raised to the power of `1/z` if and only if `x` raised to the power of `z` is less than or equal to `y`. The theorem captures a property of the relationship between exponentiation and inequalities in the context of nonnegative real numbers.
More concisely: For nonnegative real numbers x and y, and real z > 0, x <= y^(1/z) if and only if x^z <= y.
|
NNReal.rpow_lt_rpow
theorem NNReal.rpow_lt_rpow : ∀ {x y : NNReal} {z : ℝ}, x < y → 0 < z → x ^ z < y ^ z
This theorem states that for any two nonnegative real numbers `x` and `y`, and any real number `z`, if `x` is less than `y` and `z` is greater than zero, then `x` raised to the power of `z` is less than `y` raised to the power of `z`. In mathematical terms, if $x < y$ and $z > 0$, then $x^z < y^z$.
More concisely: For any nonnegative real numbers $x$ and $y$ with $x < y$, and any positive real number $z$, $x^z < y^z$.
|
ENNReal.rpow_ne_top_of_nonneg
theorem ENNReal.rpow_ne_top_of_nonneg : ∀ {x : ENNReal} {y : ℝ}, 0 ≤ y → x ≠ ⊤ → x ^ y ≠ ⊤
The theorem `ENNReal.rpow_ne_top_of_nonneg` states that for any extended nonnegative real numbers `x` and any real number `y`, if `y` is nonnegative and `x` is not equal to positive infinity, then `x` raised to the power `y` (represented as `x ^ y`) will never be equal to positive infinity. This theorem is commonly used in measure theory, where the extended nonnegative real numbers often serve as the codomain of a measure.
More concisely: For all extended nonnegative real numbers `x` that are not positive infinity and all nonnegative real numbers `y`, `x^y` is finite.
|
Real.finset_prod_rpow
theorem Real.finset_prod_rpow :
∀ {ι : Type u_1} (s : Finset ι) (f : ι → ℝ),
(∀ i ∈ s, 0 ≤ f i) → ∀ (r : ℝ), (s.prod fun i => f i ^ r) = (s.prod fun i => f i) ^ r
The theorem `Real.finset_prod_rpow` states that for any finite set `s` of elements of an arbitrary type `ι`, and any function `f` from `ι` to the real numbers that is non-negative for all elements in `s`, for any real number `r`, the product over `s` of `f(i)` raised to the power `r` is equal to the product over `s` of `f(i)` all raised to the power `r`. In other words, the rule of exponents that says `(a*b)^r = a^r * b^r` holds when `a` and `b` are the results of applying the function `f` to the elements of the finite set `s`.
More concisely: For any finite set `s` and function `f` from `s` to the real numbers that is non-negative, the product of `f(i)^r` over `i` in `s` equals the product of `f(i)` raised to the power `r` over `i` in `s`.
|
ENNReal.rpow_le_rpow
theorem ENNReal.rpow_le_rpow : ∀ {x y : ENNReal} {z : ℝ}, x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z
This theorem states that for any two extended nonnegative real numbers `x` and `y`, and any real number `z` such that `z` is nonnegative and `x` is less than or equal to `y`, the exponentiation of `x` to the power `z` is less than or equal to the exponentiation of `y` to the power `z`. In mathematical notation, this would be: for all $x, y \in [0, \infty]$ and $z \in \mathbb{R}$ such that $x \leq y$ and $0 \leq z$, we have $x^z \leq y^z$.
More concisely: For all $x, y \in [0, \infty]$ and $z \in \mathbb{R}$ with $x \leq y$ and $0 \leq z$, we have $x^z \leq y^z$.
|
Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.2
theorem Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.2 :
∀ {x : NNReal} {y : ℝ}, (x ^ y = 0) = (x = 0 ∧ y ≠ 0)
This theorem states that for all nonnegative real numbers `x` and for all real numbers `y`, the proposition that `x` raised to the power `y` is equal to 0 is equivalent to the proposition that `x` is equal to 0 and `y` is not equal to 0. In mathematical notation, for all $x \in \text{NNReal}$ and $y \in \mathbb{R}$, $x^y = 0$ if and only if $x = 0$ and $y \neq 0$.
More concisely: For all non-negative real numbers $x$ and real numbers $y$, $x^y = 0$ if and only if $x = 0$ and $y \neq 0$.
|
ENNReal.coe_rpow_of_ne_zero
theorem ENNReal.coe_rpow_of_ne_zero : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ), ↑x ^ y = ↑(x ^ y)
This theorem states that for any non-zero nonnegative real number `x` and any real number `y`, the real-number exponentiation of the real part of `x` to the power `y` equals the real part of the nonnegative real-number exponentiation of `x` to the power `y`. In other words, when raising a non-zero nonnegative real number to any real power, taking the real part before or after the exponentiation operation does not change the result.
More concisely: For any non-zero nonnegative real number x and real number y, Re(x^y) = (Re(x))^y.
|
ENNReal.mul_rpow_eq_ite
theorem ENNReal.mul_rpow_eq_ite :
∀ (x y : ENNReal) (z : ℝ), (x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z := by
sorry
This theorem states that for any extended nonnegative real numbers `x` and `y`, and any real number `z`, the value of the expression `(x * y) ^ z` is equivalent to `∞` (denoted by `⊤` in Lean) if either `x` is `0` and `y` is `∞` or `x` is `∞` and `y` is `0` and `z` is less than `0`. Otherwise, the result is `x ^ z * y ^ z`. In other words, it gives a formula for exponentiation involving multiplication in the context of extended nonnegative real numbers, taking into account the special behavior at `0` and `∞`.
More concisely: For any extended nonnegative real numbers `x` and `y` and real number `z`, if `x = 0` and `y = ∞` or `x = ∞` and `y = 0` and `z < 0`, then `(x * y) ^ z = ⊤`, otherwise, `(x * y) ^ z = x ^ z * y ^ z`.
|
ENNReal.top_rpow_of_pos
theorem ENNReal.top_rpow_of_pos : ∀ {y : ℝ}, 0 < y → ⊤ ^ y = ⊤
This theorem states that for any real number `y` that is greater than zero, the exponentiation of the extended nonnegative real number infinity (`⊤`) to the power of `y` equals infinity (`⊤`). Essentially, an infinite quantity raised to any positive real number remains infinite.
More concisely: For any real number `y` > 0, ⊤^y = ⊤.
|
NNReal.sqrt_eq_rpow
theorem NNReal.sqrt_eq_rpow : ∀ (x : NNReal), NNReal.sqrt x = x ^ (1 / 2)
This theorem states that for any nonnegative real number `x`, the square root of `x` is equal to `x` raised to the power of one-half. In mathematical terms, this theorem is saying that for all `x` in the set of nonnegative real numbers, √x = x^(1/2). This is a property that captures the relationship between the operation of taking a square root and the operation of exponentiation in the realm of nonnegative real numbers.
More concisely: For all non-negative real numbers x, √x = x^(1/2).
|
ENNReal.coe_rpow_of_nonneg
theorem ENNReal.coe_rpow_of_nonneg : ∀ (x : NNReal) {y : ℝ}, 0 ≤ y → ↑x ^ y = ↑(x ^ y)
This theorem states that for any non-negative real number 'x', and any real number 'y' where 'y' is non-negative, the real number equivalent (or coercion) of 'x' raised to the power 'y' is equal to the real number equivalent of 'x' raised to the power 'y'. In other words, when 'y' is non-negative, the operation of exponentiation commutes with the operation of converting a non-negative real number to a real number.
More concisely: For any non-negative real numbers x and y, x^y = (reals x)^y.
|
ENNReal.mul_rpow_of_ne_top
theorem ENNReal.mul_rpow_of_ne_top : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → ∀ (z : ℝ), (x * y) ^ z = x ^ z * y ^ z := by
sorry
The theorem `ENNReal.mul_rpow_of_ne_top` states that for any two numbers `x` and `y` from the set of extended nonnegative real numbers (usually denoted as [0, ∞] and is relevant as the codomain of a measure), where neither `x` nor `y` are equal to ∞, and for any real number `z`, the power of the product of `x` and `y` raised to the `z` is equal to the product of `x` raised to `z` and `y` raised to `z`. This is a version of the power of a product property from elementary algebra, but specified for the set of extended nonnegative real numbers and excluding the case where `x` or `y` are ∞.
More concisely: For any extended nonnegative real numbers `x` and `y` not equal to ∞, and for any real number `z`, `x^z * y^z = (x * y)^z`.
|
ENNReal.rpow_le_rpow_iff
theorem ENNReal.rpow_le_rpow_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
This theorem in Lean 4 states that for all extended nonnegative real numbers `x` and `y`, and for any real number `z` that is greater than zero, the statement "x raised to the power of z is less than or equal to y raised to the power of z" is equivalent to the statement "x is less than or equal to y". Here, `ENNReal` denotes the set of extended nonnegative real numbers, which is typically denoted as [0, ∞] in standard mathematical notation.
More concisely: For all `x, y ∈ ENNReal` and `z > 0`, `x^z ≤ y^z` if and only if `x ≤ y`.
|
NNReal.rpow_neg
theorem NNReal.rpow_neg : ∀ (x : NNReal) (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
This theorem, `NNReal.rpow_neg`, states that for every non-negative real number `x` and any real number `y`, the expression `x` raised to the power of `-y` is equal to the reciprocal of `x` raised to the power of `y`. In mathematical notation, this theorem says that for all x in non-negative reals and all y in reals, \(x^{-y} = \frac{1}{x^y}\).
More concisely: For all non-negative real numbers x and real numbers y, $x^{-y} = \frac{1}{x^y}$.
|
ENNReal.zero_rpow_of_pos
theorem ENNReal.zero_rpow_of_pos : ∀ {y : ℝ}, 0 < y → 0 ^ y = 0
This theorem states that for any positive real number `y`, the result of raising 0 to the power `y` is 0. In mathematical terms, if `y` is a real number such that `y` > 0, then 0^`y` = 0.
More concisely: For any positive real number `y`, 0 raised to the power `y` equals 0.
|
NNReal.rpow_inv_rpow_self
theorem NNReal.rpow_inv_rpow_self : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ y) ^ (1 / y) = x
This theorem states that for all nonzero real numbers `y` and all nonnegative real numbers `x`, raising `x` to the power of `y`, and then raising the result to the power of `1/y`, equals `x` itself. In mathematical notation, this would be written as $(x^y)^{1/y} = x$ for all $x \geq 0$ and $y \neq 0$.
More concisely: For all nonzero real numbers y and nonnegative real numbers x, $(x^y)^{1/y} = x$.
|
ENNReal.toReal_rpow
theorem ENNReal.toReal_rpow : ∀ (x : ENNReal) (z : ℝ), x.toReal ^ z = (x ^ z).toReal
This theorem states that for every extended nonnegative real number `x` and any real number `z`, the operation of raising the real part of `x` to the power of `z` is equivalent to first raising `x` to the power of `z` and then taking the real part. In mathematical notation: for all $x \in [0, \infty]$ and $z \in \mathbb{R}$, $(\text{toReal}(x))^z = \text{toReal}(x^z)$. This property establishes a consistent interaction between the power operation and the transition from extended nonnegative real numbers to real numbers.
More concisely: For all $x \in [0, \infty]_{\mathbb{R}}$ and $z \in \mathbb{R}$, $\text{toReal}(x^z) = (\text{toReal}(x))^z$.
|
ENNReal.zero_rpow_of_neg
theorem ENNReal.zero_rpow_of_neg : ∀ {y : ℝ}, y < 0 → 0 ^ y = ⊤
This theorem states that for any real number `y` that is less than zero, the expression `0 ^ y` will evaluate to positive infinity. In mathematical terms, if y ∈ ℝ and y < 0, then 0 to the power of y (0^y) is positive infinity.
More concisely: For any real number `y` less than zero, `0^y` is positive infinity.
|
NNReal.rpow_le_rpow_iff
theorem NNReal.rpow_le_rpow_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
This theorem states that for any two nonnegative real numbers `x` and `y`, and any real number `z` that is greater than zero, `x` raised to the power `z` is less than or equal to `y` raised to the power `z` if and only if `x` is less than or equal to `y`. This is a property of exponents in the real number system.
More concisely: For any nonnegative real numbers x and y, and positive real number z, x^z ≤ y^z if and only if x ≤ y.
|
ENNReal.rpow_zero
theorem ENNReal.rpow_zero : ∀ {x : ENNReal}, x ^ 0 = 1
This theorem states that for every extended nonnegative real number `x`, raising `x` to the power of `0` results in `1`. This is a reflection of the mathematical principle that any non-zero number raised to the power of zero is `1`. The extended nonnegative real numbers, denoted as `[0, ∞]`, include all nonnegative real numbers along with positive infinity.
More concisely: For every extended nonnegative real number `x`, `x^0` equals 1.
|
NNReal.finset_prod_rpow
theorem NNReal.finset_prod_rpow :
∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ), (s.prod fun i => f i ^ r) = (s.prod fun i => f i) ^ r
The theorem `NNReal.finset_prod_rpow` states that for any type `ι`, any finite set `s` of this type, any function `f` from `ι` to nonnegative real numbers (`NNReal`), and any real number `r`, the product of the function values raised to the `r`th power taken over all elements in the set equals the power `r` of the product of the function values over all elements in the set. In mathematical terms, this is the statement that $(\prod_{i \in s} f(i))^r = \prod_{i \in s} (f(i)^r)$, where the product is taken over all elements of the finite set `s`.
More concisely: For any type `ι`, finite set `s` of `ι`, function `f` from `ι` to nonnegative real numbers, and real number `r`, we have $(\prod\_{i \in s} f(i))^r = \prod\_{i \in s} (f(i)^r)$.
|
NNReal.rpow_self_rpow_inv
theorem NNReal.rpow_self_rpow_inv : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ (1 / y)) ^ y = x
The theorem `NNReal.rpow_self_rpow_inv` states that for any non-zero real number `y`, and for any non-negative real number `x`, when `x` is raised to the power of `1/y` and the result is then raised to the power `y`, we get back the original number `x`. In mathematical terms, this can be written as \((x^{(1/y)})^y = x\). This theorem is essentially a version of the property of exponents which states that raising a number to the power of a fraction and then raising the result to the inverse of that fraction will return the original number.
More concisely: For any non-zero real number `y` and non-negative real number `x`, `x^(1/y) * x^y = x`.
|
ENNReal.mul_rpow_of_nonneg
theorem ENNReal.mul_rpow_of_nonneg : ∀ (x y : ENNReal) {z : ℝ}, 0 ≤ z → (x * y) ^ z = x ^ z * y ^ z
This theorem states that for all extended nonnegative real numbers 'x' and 'y', and for any real number 'z' that is nonnegative (i.e., 'z' is greater than or equal to zero), the power of the product 'x * y' raised to 'z' is equal to the product of 'x' raised to 'z' and 'y' raised to 'z'. In mathematical notation, this is saying that $(x * y) ^ z = x ^ z * y ^ z$ for $x, y \in [0, \infty]$ and $z \in \mathbb{R}$ with $z \geq 0$. This theorem is a key property of exponents in the context of extended nonnegative real numbers.
More concisely: For all extended nonnegative real numbers x, y, and nonnegative real number z, $(x * y) ^ z = x ^ z \cdot y ^ z$.
|
ENNReal.one_rpow
theorem ENNReal.one_rpow : ∀ (x : ℝ), 1 ^ x = 1
This theorem states that for any real number `x`, the power of `1` raised to `x` is always `1`. In mathematical notation, if `x` is any real number, then `1^x = 1`. This is a basic theorem in the field of real number algebra, demonstrating that any power of `1` remains `1`.
More concisely: For all real numbers x, 1^x = 1.
|
ENNReal.rpow_lt_top_of_nonneg
theorem ENNReal.rpow_lt_top_of_nonneg : ∀ {x : ENNReal} {y : ℝ}, 0 ≤ y → x ≠ ⊤ → x ^ y < ⊤
This theorem states that for any extended nonnegative real number `x` and any real number `y`, if `y` is greater than or equal to zero and `x` is not equal to positive infinity, then `x` raised to the power `y` is less than positive infinity. In mathematical notation, if $x \in [0, \infty)$, $y \in \mathbb{R}$, $y \geq 0$ and $x \neq \infty$, then $x^y < \infty$. The importance of this theorem is in the context of measure theory, where measures take values in the extended nonnegative real numbers.
More concisely: For any extended nonnegative real number $x$ not equal to positive infinity and any non-negative real number $y$, $x^y$ is finite.
|
NNReal.coe_rpow
theorem NNReal.coe_rpow : ∀ (x : NNReal) (y : ℝ), ↑(x ^ y) = ↑x ^ y
This theorem states that for all nonnegative real numbers `x` and any real number `y`, the real number representation of `x` raised to the power `y` is equal to the nonnegative real number `x` itself raised to the power `y`. In mathematical notation, this would be expressed as ∀x ∈ NNReal, ∀y ∈ ℝ, (x^y) = x^y, where ^ denotes exponentiation. The theorem involves the type coercion (↑) from `NNReal` to `ℝ`, which does not affect the value of exponentiation.
More concisely: For all non-negative real numbers x and real numbers y, x raised to the power y, with x coerced to a real number, equals x raised to the power y. (i.e., (↑x)^y = x^y)
|
ENNReal.strictMono_rpow_of_pos
theorem ENNReal.strictMono_rpow_of_pos : ∀ {z : ℝ}, 0 < z → StrictMono fun x => x ^ z
The theorem `ENNReal.strictMono_rpow_of_pos` states that for any real number `z` which is greater than `0`, the function `f(x) = x^z` is strictly increasing. This means that if `a` and `b` are any two numbers and `a < b`, then `a^z` will be less than `b^z`. Essentially, if you have a positive real exponent `z`, raising numbers to the power of `z` is a strictly monotone operation.
More concisely: For any real number `z > 0`, the function `x => x^z` is strictly increasing on the positive real numbers.
|
ENNReal.rpow_one
theorem ENNReal.rpow_one : ∀ (x : ENNReal), x ^ 1 = x
This theorem states that for any extended nonnegative real number `x`, raising `x` to the power of 1 is equal to `x` itself. In mathematical terms, for all `x` in the set of extended nonnegative real numbers, which is usually denoted as [0, ∞], it holds that x^1 = x. This rule reflects a fundamental property of exponents in the field of real numbers.
More concisely: For all extended nonnegative real numbers x, x^1 = x.
|
ENNReal.le_rpow_one_div_iff
theorem ENNReal.le_rpow_one_div_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ≤ y ^ (1 / z) ↔ x ^ z ≤ y)
The theorem `ENNReal.le_rpow_one_div_iff` states that for any extended nonnegative real numbers `x` and `y`, and any real number `z` greater than zero, `x` is less than or equal to the `z`th root of `y` if and only if `x` raised to the power `z` is less than or equal to `y`. In other words, it provides a relationship between the comparison of two extended nonnegative real numbers and the comparison of their powers.
More concisely: For any extended nonnegative real numbers `x` and `y`, and real number `z` > 0, `x` ≤ y if and only if x^z ≤ y.
|
Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.31
theorem Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.31 : ∀ {r : NNReal}, (0 < ↑r) = (0 < r)
This theorem, named `Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.31`, states that for every nonnegative real number `r`, the condition that the real part (or value) of `r` is greater than zero is equivalent to the condition that `r` itself is greater than zero. In essence, it establishes that checking whether a nonnegative real number `r` is positive is the same as checking whether the real part of `r` is positive.
More concisely: For every nonnegative real number `r`, `r` is positive if and only if its real part is positive.
|
ENNReal.inv_rpow
theorem ENNReal.inv_rpow : ∀ (x : ENNReal) (y : ℝ), x⁻¹ ^ y = (x ^ y)⁻¹
This theorem states that for all extended nonnegative real numbers `x` and any real number `y`, the inverse of `x` raised to the power `y` is equal to the inverse of `x` raised to the power `y`. Symbolically, this can be represented as $(x^{-1})^y = (x^y)^{-1}$. This property is commonly used in the manipulation of exponents and is part of the general rules of exponents in mathematics.
More concisely: For all extended nonnegative real numbers x and real number y, $(x^{-1})^y = (x^y)^{-1}$.
|
ENNReal.rpow_neg
theorem ENNReal.rpow_neg : ∀ (x : ENNReal) (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
The theorem `ENNReal.rpow_neg` states that for any extended nonnegative real number `x` and any real number `y`, the negative power of `x` raised to `y` is equal to the reciprocal of `x` raised to `y`. In mathematical notation, this can be written as `x^(-y) = (x^y)⁻¹`. This theorem is applicable in the context of extended nonnegative real numbers, which is typically used as the codomain of a measure. It provides a mathematical relationship for dealing with negative exponents in this context.
More concisely: For any extended nonnegative real number x and real number y, x^(-y) = (x^y)⁻¹.
|
Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.30
theorem Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.30 : ∀ {p : NNReal}, (↑p < 1) = (p < 1)
This theorem, which is from the Mathlib library in Lean 4, states that for all non-negative real numbers `p` (denoted as `NNReal`), the inequality of `p` being less than 1 in the context of real numbers (expressed as `↑p < 1`) is equivalent to `p` being less than 1 in the context of non-negative real numbers (expressed as `p < 1`). In other words, the embedding of `p` into the real numbers does not change the truth value of the inequality `p < 1`.
More concisely: For all non-negative real numbers `p`, the inequality `p < 1` in the context of non-negative real numbers is equivalent to the inequality `↑p < 1` in the context of real numbers.
|
NNReal.multiset_prod_map_rpow
theorem NNReal.multiset_prod_map_rpow :
∀ {ι : Type u_1} (s : Multiset ι) (f : ι → NNReal) (r : ℝ),
(Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
The theorem `NNReal.multiset_prod_map_rpow` states that for any multiset `s` of elements of some type `ι`, any function `f` mapping elements of `ι` to nonnegative real numbers (`NNReal`), and any real number `r`, the product of the multiset obtained by mapping each element `x` of `s` to `f(x)` raised to the power `r` is equal to the product of the multiset obtained by mapping `s` through `f`, all raised to the power `r`. In other words, the operation of raising to the power `r` commutes with the operation of taking the product over a multiset in the context of nonnegative real numbers.
More concisely: For any multiset `s` of non-negative real numbers and function `f` mapping elements to non-negative real numbers, the product of the multiset `{f(x) : x ∈ s}` raised to power `r` equals the product of `s` raised to power `r`, i.e., `∏(f(x)^r : x ∈ s) = ∏(x^r : x ∈ s)`.
|
Real.list_prod_map_rpow
theorem Real.list_prod_map_rpow :
∀ (l : List ℝ), (∀ x ∈ l, 0 ≤ x) → ∀ (r : ℝ), (List.map (fun x => x ^ r) l).prod = l.prod ^ r
This theorem states that for any list of real numbers `l` where every element `x` in `l` is nonnegative, and for any real number `r`, the product of all elements in `l` each raised to the power of `r` (after applying `List.map` with the function `x ^ r` to `l`) equals the product of all elements in `l` itself, raised to the power of `r`. In mathematical terms, this means that for any list of nonnegative real numbers, the operation $ (\prod_{i=1}^{n} x_{i})^r $ is equivalent to $ \prod_{i=1}^{n} x_{i}^r $, where $\prod$ denotes the product operation over the elements of the list.
More concisely: For any list of nonnegative real numbers, the product of each element raised to the power of a real number, is equal to the list's product raised to that power.
|
ENNReal.rpow_mul
theorem ENNReal.rpow_mul : ∀ (x : ENNReal) (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
This theorem states that for any extended nonnegative real number `x` and any two real numbers `y` and `z`, the exponentiation of `x` by the product of `y` and `z` is equal to the exponentiation of `x` raised to the power of `y`, then raised to the power of `z`. In mathematical notation, this can be written as \(x^{(y * z)} = ((x^y)^z)\). This theorem is demonstrating the property of exponentiation in the context of extended nonnegative real numbers.
More concisely: For any extended nonnegative real number x and real numbers y and z, x^(y * z) = (x^y)^z.
|
NNReal.zero_rpow
theorem NNReal.zero_rpow : ∀ {x : ℝ}, x ≠ 0 → 0 ^ x = 0
This theorem states that for any real number `x` that is not equal to zero, raising zero to the power of `x` always gives zero. In mathematical terms, for all `x ∈ ℝ` where `x ≠ 0`, `0^x = 0`.
More concisely: For all non-zero real numbers `x`, `0^x = 0`.
|
ENNReal.top_rpow_of_neg
theorem ENNReal.top_rpow_of_neg : ∀ {y : ℝ}, y < 0 → ⊤ ^ y = 0
This theorem states that for any real number `y`, if `y` is less than 0, then raising the extended non-negative real number "top" (which represents positive infinity) to the power `y` results in 0. In other words, in the extended non-negative real number system, positive infinity raised to any negative real number power equals zero.
More concisely: For any real number `y` less than 0, 0 = ∞^y in the extended non-negative real numbers.
|
Real.multiset_prod_map_rpow
theorem Real.multiset_prod_map_rpow :
∀ {ι : Type u_1} (s : Multiset ι) (f : ι → ℝ),
(∀ i ∈ s, 0 ≤ f i) → ∀ (r : ℝ), (Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
This theorem states that for any type `ι`, multiset `s` of type `ι`, function `f` mapping `ι` to real numbers, and any real number `r`, if every element of `s` mapped through `f` is greater than or equal to zero, then the product of the multiset obtained by mapping `s` through the function that raises `f x` to the power `r` is equal to the product of the multiset obtained by mapping `s` through `f`, raised to the power `r`. This is the version of the `Multiset.prod_map_pow` theorem for real powers, and it essentially states that the product of the powers is equal to the power of the product.
More concisely: For any type `ι`, multiset `s` of type `ι`, function `f`: `ι → ℝ`, and real number `r`, if every application of `f` to an element of `s` is non-negative, then the product of `s` raised to the power `r` using `f` is equal to the power of the product of `s` using `f`, raised to the power `r`.
|
NNReal.list_prod_map_rpow
theorem NNReal.list_prod_map_rpow : ∀ (l : List NNReal) (r : ℝ), (List.map (fun x => x ^ r) l).prod = l.prod ^ r := by
sorry
The theorem `NNReal.list_prod_map_rpow` states that for any list `l` of nonnegative real numbers and any real number `r`, the product of the elements of `l` each raised to the power `r` (i.e., `(List.map (fun x => x ^ r) l).prod`) is equal to the product of the elements of `l` raised to the power `r` (i.e., `l.prod ^ r`). In mathematical terms, this is saying that for the list $l = [a, b, c, \dots]$, we have $(a^r \cdot b^r \cdot c^r \cdot \dots) = (a \cdot b \cdot c \cdot \dots)^r$. This is a property of exponentiation applied to the product operation over lists of nonnegative real numbers.
More concisely: For any list of nonnegative real numbers and real number, the product of the list's elements raised to that power is equal to the list's product raised to that power. (i.e., `(List.map (fun x => x ^ r) l).prod = l.prod ^ r`)
|
NNReal.rpow_zero
theorem NNReal.rpow_zero : ∀ (x : NNReal), x ^ 0 = 1
This theorem states that for any nonnegative real number `x`, the zeroth power of `x` (`x` to the power of 0) is equal to 1. This is consistent with the general mathematical principle that any number (except 0) raised to the power of 0 is 1.
More concisely: For any non-negative real number x, x^0 = 1.
|
ENNReal.rpow_ofNat
theorem ENNReal.rpow_ofNat : ∀ (x : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n := by
sorry
This theorem states that for any extended nonnegative real number 'x' and any natural number 'n' that is at least two, the power of 'x' raised to the value 'n' (converted to the relevant type via the `OfNat.ofNat` function) is equal to itself. In other words, for any given values of 'x' and 'n', the operation 'x' raised to the power of 'n' is idempotent in the space of extended nonnegative real numbers.
More concisely: For any extended nonnegative real number x and natural number n ≥ 2, x^(OfNat.ofNat n) = x^(OfNat.ofNat n)^(OfNat.ofNat n).
Or, in simpler mathematical notation:
For any x ∈ ℝᵀ⁺ and n ∈ ℕ with n ≥ 2, x^n = x^n ^ n.
|
NNReal.rpow_mul
theorem NNReal.rpow_mul : ∀ (x : NNReal) (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
This theorem states that for any nonnegative real number `x` and any two real numbers `y` and `z`, the result of raising `x` to the power of the product of `y` and `z` is equal to the result of raising `x` to the power of `y`, and then raising the result to the power of `z`. In mathematical notation, this could be represented as \(x^{(y*z)} = ((x^y)^z)\). It's essentially asserting the property of exponentiation in the context of nonnegative real numbers.
More concisely: For any non-negative real number x and real numbers y and z, (x^(y*z)) = (x^y)^z.
|
Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.15
theorem Mathlib.Analysis.SpecialFunctions.Pow.NNReal._auxLemma.15 :
∀ {x : ENNReal} {y : ℝ}, (x ^ y = ⊤) = (x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y)
This theorem states that for any extended nonnegative real number "x" and any real number "y", the condition of "x" raised to the power "y" being equal to positive infinity is equivalent to either of the two following scenarios: (1) "x" is zero and "y" is negative, or (2) "x" is positive infinity and "y" is positive. Here, the extended nonnegative real numbers are denoted by `[0, ∞]` and they represent the codomain of a measure.
More concisely: For any extended nonnegative real number x and real number y, x^y = +∞ if and only if (x = 0 and y < 0) or (x = +∞ and y > 0).
|