Real.rpow_def_of_neg
theorem Real.rpow_def_of_neg : ∀ {x : ℝ}, x < 0 → ∀ (y : ℝ), x ^ y = (x.log * y).exp * (y * Real.pi).cos
This theorem states that for any real number `x` that is less than zero, and for any real number `y`, the power of `x` raised to `y` (denoted as `x ^ y`) can be expressed in terms of the exponential, logarithm, and cosine functions. Specifically, `x ^ y` is equal to the product of the exponential of the logarithm of `x` multiplied by `y`, and the cosine of the product of `y` and the constant pi (`π`). In mathematical notation, this can be written as: if `x` is a real number such that `x < 0`, and `y` is any real number, then `x ^ y = exp(log(x) * y) * cos(y * π)`.
More concisely: For any real number `x` with `x < 0` and any real number `y`, `x^y` equals the product of `exp(log(x)*y)` and `cos(y*π)`.
|
Real.rpow_zero
theorem Real.rpow_zero : ∀ (x : ℝ), x ^ 0 = 1
This theorem states that for any real number `x`, it raised to the power of 0 is equal to 1. This is a property of exponentiation in mathematics, where any non-zero number to the power of zero is defined as 1.
More concisely: For all real numbers x, x^0 = 1.
|
Real.le_rpow_add
theorem Real.le_rpow_add : ∀ {x : ℝ}, 0 ≤ x → ∀ (y z : ℝ), x ^ y * x ^ z ≤ x ^ (y + z)
This theorem states that for any real number `x` such that `0 ≤ x`, and any real numbers `y` and `z`, the inequality `x ^ y * x ^ z ≤ x ^ (y + z)` is always true. The only special case we need to be careful of is when `x = 0` and `y + z = 0`, in which case the right hand side equals `1` but the left hand side can be `0`. But in general, the product of `x` raised to the power of `y` and `x` raised to the power of `z` is always less than or equal to `x` raised to the power of `y + z`.
More concisely: For any real numbers `x` greater than or equal to 0, `y`, and `z`, `x^y * x^z ≤ x^(y + z)`. However, if `x = 0` or `y + z = 0`, the inequality may not hold.
|
Real.log_natCast_le_rpow_div
theorem Real.log_natCast_le_rpow_div : ∀ (n : ℕ) {ε : ℝ}, 0 < ε → (↑n).log ≤ ↑n ^ ε / ε
This theorem states that for any natural number `n` and any real number `ε` such that `ε` is greater than 0, the natural logarithm of `n` is less than or equal to `n` raised to the power `ε` divided by `ε`. In terms of mathematical notation, if we have a natural number `n` and a positive real number `ε`, then we have `log(n) ≤ n^ε / ε`.
More concisely: For any natural number `n` and positive real number `ε`, `log(n) ≤ n^ε / ε`.
|
Real.abs_log_mul_self_rpow_lt
theorem Real.abs_log_mul_self_rpow_lt : ∀ (x t : ℝ), 0 < x → x ≤ 1 → 0 < t → |x.log * x ^ t| < 1 / t
This theorem states that for all real numbers `x` and `t`, if `x` is positive and less than or equal to 1, and `t` is positive, then the absolute value of the product of the natural logarithm of `x` and `x` raised to the power of `t` is less than the reciprocal of `t`. In mathematical terms, it denotes that for every `0 < x ≤ 1` and `0 < t`, it holds that `|log(x) * x^t| < 1/t`.
More concisely: For all positive real numbers x <= 1 and t > 0, |log(x) * x^t| < 1/t.
|
Real.log_rpow
theorem Real.log_rpow : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), (x ^ y).log = y * x.log
This theorem states that for any real number `x` that is greater than zero and for any other real number `y`, the logarithm of `x` raised to the power of `y` is equal to `y` times the logarithm of `x`. In other words, for $x > 0$ and any $y$, $\log(x^y) = y \log(x)$. This is a formal statement of a well-known logarithmic identity in the real number context.
More concisely: For any real numbers $x > 0$ and $y$, $\log(x^y) = y\log(x)$.
|
Real.zero_rpow
theorem Real.zero_rpow : ∀ {x : ℝ}, x ≠ 0 → 0 ^ x = 0
This theorem states that for any real number 'x' which is not equal to zero, the real number zero raised to the power of 'x' results in zero. In mathematical notation, this is expressed as `0^x = 0` for all `x ≠ 0`.
More concisely: For any non-zero real number x, 0 raised to the power x equals 0.
|
Real.rpow_add'
theorem Real.rpow_add' : ∀ {x y z : ℝ}, 0 ≤ x → y + z ≠ 0 → x ^ (y + z) = x ^ y * x ^ z
This theorem states that for any real numbers `x`, `y`, and `z`, given that `x` is nonnegative and the sum of `y` and `z` is nonzero, the power of `x` raised to the sum of `y` and `z` is equal to the product of `x` raised to `y` and `x` raised to `z`. This is essentially the property of exponents $x^{y + z} = x^y * x^z$, extended to real numbers with some restrictions.
More concisely: For real numbers `x` > 0 and `y`, `z` such that `y + z` ≠ 0, `x^(y + z)` = `x^y * x^z`.
|
Real.rpow_lt_rpow_iff
theorem Real.rpow_lt_rpow_iff : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z < y ^ z ↔ x < y)
This theorem states that for all real numbers `x`, `y`, and `z`, given that `x` and `y` are non-negative (i.e., greater than or equal to zero), and `z` is strictly positive (greater than zero), then `x` raised to the power of `z` is less than `y` raised to the power of `z` if and only if `x` is less than `y`. Essentially, it's about how powers preserve the order of non-negative real numbers when the exponent is positive.
More concisely: For all non-negative real numbers x, y, and positive real number z, x^z < y^z if and only if x < y.
|
Real.rpow_le_rpow_iff
theorem Real.rpow_le_rpow_iff : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
This theorem states that for any real numbers `x`, `y`, and `z`, given that `x` and `y` are non-negative and `z` is positive, `x` raised to the power of `z` is less than or equal to `y` raised to the power of `z` if and only if `x` is less than or equal to `y`. In mathematical notation, this is expressed as: for all real numbers `x`, `y`, `z` such that `0 ≤ x`, `0 ≤ y` and `0 < z`, we have that `x ^ z ≤ y ^ z` if and only if `x ≤ y`.
More concisely: For real numbers `x`, `y`, and `z` with `0 ≤ x`, `0 ≤ y`, and `0 < z`, `x ^ z ≤ y ^ z` if and only if `x ≤ y`.
|
Real.rpow_add
theorem Real.rpow_add : ∀ {x : ℝ}, 0 < x → ∀ (y z : ℝ), x ^ (y + z) = x ^ y * x ^ z
This theorem states that for any real number `x` that is greater than zero and any two real numbers `y` and `z`, the exponentiation of `x` to the power of the sum of `y` and `z` is equal to the product of `x` raised to the power of `y` and `x` raised to the power of `z`. In mathematics notation, this can be written as: if $0 < x$ and $y, z \in \mathbb{R}$, then $x^{y+z} = x^y \cdot x^z$. This property is an important characteristic of exponentiation.
More concisely: For any real number `x` > 0, `x^(y + z)` equals `x^y * x^z` for all `y, z` in the real numbers.
|
Real.rpow_sub'
theorem Real.rpow_sub' : ∀ {x : ℝ}, 0 ≤ x → ∀ {y z : ℝ}, y - z ≠ 0 → x ^ (y - z) = x ^ y / x ^ z
This theorem states that for any real number `x` that is greater than or equal to zero, and for any real numbers `y` and `z` such that their difference is not zero, the power of `x` raised to the difference of `y` and `z` is equal to the ratio of the power of `x` raised to `y` and the power of `x` raised to `z`. In mathematical notation, this would be represented as: for all $x$, $y$, $z$ in $\mathbb{R}$ with $x \geq 0$ and $y - z \neq 0$, $x^{y-z} = \frac{x^y}{x^z}$.
More concisely: For any real numbers $x \ge 0$, $y$, and $z$ with $y \neq z$, $x^{y-z} = \frac{x^y}{x^z}$.
|
Real.rpow_neg_one
theorem Real.rpow_neg_one : ∀ (x : ℝ), x ^ (-1) = x⁻¹
This theorem states that for any real number `x`, raising `x` to the power of `-1` is equivalent to the multiplicative inverse of `x` (denoted as `x⁻¹`). In other words, for any real number, the operation of taking the power of `-1` is the same as taking the reciprocal. This is a standard result in real number arithmetic.
More concisely: For any real number x, x^(-1) = 1/x (or x^(-1) is the multiplicative inverse of x).
|
Real.rpow_neg
theorem Real.rpow_neg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x ^ (-y) = (x ^ y)⁻¹
This theorem states that for any real number `x` that is non-negative, and for any real number `y`, the power of `x` to the negation of `y` (i.e., `x` raised to the power `-y`) is equal to the reciprocal of `x` raised to the power `y`. This is a standard rule of exponents that is also valid in the realm of real numbers.
More concisely: For any non-negative real number `x` and real number `y`, `x^(-y) = 1/x^y`.
|
Real.inv_rpow
theorem Real.inv_rpow : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x⁻¹ ^ y = (x ^ y)⁻¹
This theorem states that for any real number `x` which is greater than or equal to zero, and for any real number `y`, the inverse of `x` raised to the power of `y` is equal to the inverse of `x` raised to the power of `y`. In mathematical notation, this is written as (for every `x ≥ 0` and any `y` in the real numbers) `1/x^y = (x^y)^-1`.
More concisely: For any non-negative real number `x` and real number `y`, `(x^y)^-1 = 1/x^y`.
|
Real.exp_mul
theorem Real.exp_mul : ∀ (x y : ℝ), (x * y).exp = x.exp ^ y
This theorem states that for all real numbers `x` and `y`, the exponential function of the product of `x` and `y` is equal to the exponential function of `x` raised to the power `y`. In mathematical notation, this can be written as: for all `x, y` in ℝ, exp(xy) = (exp(x))^y. This is an important property of the exponential function in real numbers, which is defined as the real part of the complex exponential function.
More concisely: For all real numbers x and y, exp(xy) = (exp x)^y.
|
Real.rpow_two
theorem Real.rpow_two : ∀ (x : ℝ), x ^ 2 = x ^ 2
This theorem is stating that for every real number `x`, the square of `x` is equal to the square of `x`. In other words, the square of any real number is always consistent and equal to itself. The square of a number is calculated by raising it to the power of 2, thus `x ^ 2` represents the square of `x` in this context. It's a simple and straightforward mathematical identity.
More concisely: For every real number x, x ^ 2 equals x ^ 2. (The square of a real number is self-equal.)
|
Complex.norm_natCast_cpow_of_pos
theorem Complex.norm_natCast_cpow_of_pos : ∀ {n : ℕ}, 0 < n → ∀ (s : ℂ), ‖↑n ^ s‖ = ↑n ^ s.re
The theorem `Complex.norm_natCast_cpow_of_pos` states that for any positive natural number `n` and any complex number `s`, the norm of `n` (casted to a complex number) raised to the power `s` is equal to `n` (casted to a complex number) raised to the real part of `s`. This can be formally written as: for all `n` in natural numbers and `s` in complex numbers, if `n` is greater than 0, then the complex norm of `n` to the power of `s` equals `n` to the power of the real part of `s`.
More concisely: For any positive natural number `n` and complex number `s`, the complex norm of `n` raised to the power of `s` equals `n` raised to the real part of `s`.
|
Real.rpow_def_of_nonneg
theorem Real.rpow_def_of_nonneg :
∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), x ^ y = if x = 0 then if y = 0 then 1 else 0 else (x.log * y).exp
This theorem provides a definition for raising a non-negative real number `x` to any real power `y`. It states that for every real number `x` that is greater than or equal to 0, and any real number `y`, `x` raised to the power `y` equals to the exponential of the real logarithm of `x` multiplied by `y`, unless `x` equals to 0. If `x` is 0, then the result will be 1 if `y` is also 0, and 0 for any other value of `y`.
More concisely: For non-negative real numbers `x` and `y`, `x^y` equals `exp(y * log(x))` if `x` is not 0, and equals 1 if both `x` and `y` are 0.
|
Real.rpow_nonneg
theorem Real.rpow_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), 0 ≤ x ^ y
This theorem states that for all real numbers `x`, if `x` is greater than or equal to zero, then for any real number `y`, `x` raised to the power of `y` (x^y) will also be greater than or equal to zero. In other words, it proves that any non-negative real number raised to any real number power is non-negative.
More concisely: For all real numbers `x` and `y`, if `x` is non-negative, then `x^y` is non-negative.
|
Real.rpow_le_rpow
theorem Real.rpow_le_rpow : ∀ {x y z : ℝ}, 0 ≤ x → x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z
This theorem states that for any real numbers `x`, `y`, and `z`, if `x` is non-negative, `x` is less than or equal to `y`, and `z` is non-negative, then `x` raised to the power of `z` is less than or equal to `y` raised to the power of `z`. It expresses a property of exponentiation in the real numbers.
More concisely: For all real numbers x, y, and z where x ≥ 0 and z ≥ 0, x^z ≤ y^z.
|
Real.rpow_lt_rpow_iff_of_neg
theorem Real.rpow_lt_rpow_iff_of_neg : ∀ {x y z : ℝ}, 0 < x → 0 < y → z < 0 → (x ^ z < y ^ z ↔ y < x)
This theorem states that for any three real numbers `x`, `y`, and `z`, if `x` and `y` are both positive and `z` is negative, then `x` raised to the power of `z` is less than `y` raised to the power of `z` if and only if `y` is less than `x`. This essentially lays down a condition under which we can compare the powers of two positive numbers, given a negative exponent.
More concisely: For real numbers x, y, and z with x > 0, y > 0, and z < 0, x^z < y^z if and only if y < x.
|
Real.rpow_def
theorem Real.rpow_def : ∀ (x y : ℝ), x ^ y = (↑x ^ ↑y).re
This theorem states that for any two real numbers `x` and `y`, the expression `x ^ y` (which represents x raised to the power y) is equal to the real part of `x` and `y` cast to complex numbers (`↑x ^ ↑y`) raised to the power of each other. In other words, exponentiation in the real numbers can be defined in terms of exponentiation in the complex numbers, when we only consider the real part of the result.
More concisely: For all real numbers x and y, x ^ y = ↑(xc ^ ↑y), where xc is the complex number obtained by lifting x to the complex plane.
|
Real.log_le_rpow_div
theorem Real.log_le_rpow_div : ∀ {x ε : ℝ}, 0 ≤ x → 0 < ε → x.log ≤ x ^ ε / ε
The theorem `Real.log_le_rpow_div` states that for all real numbers `x` and `ε`, where `x` is nonnegative and `ε` is positive, the natural logarithm of `x` (`log x`) is less than or equal to `x` raised to the power of `ε`, divided by `ε`. In mathematical notation, this is $\log(x) \leq \frac{x^\varepsilon}{\varepsilon}$ for all $x \geq 0$ and $\varepsilon > 0$. Essentially, this theorem says that the natural logarithm of `x` is upper-bounded by a multiple of any positive power of `x`.
More concisely: For all non-negative real numbers `x` and positive real numbers `ε`, we have `log x ≤ x^ε / ε`.
|
Real.one_rpow
theorem Real.one_rpow : ∀ (x : ℝ), 1 ^ x = 1
This theorem states that for every real number `x`, the real number `1` raised to the power of `x` always equals `1`. This is a mathematical property of the number `1` in real number space where any power of `1` results in `1`.
More concisely: For all real numbers x, 1^x = 1.
|
Complex.abs_cpow_eq_rpow_re_of_pos
theorem Complex.abs_cpow_eq_rpow_re_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℂ), Complex.abs (↑x ^ y) = x ^ y.re
This theorem states that for a given real number `x` that is greater than zero, and for any complex number `y`, the absolute value of `x` raised to the power of `y` in the complex number system (i.e., `x` as a complex number) is equal to `x` raised to the real part of `y` in the standard real number calculus. This theorem establishes a connection between complex exponentiation and real exponentiation when the base is a positive real number.
More concisely: For any complex number `y` and positive real number `x`, |x^(Re(y))| = |x|^(Re(y)), where |.| denotes the absolute value in the complex number system.
|
Real.rpow_pos_of_pos
theorem Real.rpow_pos_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), 0 < x ^ y
This theorem states that for all real numbers `x`, if `x` is greater than 0, then for any real number `y`, `x` raised to the power of `y` (represented as `x ^ y`) is also greater than 0. In other words, the result of raising a positive real number to any power is always a positive real number.
More concisely: For all real numbers `x` and `y`, if `x > 0`, then `x ^ y > 0`.
|
Real.rpow_inv_rpow
theorem Real.rpow_inv_rpow : ∀ {x y : ℝ}, 0 ≤ x → y ≠ 0 → (x ^ y⁻¹) ^ y = x
This theorem states that for all real numbers 'x' and 'y', if 'x' is nonnegative and 'y' is nonzero, then raising 'x' to the power of the reciprocal of 'y', and then raising the result to the power of 'y', gives back 'x'. This equation can be expressed mathematically as: `(x^(1/y))^y = x`.
More concisely: For all nonnegative real numbers x and nonzero y, (x^(1/y))^y = x.
|
Real.rpow_lt_rpow
theorem Real.rpow_lt_rpow : ∀ {x y z : ℝ}, 0 ≤ x → x < y → 0 < z → x ^ z < y ^ z
This theorem states that for any real numbers `x`, `y`, and `z`, if `x` is non-negative, `x` is less than `y`, and `z` is positive, then `x` raised to the power of `z` is less than `y` raised to the power of `z`. In other words, if you have two real numbers where one is smaller than the other and a positive exponent, the exponentiation of the smaller number is also smaller than the exponentiation of the larger number.
More concisely: For any real numbers `x` with `x ≥ 0`, `y` with `x < y`, and `z` with `z > 0`, we have `x^z < y^z`.
|
Complex.abs_cpow_eq_rpow_re_of_nonneg
theorem Complex.abs_cpow_eq_rpow_re_of_nonneg :
∀ {x : ℝ}, 0 ≤ x → ∀ {y : ℂ}, y.re ≠ 0 → Complex.abs (↑x ^ y) = x ^ y.re
This theorem states that for any nonnegative real number `x` and any complex number `y` with a non-zero real part, the absolute value of `x` raised to the power of `y` (where `x` is considered as a complex number) is equal to `x` raised to the power of the real part of `y`. In mathematical notation, this can be written as: for all $x \geq 0$ and $y \in \mathbb{C}$ with $\Re(y) \neq 0$, $|x^y| = x^{\Re(y)}$.
More concisely: For any nonnegative real number $x$ and complex number $y$ with non-zero real part, $|x^y| = x^{\Re(y)}$.
|
Real.rpow_le_one
theorem Real.rpow_le_one : ∀ {x z : ℝ}, 0 ≤ x → x ≤ 1 → 0 ≤ z → x ^ z ≤ 1
The theorem `Real.rpow_le_one` states that for any real numbers `x` and `z`, if `x` is non-negative and less than or equal to 1, and `z` is also non-negative, then `x` raised to the power of `z` will always be less than or equal to 1. This is a property about exponentiation in the set of real numbers.
More concisely: For all real numbers `x` and `z` with `0 ≤ x ≤ 1` and `z ≥ 0`, `x^z ≤ 1`.
|
Real.rpow_le_rpow_left_iff_of_base_lt_one
theorem Real.rpow_le_rpow_left_iff_of_base_lt_one : ∀ {x y z : ℝ}, 0 < x → x < 1 → (x ^ y ≤ x ^ z ↔ z ≤ y)
This theorem states that for any three real numbers `x`, `y`, and `z`, if `x` is positive and less than one, then `x` raised to the power of `y` is less than or equal to `x` raised to the power of `z` if and only if `z` is less than or equal to `y`. In mathematical terms, for all real numbers x, y, z where 0 < x < 1, it holds that x^y ≤ x^z if and only if z ≤ y.
More concisely: For real numbers x, y, and z with 0 < x < 1, x^y ≤ x^z if and only if z ≤ y.
|
Real.sqrt_eq_rpow
theorem Real.sqrt_eq_rpow : ∀ (x : ℝ), x.sqrt = x ^ (1 / 2)
The theorem `Real.sqrt_eq_rpow` states that for every real number `x`, the square root of `x` is equivalent to `x` raised to the power of `1/2`. In mathematical terms, this theorem verifies the principle that the square root function (√x) and the fractional exponentiation function (x^(1/2)) are the same for any given real number `x`.
More concisely: For all real numbers x, sqrt(x) = x^(1/2).
|
Real.rpow_def_of_pos
theorem Real.rpow_def_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℝ), x ^ y = (x.log * y).exp
The theorem `Real.rpow_def_of_pos` states that for any real number `x` that is greater than zero, and for any other real number `y`, the exponentiation of `x` to the power of `y` is equal to the real exponential function of the product of the real logarithm of `x` and `y`. In mathematical terms, this means for all `x > 0` and any `y`, we have `x^y = exp(log(x) * y)`.
More concisely: For all `x > 0` in the real numbers, `x^y` equals the exponential function `exp(log(x) * y)`.
|
Real.rpow_mul
theorem Real.rpow_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
This theorem states that for any real number `x` that is greater than or equal to zero, and for any two real numbers `y` and `z`, the power of `x` raised to the product of `y` and `z` is equal to `x` raised to the power `y` and then the result raised to the power `z`. In LaTeX, this is expressed as `x^{yz} = (x^y)^z` for all `x ≥ 0`, `y`, and `z` in the set of real numbers.
More concisely: For any real number `x ≥ 0`, `x^(yz) = (x^y)^z`.
|
Real.abs_rpow_of_nonneg
theorem Real.abs_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → |x ^ y| = |x| ^ y
This theorem states that for any real numbers `x` and `y`, if `x` is non-negative (i.e., `x` is greater than or equal to 0), then the absolute value of `x` raised to the power of `y` is equal to the absolute value of `x` raised to the power of `y`. In mathematical notation, this reads: for all $x, y \in \mathbb{R}$ with $x \geq 0$, we have $|x^y| = |x|^y$.
More concisely: For all real numbers $x \geq 0$ and $y$, $|x|^y = |x^y|$.
|
Complex.ofReal_cpow
theorem Complex.ofReal_cpow : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), ↑(x ^ y) = ↑x ^ ↑y
This theorem states that for any real number `x` that is greater than or equal to zero, and for any real number `y`, the complex representation of `x` raised to the power of `y` is equal to the complex representation of `x` raised to the power of the complex representation of `y`. In other words, if `x` is a non-negative real number and `y` is any real number, then `(x ^ y)` converted to a complex number is the same as `x` converted to a complex number and then raised to the power of `y` converted to a complex number. In mathematical notation, this could be expressed as ∀ x, y ∈ ℝ, x ≥ 0 ⇒ (x ^ y) ∈ ℂ = (x ∈ ℂ) ^ (y ∈ ℂ).
More concisely: For any non-negative real number `x` and complex number `y`, `x^y` equals the complex number `x` raised to the power of `y`.
|
rpow_nonneg_of_nonneg
theorem rpow_nonneg_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), 0 ≤ x ^ y
This theorem, `rpow_nonneg_of_nonneg`, is an alias of `Real.rpow_nonneg`. It states that for any real number `x` that is non-negative (0 ≤ x), for all real numbers `y`, `x` raised to the power of `y` (x ^ y) will also be non-negative (0 ≤ x ^ y).
More concisely: For any non-negative real number x and any real number y, x^y ≥ 0.
|
Real.rpow_one
theorem Real.rpow_one : ∀ (x : ℝ), x ^ 1 = x
This theorem states that for any real number `x`, raising `x` to the power of `1` results in `x` itself. This is a standard property of exponentiation in mathematics, usually written as $x^1 = x$ for all real numbers $x$.
More concisely: For all real numbers x, x^1 = x.
|
Real.rpow_le_rpow_of_exponent_le
theorem Real.rpow_le_rpow_of_exponent_le : ∀ {x y z : ℝ}, 1 ≤ x → y ≤ z → x ^ y ≤ x ^ z
This theorem states that for all real numbers x, y, and z, if x is greater than or equal to 1 and y is less than or equal to z, then x raised to the power of y is less than or equal to x raised to the power of z. In other words, for any real number x that is at least 1, increasing the exponent from y to z (where z ≥ y) only increases (or keeps the same) the power of x.
More concisely: For all real numbers x, y, and z with x ≥ 1 and y ≤ z, x^y ≤ x^z.
|
Real.exists_rat_pow_btwn
theorem Real.exists_rat_pow_btwn :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : Archimedean α],
n ≠ 0 → ∀ {x y : α}, x < y → 0 < y → ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
This theorem states that for every natural number `n` that is not zero, and for any two positive elements `x` and `y` of an archimedean linearly ordered field `α` where `x` is less than `y`, there exists a positive rational number `q` such that `x` is less than `q` to the power of `n` and `q` to the power of `n` is less than `y`. In other words, there's a rational power between any two positive elements in this kind of field.
More concisely: For every archimedean linearly ordered field `α` and natural number `n` (`n > 0`), and for any positive elements `x` and `y` in `α` with `x < y`, there exists a positive rational number `q` such that `x < q^n < y`.
|
Complex.abs_cpow_of_imp
theorem Complex.abs_cpow_of_imp :
∀ {z w : ℂ}, (z = 0 → w.re = 0 → w = 0) → Complex.abs (z ^ w) = Complex.abs z ^ w.re / (z.arg * w.im).exp := by
sorry
This theorem, `Complex.abs_cpow_of_imp`, states that for any two complex numbers `z` and `w`, if `z` equals to zero implies that the real part of `w` equals to zero and `w` equals to zero, then the absolute value of `z` raised to the power of `w` equals to the absolute value of `z` raised to the power of the real part of `w` divided by the exponential of the product of the argument of `z` and the imaginary part of `w`. More formally, for all complex numbers `z` and `w`, if `z = 0` implies `(w.re = 0 and w = 0)`, then `|z ^ w| = |z|^(w.re) / exp(arg(z) * w.im)`.
More concisely: If complex number `z` equals to zero implies real and imaginary parts of `w` are zero, then `|z|^(w.re) * exp(-arg(z) * w.im) = |z|^w`.
|
Real.rpow_le_rpow_left_iff
theorem Real.rpow_le_rpow_left_iff : ∀ {x y z : ℝ}, 1 < x → (x ^ y ≤ x ^ z ↔ y ≤ z)
This theorem states that for any real numbers x, y, and z, if x is greater than 1, then x raised to the power of y is less than or equal to x raised to the power of z if and only if y is less than or equal to z. In other words, if we have a real number x that's greater than 1, the function f(n) = x^n is non-decreasing with respect to n.
More concisely: For any real numbers x > 1, x^y <= x^z if and only if y <= z.
|
Real.mul_rpow
theorem Real.mul_rpow : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → (x * y) ^ z = x ^ z * y ^ z
The theorem `Real.mul_rpow` states that for any real numbers `x`, `y`, and `z`, if `x` and `y` are both non-negative, then the `z`th power of the product of `x` and `y` is equal to the product of the `z`th power of `x` and the `z`th power of `y`. In mathematical notation, it says that for all $x, y, z \in \mathbb{R}$ with $x, y \geq 0$, we have $(xy)^z = x^z y^z$.
More concisely: For any non-negative real numbers x, y, and z, $(xy)^z = x^z \cdot y^z$.
|
Real.abs_rpow_le_abs_rpow
theorem Real.abs_rpow_le_abs_rpow : ∀ (x y : ℝ), |x ^ y| ≤ |x| ^ y
This theorem states that for any two real numbers `x` and `y`, the absolute value of `x` raised to the power of `y` is less than or equal to the absolute value of `x` raised to the power of `y`. In LaTeX notation, it can be represented as for all $x, y \in \mathbb{R}$, $|x^y| \leq |x|^y$.
More concisely: For all real numbers x and y, the absolute value of x raised to the power of y is less than or equal to the absolute value of x raised to the power of y (i.e., |x^y| ≤ |x|^y).
|