Power function on ℂ

We construct the power functions x ^ y, where x and y are complex numbers.

noncomputable def Complex.cpow (x y : ℂ) : ℂ

The complex power function x ^ y, given by x ^ y = exp(y log x) (where log is the principal determination of the logarithm), unless x = 0 where one sets 0 ^ 0 = 1 and 0 ^ y = 0 for y ≠ 0.

@[implicit_reducible]

noncomputable instance Complex.instPow : Pow ℂ ℂ

@[simp]

theorem Complex.cpow_eq_pow (x y : ℂ) : x.cpow y = x ^ y

theorem Complex.cpow_def (x y : ℂ) : x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)

theorem Complex.cpow_def_of_ne_zero {x : ℂ} (hx : x ≠ 0) (y : ℂ) : x ^ y = exp (log x * y)

@[simp]

theorem Complex.cpow_zero (x : ℂ) : x ^ 0 = 1

@[simp]

theorem Complex.cpow_eq_zero_iff (x y : ℂ) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

theorem Complex.cpow_ne_zero_iff {x y : ℂ} : x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0

theorem Complex.cpow_ne_zero_iff_of_exponent_ne_zero {x y : ℂ} (hy : y ≠ 0) : x ^ y ≠ 0 ↔ x ≠ 0

@[simp]

theorem Complex.zero_cpow {x : ℂ} (h : x ≠ 0) : 0 ^ x = 0

theorem Complex.zero_cpow_eq_iff {x a : ℂ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

theorem Complex.eq_zero_cpow_iff {x a : ℂ} : a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

@[simp]

theorem Complex.cpow_one (x : ℂ) : x ^ 1 = x

@[simp]

theorem Complex.one_cpow (x : ℂ) : 1 ^ x = 1

theorem Complex.cpow_add {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y + z) = x ^ y * x ^ z

theorem Complex.cpow_mul {x y : ℂ} (z : ℂ) (h₁ : -Real.pi < (log x * y).im) (h₂ : (log x * y).im ≤ Real.pi) : x ^ (y * z) = (x ^ y) ^ z

theorem Complex.cpow_neg (x y : ℂ) : x ^ (-y) = (x ^ y)⁻¹

theorem Complex.cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y - z) = x ^ y / x ^ z

theorem Complex.cpow_neg_one (x : ℂ) : x ^ (-1) = x⁻¹

theorem Complex.cpow_int_mul (x : ℂ) (n : ℤ) (y : ℂ) : x ^ (↑n * y) = (x ^ y) ^ n

See also Complex.cpow_int_mul'.

