Documentation

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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
Instances For
    noncomputable instance Complex.instPow :
    Equations
    @[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 Complex.exp (Complex.log x * y)
    theorem Complex.cpow_def_of_ne_zero {x : } (hx : x 0) (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⁻¹
    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

    See Note [no_index around OfNat.ofNat]

    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

    See Note [no_index around OfNat.ofNat]

    @[simp]
    theorem Complex.cpow_natCast (x : ) (n : ) :
    x ^ n = x ^ n
    @[deprecated Complex.cpow_natCast]
    theorem Complex.cpow_nat_cast (x : ) (n : ) :
    x ^ n = x ^ n

    Alias of Complex.cpow_natCast.

    @[simp]
    theorem Complex.cpow_ofNat (x : ) (n : ) [n.AtLeastTwo] :

    See Note [no_index around OfNat.ofNat]

    theorem Complex.cpow_two (x : ) :
    x ^ 2 = x ^ 2
    @[simp]
    theorem Complex.cpow_intCast (x : ) (n : ) :
    x ^ n = x ^ n
    @[deprecated Complex.cpow_intCast]
    theorem Complex.cpow_int_cast (x : ) (n : ) :
    x ^ n = x ^ n

    Alias of Complex.cpow_intCast.

    @[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] :

    See Note [no_index around OfNat.ofNat]

    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) :
    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.

    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) :
    theorem Complex.cpow_conj (x : ) (n : ) (hx : x.arg Real.pi) :