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.

Equations

• Complex.cpow x y = if x = 0 then if y = 0 then 1 else 0 else Complex.exp (Complex.log x * y)

noncomputable instance Complex.instPowComplex : Pow ℂ ℂ

Equations

• Complex.instPowComplex = { pow := Complex.cpow }

@[simp]

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

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

theorem Complex.cpow_def_of_ne_zero {x : ℂ} (hx : x ≠ 0) (y : ℂ) : x ^ y = Complex.exp (Complex.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

@[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 < (Complex.log x * y).im) (h₂ : (Complex.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⁻¹

@[simp]

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

@[simp]

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

@[simp]

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

theorem Complex.cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) : (x ^ (↑n)⁻¹) ^ n = 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.inv_cpow_eq_ite (x : ℂ) (n : ℂ) : x⁻¹ ^ n = if Complex.arg x = Real.pi then ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

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

theorem Complex.inv_cpow_eq_ite' (x : ℂ) (n : ℂ) : (x ^ n)⁻¹ = if Complex.arg x = 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 Complex.arg x = Real.pi then x ^ n else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)

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

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