theorem Complex.cpow_mul_int (x y : ℂ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n

theorem Complex.cpow_nat_mul (x : ℂ) (n : ℕ) (y : ℂ) : x ^ (↑n * y) = (x ^ y) ^ n

theorem Complex.cpow_ofNat_mul (x : ℂ) (n : ℕ) [n.AtLeastTwo] (y : ℂ) : x ^ (OfNat.ofNat n * y) = (x ^ y) ^ OfNat.ofNat n

theorem Complex.cpow_mul_nat (x y : ℂ) (n : ℕ) : x ^ (y * ↑n) = (x ^ y) ^ n

theorem Complex.cpow_mul_ofNat (x y : ℂ) (n : ℕ) [n.AtLeastTwo] : x ^ (y * OfNat.ofNat n) = (x ^ y) ^ OfNat.ofNat n

@[simp]

theorem Complex.cpow_natCast (x : ℂ) (n : ℕ) : x ^ ↑n = x ^ n

@[simp]

theorem Complex.cpow_ofNat (x : ℂ) (n : ℕ) [n.AtLeastTwo] : x ^ OfNat.ofNat n = x ^ OfNat.ofNat n

theorem Complex.cpow_two (x : ℂ) : x ^ 2 = x ^ 2

@[simp]

theorem Complex.cpow_intCast (x : ℂ) (n : ℤ) : x ^ ↑n = x ^ n

@[simp]

theorem Complex.cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : (x ^ (↑n)⁻¹) ^ n = x

@[simp]

theorem Complex.cpow_ofNat_inv_pow (x : ℂ) (n : ℕ) [n.AtLeastTwo] : (x ^ (OfNat.ofNat n)⁻¹) ^ OfNat.ofNat n = x

theorem Complex.cpow_int_mul' {x : ℂ} {n : ℤ} (hlt : -Real.pi < ↑n * x.arg) (hle : ↑n * x.arg ≤ Real.pi) (y : ℂ) : x ^ (↑n * y) = (x ^ n) ^ y

A version of Complex.cpow_int_mul with RHS that matches Complex.cpow_mul.

The assumptions on the arguments are needed because the equality fails, e.g., for x = -I, n = 2, y = 1/2.

theorem Complex.cpow_nat_mul' {x : ℂ} {n : ℕ} (hlt : -Real.pi < ↑n * x.arg) (hle : ↑n * x.arg ≤ Real.pi) (y : ℂ) : x ^ (↑n * y) = (x ^ n) ^ y

A version of Complex.cpow_nat_mul with RHS that matches Complex.cpow_mul.

The assumptions on the arguments are needed because the equality fails, e.g., for x = -I, n = 2, y = 1/2.

theorem Complex.cpow_ofNat_mul' {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -Real.pi < OfNat.ofNat n * x.arg) (hle : OfNat.ofNat n * x.arg ≤ Real.pi) (y : ℂ) : x ^ (OfNat.ofNat n * y) = (x ^ OfNat.ofNat n) ^ y

theorem Complex.pow_cpow_nat_inv {x : ℂ} {n : ℕ} (h₀ : n ≠ 0) (hlt : -(Real.pi / ↑n) < x.arg) (hle : x.arg ≤ Real.pi / ↑n) : (x ^ n) ^ (↑n)⁻¹ = x

theorem Complex.pow_cpow_ofNat_inv {x : ℂ} {n : ℕ} [n.AtLeastTwo] (hlt : -(Real.pi / OfNat.ofNat n) < x.arg) (hle : x.arg ≤ Real.pi / OfNat.ofNat n) : (x ^ OfNat.ofNat n) ^ (OfNat.ofNat n)⁻¹ = x

theorem Complex.sq_cpow_two_inv {x : ℂ} (hx : 0 < x.re) : (x ^ 2) ^ 2⁻¹ = x

See also Complex.pow_cpow_ofNat_inv for a version that also works for x * I, 0 ≤ x.

@[simp]

theorem Complex.isSquare (x : ℂ) : IsSquare x

theorem Complex.mul_cpow_ofReal_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) : (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

theorem Complex.natCast_mul_natCast_cpow (m n : ℕ) (s : ℂ) : (↑m * ↑n) ^ s = ↑m ^ s * ↑n ^ s

theorem Complex.natCast_cpow_natCast_mul (n m : ℕ) (z : ℂ) : ↑n ^ (↑m * z) = (↑n ^ m) ^ z

theorem Complex.inv_cpow_eq_ite (x n : ℂ) : x⁻¹ ^ n = if x.arg = Real.pi then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

theorem Complex.inv_cpow (x n : ℂ) (hx : x.arg ≠ Real.pi) : x⁻¹ ^ n = (x ^ n)⁻¹

theorem Complex.inv_cpow_eq_ite' (x n : ℂ) : (x ^ n)⁻¹ = if x.arg = Real.pi then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n

Complex.inv_cpow_eq_ite with the ite on the other side.

theorem Complex.conj_cpow_eq_ite (x n : ℂ) : (starRingEnd ℂ) x ^ n = if x.arg = Real.pi then x ^ n else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

theorem Complex.conj_cpow (x n : ℂ) (hx : x.arg ≠ Real.pi) : (starRingEnd ℂ) x ^ n = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

theorem Complex.cpow_conj (x n : ℂ) (hx : x.arg ≠ Real.pi) : x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) x ^ n)

theorem Complex.natCast_add_one_cpow_ne_zero (n : ℕ) (z : ℂ) : (↑n + 1) ^ z ≠ 0