Power normalization of a conformal corner

A conformal map meeting two straight boundary edges at an angle βπ can be straightened by the power z ↦ z ^ (1 / β). For a convex corner, 0 < β ≤ 1, the normalized corner lies in the closed upper half-plane, so the principal power is continuous up to both edges. It maps the open corner to the upper half-plane and both edges to the real axis. Schwarz reflection therefore extends it through the prevertex.

This file proves that the reflected power coordinate is holomorphic and injective, vanishes simply at the prevertex, and recovers the original map in the corner-power form w + h ^ β. The simple-zero coordinate is the local input used to compute the pre-Schwarzian residue at a Schwarz--Christoffel prevertex.

Main result

• TauCeti.exists_differentiableOn_injOn_eqOn_add_cpow_of_convex_corner -- a conformal convex corner admits a holomorphic simple-zero power coordinate across its prevertex.
• TauCeti.tendsto_sub_mul_nhdsNE_of_convex_corner -- the continued pre-Schwarzian derivative has residue β - 1 at such a corner.

References

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

theorem TauCeti.exists_differentiableOn_injOn_eqOn_add_cpow_of_convex_corner {f : ℂ → ℂ} {Ω : Set ℂ} {x : ℝ} {w : ℂ} {β : ℝ} (hβ : 0 < β) (hβ1 : β ≤ 1) (hΩopen : IsOpen Ω) (hΩconj : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hxΩ : ↑x ∈ Ω) (hfx : f ↑x = w) (hinterior : ∀ z ∈ Ω ∩ {z : ℂ | 0 < z.im}, (f z - w).arg ∈ Set.Ioo 0 (β * Real.pi)) (hedges : ∀ z ∈ Ω, z.im = 0 → (f z - w).arg = 0 ∨ (f z - w).arg = β * Real.pi) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h Ω ∧ Set.InjOn h Ω ∧ h ↑x = 0 ∧ deriv h ↑x ≠ 0 ∧ Set.MapsTo h (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im} ∧ Set.EqOn f (fun (z : ℂ) => w + h z ^ ↑β) (Ω ∩ {z : ℂ | 0 < z.im})

A convex conformal corner has a holomorphic simple-zero power coordinate.

Let f be continuous and injective on the closed upper part of a conjugation-symmetric open set and holomorphic on its open upper part. Suppose f x = w at a real boundary point and f - w lies in the closed sector from angle 0 to angle βπ, taking interior points to the open sector and boundary points to one of its two rays. If 0 < β ≤ 1, then the principal power (f - w) ^ (1 / β) straightens the sector to the upper half-plane. Its Schwarz reflection is a holomorphic injection h through x, has a simple zero there, and satisfies f = w + h ^ β on the open upper part.

The bound β ≤ 1 is the convex-corner condition. It ensures that the original sector is contained in the closed upper half-plane, including the one-sided principal-power continuity on its second edge.

theorem TauCeti.tendsto_sub_mul_nhdsNE_of_convex_corner {φ f : ℂ → ℂ} {Ω : Set ℂ} {x r β : ℝ} {w : ℂ} (hr : 0 < r) (hφ : DifferentiableOn ℂ φ (Metric.ball (↑x) r \ {↑x})) (hφconj : ∀ z ∈ Metric.ball (↑x) r \ {↑x}, φ ((starRingEnd ℂ) z) = (starRingEnd ℂ) (φ z)) (hφf : Set.EqOn φ (logDeriv (deriv f)) ({z : ℂ | 0 < z.im} ∩ Ω)) (hβ : 0 < β) (hβ1 : β ≤ 1) (hΩopen : IsOpen Ω) (hΩconj : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hxΩ : ↑x ∈ Ω) (hfx : f ↑x = w) (hinterior : ∀ z ∈ Ω ∩ {z : ℂ | 0 < z.im}, (f z - w).arg ∈ Set.Ioo 0 (β * Real.pi)) (hedges : ∀ z ∈ Ω, z.im = 0 → (f z - w).arg = 0 ∨ (f z - w).arg = β * Real.pi) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : Filter.Tendsto (fun (z : ℂ) => (z - ↑x) * φ z) (nhdsWithin ↑x {↑x}ᶜ) (nhds (↑β - 1))

The pre-Schwarzian residue at a convex conformal corner. Under the geometric sector hypotheses of TauCeti.exists_differentiableOn_injOn_eqOn_add_cpow_of_convex_corner, a conjugation-symmetric holomorphic continuation φ of the pre-Schwarzian derivative has residue β - 1 at the prevertex. This discharges the abstract corner-power-coordinate hypotheses of TauCeti.tendsto_sub_mul_nhdsNE_of_eqOn_add_cpow.