Straightening a conformal corner

Suppose that, after translation, a conformal map takes the upper half of a neighbourhood of a real point into a sector of opening βπ, centred on the positive real axis. The principal power (f - w) ^ (1 / β) maps that sector into the right half-plane, and multiplication by I maps it into the upper half-plane. If the two boundary sides go to the real axis, Schwarz reflection extends this straightened coordinate holomorphically across the corner. Injectivity makes its zero at the corner simple. Rotating back gives a holomorphic base h with

f = w + h ^ β.

This is the local analytic bridge between polygonal boundary geometry and the corner-power hypothesis used to compute the pre-Schwarzian residue. The second theorem feeds the constructed base directly to that residue theorem.

Main results

• TauCeti.exists_corner_power_of_arg_mem_sector -- Schwarz reflection produces a holomorphic simple-zero base for the corner power.
• TauCeti.tendsto_sub_mul_nhdsNE_of_arg_mem_sector -- a continued pre-Schwarzian 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_corner_power_of_arg_mem_sector {Ω : Set ℂ} {f : ℂ → ℂ} {x : ℝ} {w : ℂ} {β : ℝ} (hΩopen : IsOpen Ω) (hΩconj : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hxΩ : ↑x ∈ Ω) (hβ : β ∈ Set.Ioo 0 2) (hfcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hfd : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (Complex.I * (f z - w) ^ ↑β⁻¹).im = 0) (hfinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hfx : f ↑x = w) (hsector_open : ∀ z ∈ Ω ∩ {z : ℂ | 0 < z.im}, (f z - w).arg ∈ Set.Ioo (-(Real.pi * β / 2)) (Real.pi * β / 2)) : ∃ (h : ℂ → ℂ), DifferentiableOn ℂ h Ω ∧ h ↑x = 0 ∧ deriv h ↑x ≠ 0 ∧ (∀ z ∈ Ω ∩ {z : ℂ | 0 < z.im}, h z ∈ Complex.slitPlane) ∧ Set.EqOn f (fun (z : ℂ) => w + h z ^ ↑β) (Ω ∩ {z : ℂ | 0 < z.im})

Power-map straightening of a conformal corner. Let f be continuous and injective on the closed upper part of a conjugation-symmetric neighbourhood Ω, holomorphic on its open upper part, and send a real point x to the corner w. Assume the translated interior values lie strictly inside the sector of opening βπ, and that the straightened coordinate

I * (f z - w) ^ (1 / β)

is real on the boundary. Then there is a holomorphic function h on Ω, with a simple zero at x, whose values above the axis lie in the slit plane and satisfy f = w + h ^ β.

theorem TauCeti.tendsto_sub_mul_nhdsNE_of_arg_mem_sector {Ω : Set ℂ} {f φ : ℂ → ℂ} {x r : ℝ} {w : ℂ} {β : ℝ} (hΩopen : IsOpen Ω) (hΩconj : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hxΩ : ↑x ∈ Ω) (hβ : β ∈ Set.Ioo 0 2) (hfcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hfd : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (Complex.I * (f z - w) ^ ↑β⁻¹).im = 0) (hfinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hfx : f ↑x = w) (hsector_open : ∀ z ∈ Ω ∩ {z : ℂ | 0 < z.im}, (f z - w).arg ∈ Set.Ioo (-(Real.pi * β / 2)) (Real.pi * β / 2)) (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})) : Filter.Tendsto (fun (z : ℂ) => (z - ↑x) * φ z) (nhdsWithin ↑x {↑x}ᶜ) (nhds (↑β - 1))

The pre-Schwarzian residue after sector straightening. Under the hypotheses of exists_corner_power_of_arg_mem_sector, a conjugation-symmetric holomorphic continuation φ of the pre-Schwarzian derivative has residue β - 1 at the corner.