Principal complex powers: scaling, sector inversion, and holomorphic products

Multiplication of a complex number by a nonnegative real scalar is compatible with principal complex powers. Away from zero, this follows because positive scaling does not cross the branch cut of the principal logarithm; the zero cases follow from the totalized definition of cpow.

Taking the principal power u ^ (r⁻¹ : ℝ) of a nonzero u divides its argument by r, so raising the result back to the power r returns u — but only as long as the intermediate argument stays inside the principal range (-π, π], which is where Complex.cpow_mul may be applied. For a positive real exponent r that range is reached exactly on the sector -(r * π) < arg u ≤ r * π.

Products ∏ i, (1 - a i * w) ^ e i are holomorphic near zero, with derivative -∑ i, e i * a i and second derivative (∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2 at zero. The quadratic difference quotient tends to half that second derivative. These coefficients describe the integrand of a Schwarz--Christoffel map in the reciprocal coordinate at infinity.

Main results

• TauCeti.ofReal_mul_cpow -- a principal power splits across a nonnegative real factor.
• TauCeti.ofReal_pow_cpow -- a principal power of a natural power of a nonnegative real multiplies the exponents.
• TauCeti.cpow_sum -- a principal power of a finite sum splits into a product for a nonzero complex base.
• TauCeti.ofReal_exp_cpow -- a principal power of a positive real exponential is an exponential.
• TauCeti.cpow_inv_cpow_of_arg_mem_Ioc -- raising an inverse principal power recovers its base on a suitable sector.

theorem TauCeti.ofReal_mul_cpow {r : ℝ} (hr : 0 ≤ r) (z w : ℂ) : (↑r * z) ^ w = ↑r ^ w * z ^ w

A principal complex power splits across multiplication by a nonnegative real scalar: ((r : ℂ) * z) ^ w = (r : ℂ) ^ w * z ^ w for all complex z and w, without a branch hypothesis on z. This generalizes Complex.mul_cpow_ofReal_nonneg to a complex second factor; the proof follows Mathlib's.

theorem TauCeti.ofReal_pow_cpow {r : ℝ} (hr : 0 ≤ r) (n : ℕ) (s : ℂ) : (↑r ^ n) ^ s = ↑r ^ (↑n * s)

A principal complex power of a natural power of a nonnegative real multiplies the exponents: ((r : ℂ) ^ n) ^ s = (r : ℂ) ^ (n * s). The argument of (r : ℂ) is 0, so the principal branch is not crossed.

theorem TauCeti.cpow_sum {ι : Type u_1} {x : ℂ} (hx : x ≠ 0) (f : ι → ℂ) (s : Finset ι) : x ^ ∑ i ∈ s, f i = ∏ i ∈ s, x ^ f i

A principal complex power with nonzero base takes a finite sum of exponents to the corresponding product.

theorem TauCeti.ofReal_exp_cpow (t : ℝ) (s : ℂ) : ↑(Real.exp t) ^ s = Complex.exp (↑t * s)

A principal complex power of the positive real Real.exp t is exp (t * s): the principal logarithm of Real.exp t is t.

theorem TauCeti.cpow_inv_cpow_of_arg_mem_Ioc {u : ℂ} {r : ℝ} (hr : 0 < r) (harg : u.arg ∈ Set.Ioc (-(r * Real.pi)) (r * Real.pi)) : (u ^ ↑r⁻¹) ^ ↑r = u

The principal power u ^ (r⁻¹ : ℝ) raised to the real power r is again u, for a positive r and a base whose argument lies in the sector (-(r * π), r * π]. The intermediate argument arg u / r then lies in (-π, π], so the principal branch is not crossed.

theorem TauCeti.analyticAt_prod_one_sub_mul_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℂ) : AnalyticAt ℂ (fun (w : ℂ) => ∏ i : ι, (1 - a i * w) ^ e i) 0

The reciprocal-coordinate product of principal powers is holomorphic at zero, where every base equals one.

theorem TauCeti.hasDerivAt_prod_one_sub_mul_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℂ) : HasDerivAt (fun (w : ℂ) => ∏ i : ι, (1 - a i * w) ^ e i) (-∑ i : ι, e i * a i) 0

The derivative at zero of the reciprocal-coordinate product is the negative weighted sum of its coefficients.

theorem TauCeti.hasDerivAt_deriv_prod_one_sub_mul_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℂ) : HasDerivAt (deriv fun (w : ℂ) => ∏ i : ι, (1 - a i * w) ^ e i) ((∑ i : ι, e i * a i) ^ 2 - ∑ i : ι, e i * a i ^ 2) 0

The second derivative at zero of a product of principal powers. The coefficients and exponents may be complex; no branch assumptions are needed at zero, where each base is one.

theorem TauCeti.tendsto_prod_one_sub_mul_cpow_sub_linear_div_sq {ι : Type u_1} [Fintype ι] (a e : ι → ℂ) : Filter.Tendsto (fun (w : ℂ) => (∏ i : ι, (1 - a i * w) ^ e i - 1 + (∑ i : ι, e i * a i) * w) / w ^ 2) (nhdsWithin 0 {0}ᶜ) (nhds (((∑ i : ι, e i * a i) ^ 2 - ∑ i : ι, e i * a i ^ 2) / 2))

The quadratic coefficient in the product of principal powers, expressed as a second-order difference quotient. The limit is taken in the whole complex plane.