mathlib3 documentation

analysis.special_functions.pow.complex

Power function on ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
source
@[protected, instance]
noncomputable def complex.has_pow  :
has_pow ℂ ℂ
Equations
source
@[simp]
theorem complex.cpow_eq_pow (x y : ℂ) :
x.cpow y = x ^ y
source
theorem complex.cpow_def (x y : ℂ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (cexp (complex.log x * y))
source
theorem complex.cpow_def_of_ne_zero {x : ℂ} (hx : x ≠ 0) (y : ℂ) :
x ^ y = cexp (complex.log x * y)
source
@[simp]
theorem complex.cpow_zero (x : ℂ) :
x ^ 0 = 1
source
@[simp]
theorem complex.cpow_eq_zero_iff (x y : ℂ) :
x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
source
@[simp]
theorem complex.zero_cpow {x : ℂ} (h : x ≠ 0) :
0 ^ x = 0
source
theorem complex.zero_cpow_eq_iff {x a : ℂ} :
0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
theorem complex.eq_zero_cpow_iff {x a : ℂ} :
a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
@[simp]
theorem complex.cpow_one (x : ℂ) :
x ^ 1 = x
source
@[simp]
theorem complex.one_cpow (x : ℂ) :
1 ^ x = 1
source
theorem complex.cpow_add {x : ℂ} (y z : ℂ) (hx : x ≠ 0) :
x ^ (y + z) = x ^ y * x ^ z
source
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
source
theorem complex.cpow_neg (x y : ℂ) :
x ^ -y = (x ^ y)⁻¹
source
theorem complex.cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem complex.cpow_neg_one (x : ℂ) :
x ^ -1 = x⁻¹
source
@[simp, norm_cast]
theorem complex.cpow_nat_cast (x : ℂ) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem complex.cpow_two (x : ℂ) :
x ^ 2 = x ^ 2
source
@[simp, norm_cast]
theorem complex.cpow_int_cast (x : ℂ) (n : ℤ) :
x ^ ↑n = x ^ n
source
theorem complex.cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem complex.mul_cpow_of_real_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) :
(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
source
theorem complex.inv_cpow_eq_ite (x n : ℂ) :
x⁻¹ ^ n = ite (x.arg = real.pi) (⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n)⁻¹) (x ^ n)⁻¹
source
theorem complex.inv_cpow (x n : ℂ) (hx : x.arg ≠ real.pi) :
x⁻¹ ^ n = (x ^ n)⁻¹
source
theorem complex.inv_cpow_eq_ite' (x n : ℂ) :
(x ^ n)⁻¹ = ite (x.arg = real.pi) (⇑(star_ring_end ℂ) (x⁻¹ ^ ⇑(star_ring_end ℂ) n)) (x⁻¹ ^ n)

complex.inv_cpow_eq_ite with the ite on the other side.

source
theorem complex.conj_cpow_eq_ite (x n : ℂ) :
⇑(star_ring_end ℂ) x ^ n = ite (x.arg = real.pi) (x ^ n) (⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n))
source
theorem complex.conj_cpow (x n : ℂ) (hx : x.arg ≠ real.pi) :
⇑(star_ring_end ℂ) x ^ n = ⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n)
source
theorem complex.cpow_conj (x n : ℂ) (hx : x.arg ≠ real.pi) :
x ^ ⇑(star_ring_end ℂ) n = ⇑(star_ring_end ℂ) (⇑(star_ring_end ℂ) x ^ n)

Tactic extensions for complex powers #

source
theorem norm_num.cpow_pos (a b : ℂ) (b' : ℕ) (c : ℂ) (hb : b = ↑b') (h : a ^ b' = c) :
a ^ b = c
source
theorem norm_num.cpow_neg (a b : ℂ) (b' : ℕ) (c c' : ℂ) (hb : b = ↑b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
source
meta def norm_num.prove_rpow' (pos neg zero : name) (α β one a b : expr) :
tactic (expr × expr)

Generalized version of prove_cpow, prove_nnrpow, prove_ennrpow.

source
meta def norm_num.prove_cpow  :
expr → expr → tactic (expr × expr)

Evaluate complex.cpow a b where a is a rational numeral and b is an integer.

source
meta def norm_num.eval_cpow  :
expr → tactic (expr × expr)

Evaluates expressions of the form cpow a b and a ^ b in the special case where b is an integer and a is a positive rational (so it's really just a rational power).