Complex.cpow_ofNat_inv_pow
theorem Complex.cpow_ofNat_inv_pow :
∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo], (x ^ (OfNat.ofNat n)⁻¹) ^ OfNat.ofNat n = x
The theorem `Complex.cpow_ofNat_inv_pow` asserts that for any complex number `x` and any natural number `n` that is at least two, raising `x` to the power of the reciprocal of `n` (where `n` is treated as a complex number using `OfNat.ofNat`) and then raising the result to the power of `n` (again, treated as a complex number) equals `x`. This essentially states that taking a root and then raising to that power undoes the root-taking operation in the field of complex numbers.
More concisely: For any complex number `x` and natural number `n` greater than or equal to 2, `(x ^ (1 / n)) ^ n = x`.
|
Complex.cpow_zero
theorem Complex.cpow_zero : ∀ (x : ℂ), x ^ 0 = 1
This theorem states that any complex number raised to the power of zero is equal to one. In other words, for all values of `x` in the complex number space ℂ, `x ^ 0` equals 1. This is a fundamental property of exponents, and holds true not just for real numbers, but also for complex numbers in Lean 4.
More concisely: For all complex numbers x in ℂ, x^0 = 1.
|
Complex.cpow_ofNat_mul
theorem Complex.cpow_ofNat_mul :
∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo] (y : ℂ), x ^ (OfNat.ofNat n * y) = (x ^ y) ^ OfNat.ofNat n
This theorem states that for any complex numbers `x` and `y`, and any natural number `n` that is at least two, the power of `x` raised to the product of `n` and `y` is equal to `x` raised to the power of `y`, then all raised to the power of `n`. In mathematical notation, this would be stated as: for all $x, y \in \mathbb{C}$ and $n \in \mathbb{N}$ with $n \geq 2$, we have $(x^{ny}) = ((x^y)^n)$. This theorem essentially establishes a property of exponentiation in the field of complex numbers.
More concisely: For any complex numbers x and y, and natural number n >= 2, (x^(ny)) = (x^y)^n.
|
Complex.cpow_one
theorem Complex.cpow_one : ∀ (x : ℂ), x ^ 1 = x
This theorem states that for any complex number `x`, `x` raised to the power of 1 is equal to `x` itself. It is a basic property of exponentiation that holds true for complex numbers in the field of complex arithmetic.
More concisely: For all complex numbers x, x^1 = x.
|
Complex.one_cpow
theorem Complex.one_cpow : ∀ (x : ℂ), 1 ^ x = 1
This theorem states that for any complex number `x`, the complex number `1` raised to the power of `x` is always equal to `1`. This corresponds to the mathematical statement $1^x = 1$ for all $x \in \mathbb{C}$.
More concisely: For all complex numbers x, 1 raised to the power x equals 1. (Or equivalently, the complex number 1 is its own complex exponent.)
|
Complex.sq_cpow_two_inv
theorem Complex.sq_cpow_two_inv : ∀ {x : ℂ}, 0 < x.re → (x ^ 2) ^ 2⁻¹ = x
This theorem, `Complex.sq_cpow_two_inv`, states that for all complex numbers `x` where the real part is greater than zero, (i.e., `0 < x.re`), the square of `x` raised to the power of the reciprocal of two (i.e., `(x ^ 2) ^ 2⁻¹`) is equal to `x` itself. The theorem also refers to another theorem `Complex.pow_cpow_ofNat_inv` that carries similar assertions but also works for `x * I` where `0 ≤ x`.
More concisely: For complex numbers `x` with a positive real part (`0 < x.re`), the equality `(x ^ 2) ^ (-1) = x` holds.
|
Complex.cpow_int_mul'
theorem Complex.cpow_int_mul' :
∀ {x : ℂ} {n : ℤ}, -Real.pi < ↑n * x.arg → ↑n * x.arg ≤ Real.pi → ∀ (y : ℂ), x ^ (↑n * y) = (x ^ n) ^ y
The theorem `Complex.cpow_int_mul'` states that for any complex number `x`, any integer `n`, and any complex number `y`, given that the argument of the complex number `x` multiplied by `n` is greater than `-π` and less than or equal to `π`, the complex power of `x` raised to the product of `n` and `y` is equal to `x` raised to the power of `n` and then the result raised to the power of `y`. However, this equality doesn't hold for all values of `x`, `n`, and `y`. For example, if `x` is the imaginary unit `-i`, `n` equals 2, and `y` equals 1/2, the equality fails.
More concisely: If the argument of the complex number $x$ raised to the power of $n$ is bounded between $-\pi$ and $\pi$, then $(x^n)^y = x^{ny}$. (This does not hold for all values of $x$, $n$, and $y$.)
|
Complex.cpow_add
theorem Complex.cpow_add : ∀ {x : ℂ} (y z : ℂ), x ≠ 0 → x ^ (y + z) = x ^ y * x ^ z
This theorem states that for all complex numbers `x`, `y`, and `z`, where `x` is not equal to zero, the property of exponentiation distributes over addition. In other words, raising `x` to the power of `(y + z)` is the same as raising `x` to the power of `y` and `z` separately, and then multiplying the results together. This is the complex number equivalent of the exponentiation rule `a^(b + c) = a^b * a^c` for real numbers.
More concisely: For complex numbers `x` neither equal to zero, `x^(y + z) = x^y * x^z`.
|
Complex.cpow_ofNat
theorem Complex.cpow_ofNat : ∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
The theorem `Complex.cpow_ofNat` states that for any given complex number `x` and a natural number `n` which is at least two, the expression `x ^ OfNat.ofNat n` remains invariant. In simpler terms, it says that if you raise a complex number to the power of a natural number (which has been transformed by the function `OfNat.ofNat`), it does not change the value of the expression. Do note that the function `OfNat.ofNat` is automatically inserted by the parser when a numeric literal is written and its function can be customized based on `n` and `α`.
More concisely: For any complex number `x` and natural number `n` ≥ 2, `x ^ OfNat.ofNat n` is equal to `x ^ n`.
|
Complex.mul_cpow_ofReal_nonneg
theorem Complex.mul_cpow_ofReal_nonneg : ∀ {a b : ℝ}, 0 ≤ a → 0 ≤ b → ∀ (r : ℂ), (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r := by
sorry
This theorem states that for all real numbers `a` and `b` that are nonnegative (i.e., `a` and `b` are greater than or equal to zero), and for any complex number `r`, the complex power of the product of `a` and `b` is equal to the product of the complex powers of `a` and `b`. In other words, `(a * b) ^ r = a ^ r * b ^ r` where the operations are performed in the complex field. This theorem generalizes a familiar property of exponents in the field of real numbers to the field of complex numbers.
More concisely: For all nonnegative real numbers `a` and `b` and any complex number `r`, `(a * b) ^ r = a ^ r * b ^ r`.
|
Complex.cpow_mul_ofNat
theorem Complex.cpow_mul_ofNat :
∀ (x y : ℂ) (n : ℕ) [inst : n.AtLeastTwo], x ^ (y * OfNat.ofNat n) = (x ^ y) ^ OfNat.ofNat n
The theorem `Complex.cpow_mul_ofNat` states that for any two complex numbers `x` and `y`, and any natural number `n` that is at least two, the power of `x` raised to the product of `y` and `n` (where `n` is converted to the appropriate type using the `OfNat.ofNat` function) is equal to the power of `x` raised to `y`, all raised to `n`. In other words, it asserts the equation \(x^{(y \cdot n)} = (x^y)^n\) holds in the complex number system, where the exponentiation is the complex power function (`cpow`).
More concisely: For any complex numbers x and y, and natural number n ≥ 2, the equation x^(y * n) = (x^y)^n holds.
|
Complex.cpow_def_of_ne_zero
theorem Complex.cpow_def_of_ne_zero : ∀ {x : ℂ}, x ≠ 0 → ∀ (y : ℂ), x ^ y = (x.log * y).exp
This theorem states that for any non-zero complex number `x` and any complex number `y`, the power of `x` raised to `y` is equivalent to the complex exponential of the product of the complex logarithm of `x` and `y`. In mathematical notation, this is commonly expressed as \(x^y = e^{(\log x) \cdot y}\) for all \(x \neq 0\). The logarithm and exponential functions used here are complex logarithm and complex exponential functions.
More concisely: For any non-zero complex number `x`, the power `x^y` equals the complex exponential `exp(y * log x)`.
|
Complex.cpow_mul
theorem Complex.cpow_mul :
∀ {x y : ℂ} (z : ℂ), -Real.pi < (x.log * y).im → (x.log * y).im ≤ Real.pi → x ^ (y * z) = (x ^ y) ^ z
The theorem `Complex.cpow_mul` states that for any complex numbers `x`, `y`, and `z`, if the imaginary part of the product of the complex logarithm of `x` and `y` is greater than `-π` and less or equal to `π`, then the power of `x` raised to the product of `y` and `z` is equal to the power of `x` raised to `y` raised to `z`. In other words, `(x^(y*z)) = ((x^y)^z)`, given the specified conditions on the imaginary part of `log(x) * y`.
More concisely: If the imaginary part of the complex logarithm of complex numbers x and y satisfies the condition -π < Im(log(x) * y) <= π, then x^(y*z) = (x^y)^z.
|
Complex.zero_cpow
theorem Complex.zero_cpow : ∀ {x : ℂ}, x ≠ 0 → 0 ^ x = 0
This theorem states that for any non-zero complex number `x`, the result of raising zero to the power of `x` is zero. In mathematical terms, if `x` is a complex number and `x ≠ 0`, then `0 ^ x = 0`.
More concisely: For any non-zero complex number `x`, `0 ^ x = 0`.
|
Complex.cpow_eq_zero_iff
theorem Complex.cpow_eq_zero_iff : ∀ (x y : ℂ), x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
This theorem in complex analysis states that for any two complex numbers `x` and `y`, `x` raised to the power `y` equals zero if and only if `x` equals zero and `y` is not equal to zero. In other words, the only way a complex number raised to the power of another complex number can result in zero is if the base number is zero and the exponent is a non-zero number. This theorem relates the conditions under which a power operation with complex numbers yields zero.
More concisely: For complex numbers x and y, x^y = 0 if and only if x = 0 and y ≠ 0.
|
Complex.cpow_nat_mul'
theorem Complex.cpow_nat_mul' :
∀ {x : ℂ} {n : ℕ}, -Real.pi < ↑n * x.arg → ↑n * x.arg ≤ Real.pi → ∀ (y : ℂ), x ^ (↑n * y) = (x ^ n) ^ y
This theorem states that for any complex number `x` and any natural number `n`, if the product of `n` and the argument of `x` is strictly greater than `-π` and less than or equal to `π`, then for any other complex number `y`, the expression `x` raised to the power of the product of `n` and `y` is equal to `x` raised to the power of `n`, which is then raised to the power of `y`. However, this theorem requires specific constraints on the arguments because the equality does not hold for all values. For example, it fails when `x` equals `-I`, `n` equals `2`, and `y` equals `1/2`.
More concisely: For complex numbers `x` and natural number `n`, if the argument of `x` times `n` lies between `-π` and `π`, then `x^(n*y)` equals `(x^n)^y`.
|
Complex.cpow_neg
theorem Complex.cpow_neg : ∀ (x y : ℂ), x ^ (-y) = (x ^ y)⁻¹
This theorem states that for all complex numbers 'x' and 'y', the power of 'x' to the negative 'y' is equal to the inverse of 'x' to the power of 'y'. In other words, it stipulates the property for complex numbers that the power of a number to a negative exponent is the reciprocal of the power to the positive exponent.
More concisely: For all complex numbers x and y, x^(-y) = 1 / x^y.
|
Complex.cpow_int_mul
theorem Complex.cpow_int_mul : ∀ (x : ℂ) (n : ℤ) (y : ℂ), x ^ (↑n * y) = (x ^ y) ^ n
This theorem, `Complex.cpow_int_mul`, states that for any three complex numbers `x`, `n`, and `y`, where `n` is actually an integer cast to a complex number, the exponentiation `x` raised to the power of (`n` multiplied by `y`) is equal to `x` raised to the power of `y` and the result again raised to the power of `n`. In mathematical terms, it states that \(x^{(n \cdot y)} = (x^y)^n\).
More concisely: The theorem asserts that for any complex number x and integers n and y, x^(ny) = (x^y)^n.
|
Complex.inv_cpow_eq_ite'
theorem Complex.inv_cpow_eq_ite' :
∀ (x n : ℂ), (x ^ n)⁻¹ = if x.arg = Real.pi then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n
The theorem `Complex.inv_cpow_eq_ite'` states that for any complex numbers `x` and `n`, the inverse of `x` raised to the power `n`, denoted as `(x ^ n)⁻¹`, is equal to a condition-dependent expression. If the argument of `x` equals the real number π, then the value is given by applying `starRingEnd ℂ` (which is the complex conjugate operation) to `x⁻¹` raised to the power `starRingEnd ℂ n` (which is the complex conjugate of `n`). Otherwise, the value is simply `x⁻¹` raised to the power `n`.
More concisely: For complex numbers `x` and natural number `n`, `(x ^ n)⁻¹` equals `x⁻¹` raised to the power `n` if the argument of `x` is not equal to π, and equals the complex conjugate of `x⁻¹` raised to the power of the complex conjugate of `n` otherwise.
|
Complex.cpow_nat_mul
theorem Complex.cpow_nat_mul : ∀ (x : ℂ) (n : ℕ) (y : ℂ), x ^ (↑n * y) = (x ^ y) ^ n
This theorem states that for any complex number `x`, natural number `n`, and complex number `y`, the power of `x` raised to the product of `n` and `y` is equal to the power of `x` raised to `y` all raised to the power of `n`. In mathematical terms, it's stating that `x^(n*y) = (x^y)^n` for complex numbers `x` and `y`, and natural number `n`.
More concisely: For complex numbers `x` and natural number `n`, `x^(n*y) = (x^y)^n`.
|