The prevertex residues of the pre-Schwarzian derivative

A conformal map of the upper half-plane onto a polygon is holomorphic across each open boundary interval between two consecutive prevertices, and its pre-Schwarzian derivative logDeriv (deriv f) = f'' / f' continues across those intervals to a conjugation-symmetric function φ holomorphic off the prevertices. This file computes the residue of φ at a prevertex and turns the resulting partial-fraction expansion into the Schwarz--Christoffel formula.

At a prevertex the map has a corner power form: f = w + h ^ β near the prevertex inside the upper half-plane, for a holomorphic h with a simple zero there, where β is the interior angle divided by π. The pre-Schwarzian derivative of such an f has residue asymptotic (z - x) * f''(z) / f'(z) → β - 1 from above, and conjugation symmetry propagates that asymptotic to the punctured neighbourhood, so β - 1 is the residue of φ at the prevertex. Once each prevertex contributes its residue and φ decays at infinity, partial fractions identify φ with ∑ i, e i / (z - a i) and the integration theorem identifies f itself with an affine image of the Schwarz--Christoffel primitive.

Main results

• TauCeti.tendsto_sub_mul_nhdsNE_of_eqOn_add_cpow -- the continuation of the pre-Schwarzian derivative of a map with a corner power form has residue asymptotic β - 1 at the corner.
• TauCeti.tendsto_sub_mul_nhdsNE_of_sector -- the same residue, derived from the geometric sector and boundary-ray conditions at a polygonal corner.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_tendsto -- a map of the upper half-plane whose pre-Schwarzian derivative continues with at most simple poles of residues e i at the prevertices a i and decays at infinity is an affine image of the Schwarz--Christoffel primitive for those data.

References

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

The residue at a single corner

theorem TauCeti.tendsto_sub_mul_nhdsNE_of_eqOn_add_cpow {φ f h : ℂ → ℂ} {x r : ℝ} {U : Set ℂ} {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)) (UpperHalfPlane.upperHalfPlaneSet ∩ U)) (hU : IsOpen U) (hxU : ↑x ∈ U) (hh : DifferentiableOn ℂ h U) (hhx : h ↑x = 0) (hdh : deriv h ↑x ≠ 0) (hslit : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet ∩ U, h z ∈ Complex.slitPlane) (hβ : β ≠ 0) (hf : Set.EqOn f (fun (z : ℂ) => w + h z ^ β) (UpperHalfPlane.upperHalfPlaneSet ∩ U)) : Filter.Tendsto (fun (z : ℂ) => (z - ↑x) * φ z) (nhdsWithin ↑x {↑x}ᶜ) (nhds (β - 1))

The pre-Schwarzian derivative has residue asymptotic β - 1 at a corner. Let φ be holomorphic on a punctured disc about a real point x, symmetric under conjugation, and agree with the pre-Schwarzian derivative of f above the axis near x. If f has the corner power form w + h ^ β there, with h holomorphic and having a simple zero at x, then (z - x) * φ z tends to β - 1 as z tends to x from any direction.

theorem TauCeti.tendsto_sub_mul_nhdsNE_of_sector {φ f : ℂ → ℂ} {x r β : ℝ} {Ω : Set ℂ} {b : ℂ} (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)) (UpperHalfPlane.upperHalfPlaneSet ∩ Ω)) (hβ : β ∈ Set.Ioo 0 2) (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hx : ↑x ∈ Ω) (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 - f ↑x) / b).arg| < β * Real.pi / 2) (hrays : ∀ z ∈ Ω, z.im = 0 → f z ≠ f ↑x → |((f z - f ↑x) / b).arg| = β * Real.pi / 2) : Filter.Tendsto (fun (z : ℂ) => (z - ↑x) * φ z) (nhdsWithin ↑x {↑x}ᶜ) (nhds (↑β - 1))

The pre-Schwarzian residue at a polygonal corner is its normalized angle minus one. After translating the vertex f x and rotating and scaling by b, suppose a holomorphic map is continuous and injective on the closed upper part of a conjugation-symmetric open neighborhood Ω of x. Suppose it takes the open upper part into the sector |arg w| < β * π / 2, with boundary values on its two rays. If its pre-Schwarzian has a conjugation-symmetric holomorphic continuation φ to a punctured disc about x, then (z - x) * φ z → β - 1 from every direction. Both convex and reentrant corners are allowed. No power representation or boundary differentiability is assumed.

Assembling the Schwarz--Christoffel formula

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_tendsto {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (z₀ : UpperHalfPlane) {f φ : ℂ → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0) (hφ : DifferentiableOn ℂ φ (Set.range fun (i : ι) => ↑(a i))ᶜ) (hφf : Set.EqOn φ (logDeriv (deriv f)) UpperHalfPlane.upperHalfPlaneSet) (hpole : ∀ (i : ι), Filter.Tendsto (fun (z : ℂ) => (z - ↑(a i)) * φ z) (nhdsWithin ↑(a i) {↑(a i)}ᶜ) (nhds ↑(e i))) (hinfty : Filter.Tendsto φ (Bornology.cobounded ℂ) (nhds 0)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The converse Schwarz--Christoffel theorem from the prevertex residues. Let f be holomorphic with nonvanishing derivative on the upper half-plane and suppose its pre-Schwarzian derivative continues to a function φ holomorphic off the distinct real prevertices a i, with singularities at worst simple poles of residues e i, and decaying at infinity. Then f is the affine image A * F + B of the normalized Schwarz--Christoffel primitive F for the data a and e, with A and B read off at the normalization point.