Principal powers of z - x on the upper half-plane

For a real number x, the difference z - x of an upper-half-plane point and x again has positive imaginary part, hence lies in Complex.slitPlane. The principal power (z - x) ^ (r : ℂ) is therefore holomorphic and nonvanishing there, and its logarithmic derivative is the simple fraction r / (z - x).

Negating the base, replacing z - x by x - z, multiplies the power by the constant exp (π r i) -- unimodular when r is real -- because the two bases lie on opposite sides of the real axis.

Principal powers also commute with division of two upper-half-plane points: their arguments differ by less than π, so their quotient introduces no branch jump.

These are the basic branch facts for a factor of a product of principal powers with real base points, such as the Schwarz--Christoffel integrand.

Main results

• TauCeti.sub_ofReal_mem_slitPlane_of_im_pos
• TauCeti.differentiableAt_sub_cpow_of_im_pos
• TauCeti.sub_cpow_ne_zero_of_im_pos
• TauCeti.sub_cpow_eq_exp_mul_sub_cpow_of_im_pos
• TauCeti.logDeriv_sub_cpow_of_im_pos
• TauCeti.div_cpow_of_im_pos

theorem TauCeti.div_cpow_of_im_pos {x y : ℂ} (hx : 0 < x.im) (hy : 0 < y.im) (r : ℂ) : (x / y) ^ r = x ^ r / y ^ r

Principal complex powers commute with division when both bases have positive imaginary part. Their arguments differ by less than π, so the quotient introduces no branch jump.

theorem TauCeti.sub_ofReal_mem_slitPlane_of_im_pos {z : ℂ} (hz : 0 < z.im) (x : ℝ) : z - ↑x ∈ Complex.slitPlane

Translating a point with positive imaginary part by a real number leaves it in the slit plane.

theorem TauCeti.differentiableAt_sub_cpow_of_im_pos {z : ℂ} (hz : 0 < z.im) (x r : ℝ) : DifferentiableAt ℂ (fun (w : ℂ) => (w - ↑x) ^ ↑r) z

The principal power (z - x) ^ (r : ℂ) with real base point x and real exponent r is differentiable at every point with positive imaginary part.

theorem TauCeti.sub_cpow_ne_zero_of_im_pos {z : ℂ} (hz : 0 < z.im) (x r : ℝ) : (z - ↑x) ^ ↑r ≠ 0

The principal power (z - x) ^ (r : ℂ) with real base point x and real exponent r does not vanish at a point with positive imaginary part.

theorem TauCeti.sub_cpow_eq_exp_mul_sub_cpow_of_im_pos {z : ℂ} (hz : 0 < z.im) (x : ℝ) (r : ℂ) : (z - ↑x) ^ r = Complex.exp (↑Real.pi * r * Complex.I) * (↑x - z) ^ r

Negating the base of a principal power with real base point multiplies it by the factor exp (π r i), unimodular for a real exponent r. At a point with positive imaginary part the two bases z - x and x - z lie on opposite sides of the real axis, so their arguments differ by π and neither meets the branch cut of the other.

theorem TauCeti.logDeriv_sub_cpow_of_im_pos {z : ℂ} (hz : 0 < z.im) (x r : ℝ) : logDeriv (fun (w : ℂ) => (w - ↑x) ^ ↑r) z = ↑r / (z - ↑x)

The logarithmic derivative of w ↦ (w - x) ^ (r : ℂ) at a point with positive imaginary part is the simple fraction r / (z - x).