Power coordinates at a polygonal corner

A holomorphic injection meeting the two rays of a sector of opening β * π, with 0 < β < 2, has a power representation f = h ^ β, where h extends holomorphically across the source boundary and has a simple zero at the prevertex. The sector is centered on the positive real axis; translating the vertex and rotating its bisector gives this normalization for any polygonal corner, including a reentrant corner.

The map I * f ^ (1 / β) straightens the corner to the upper half-plane. Schwarz reflection then supplies a holomorphic injection across the real axis. In particular the nonzero derivative of the corner coordinate is a conclusion, not a boundary regularity assumption. This power coordinate is the input for computing the pre-Schwarzian residue at a prevertex.

References

• L. Ahlfors, Complex Analysis, Ch. 6, Section 2.
• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.

theorem TauCeti.exists_differentiableOn_injOn_cpow_eq_of_sector {Ω : Set ℂ} {f : ℂ → ℂ} {x β : ℝ} (hβ : β ∈ Set.Ioo 0 2) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hx : ↑x ∈ Ω) (hfx : f ↑x = 0) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hsector : ∀ z ∈ Ω, 0 < z.im → |(f z).arg| < β * Real.pi / 2) (hrays : ∀ z ∈ Ω, z.im = 0 → f z ≠ 0 → |(f z).arg| = β * Real.pi / 2) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h Ω ∧ Set.InjOn h Ω ∧ h ↑x = 0 ∧ deriv h ↑x ≠ 0 ∧ Set.EqOn (fun (z : ℂ) => h z ^ ↑β) f (Ω ∩ {z : ℂ | 0 ≤ z.im}) ∧ (∀ z ∈ Ω, 0 < z.im → 0 < (h z).re) ∧ (∀ z ∈ Ω, h ((starRingEnd ℂ) z) = -(starRingEnd ℂ) (h z)) ∧ Set.EqOn h (fun (z : ℂ) => f z ^ ↑β⁻¹) (Ω ∩ {z : ℂ | 0 ≤ z.im})

Power coordinate at a corner. Suppose f is continuous and injective on the closed upper part of a symmetric open set, holomorphic on its open upper part, and takes a real point x to the vertex 0. Its interior values lie strictly between the rays of arguments ± β * π / 2, and its nonzero boundary values lie on those rays. For every opening 0 < β * π < 2 * π, there is an injective holomorphic coordinate h, with a simple zero at x, such that f = h ^ β on the closed upper part. The coordinate has positive real part on the open upper part, fixing the branch of the power. On the closed upper part it equals the principal β-th root of f, and conjugating the source negates the conjugate of the coordinate. In particular, the coordinate is purely imaginary on the real axis.