The Schwarz--Christoffel formula from local polygonal boundary data

A locally conformal map f of the upper half-plane satisfying the prescribed straight-side and corner-sector boundary conditions, and an asymptotic condition at infinity, is completely determined, up to an affine map of the target, by the real prevertices a i and the turning exponents e i: it is A * F + B, where F is the normalized Schwarz--Christoffel primitive for a and e.

The side and corner data are the two ways a real point can sit against the polygon.

• Away from the prevertices, f extends continuously and injectively to the real axis with boundary values on an affine line, the nearby upper half-plane lying strictly to one side of it; that is, the boundary interval is carried into a side.
• At the prevertex a i the image f - f (a i), rotated and scaled by some b ≠ 0, lies inside the sector of opening (e i + 1) * π and has boundary values on its two rays; that is, the two sides meeting at the vertex f (a i) make the interior angle (e i + 1) * π. The exponent condition e i ∈ Ioo (-1) 1 says that angle lies strictly between 0 and 2 * π, so both convex and reentrant vertices are allowed.

At infinity the condition is that z * f''(z) / f'(z) has a finite limit L as z tends to infinity in the upper half-plane. The geometric conditions at infinity supply it, by TauCeti.Analysis.Complex.Conformal.Reflection.Infinity: if the point at infinity is carried into a side of the polygon then L = -2, and if it is carried to a vertex at infinity, between two unbounded sides spanning a sector of opening β * π, then L = β - 1. In either case L is the sum of the turning exponents.

These are local conditions; they do not assert global injectivity or surjectivity onto a polygon. Under these conditions, the proof runs the classical argument: the pre-Schwarzian derivative f'' / f' continues by Schwarz reflection across every boundary side to a conjugation-symmetric function holomorphic off the prevertices, a straightened corner gives it the residue e i at a i, the condition at infinity makes it decay there, so partial fractions identify it with ∑ i, e i / (z - a i), and integrating that differential equation recovers f.

Main results

• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary -- a locally conformal map of the upper half-plane satisfying the prescribed local side and corner conditions, with z * f''(z) / f'(z) convergent at infinity, is an affine image of the Schwarz--Christoffel primitive for a and e.
• TauCeti.exponent_sum_eq_of_logDeriv_deriv_eqOn -- if the pre-Schwarzian derivative of such a map is ∑ i, e i / (z - a i), then ∑ i, e i is the limit of z * f''(z) / f'(z) at infinity.

References

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

theorem TauCeti.exponent_sum_eq_of_logDeriv_deriv_eqOn {ι : Type u_1} [Fintype ι] (a e : ι → ℂ) {f : ℂ → ℂ} {L : ℂ} (hpre : Set.EqOn (logDeriv (deriv f)) (fun (z : ℂ) => ∑ i : ι, e i / (z - a i)) UpperHalfPlane.upperHalfPlaneSet) (hinfty : Filter.Tendsto (fun (z : ℂ) => z * logDeriv (deriv f) z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds L)) : ∑ i : ι, e i = L

The exponent sum is the limit at infinity. Let f have pre-Schwarzian derivative f'' / f' = ∑ i, e i / (z - a i) on the upper half-plane, where the poles a i and coefficients e i may be complex, and suppose that z * f''(z) / f'(z) → L as z tends to infinity in the upper half-plane. Then ∑ i, e i = L.

When the point at infinity is carried into a side of a polygon, L = -2 (TauCeti.tendsto_mul_logDeriv_deriv_upperHalfPlaneSet_of_eqOn_neg_inv); for the turning exponents e i = α i / π - 1 of a polygon with interior angles α i, this is the angle sum ∑ i, α i = (n - 2) * π.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0) (hside : ∀ (x : ℝ), (∀ (i : ι), a i ≠ x) → ∃ r > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ContinuousOn f (Metric.ball (↑x) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ Set.InjOn f (Metric.ball (↑x) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ (∀ z ∈ Metric.ball (↑x) r, z.im = 0 → ((f z - q) / b).im = 0) ∧ ∀ z ∈ Metric.ball (↑x) r, 0 < z.im → 0 < ((f z - q) / b).im) (hcorner : ∀ (i : ι), ∃ r > 0, ∃ (b : ℂ), b ≠ 0 ∧ ContinuousOn f (Metric.ball (↑(a i)) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ Set.InjOn f (Metric.ball (↑(a i)) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ (∀ z ∈ Metric.ball (↑(a i)) r, 0 < z.im → |((f z - f ↑(a i)) / b).arg| < (e i + 1) * Real.pi / 2) ∧ ∀ z ∈ Metric.ball (↑(a i)) r, z.im = 0 → f z ≠ f ↑(a i) → |((f z - f ↑(a i)) / b).arg| = (e i + 1) * Real.pi / 2) {L : ℂ} (hinfty : Filter.Tendsto (fun (z : ℂ) => z * logDeriv (deriv f) z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds L)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula. Let f be holomorphic with nonvanishing derivative on the upper half-plane. Assume that away from the distinct real prevertices a i its boundary values run along affine lines with the upper half-plane on one side, that at a i it opens the sector of angle (e i + 1) * π with boundary values on the two bounding rays, and that z * f''(z) / f'(z) has a finite limit as z tends to infinity in the upper half-plane. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the data a and e. So f is an affine image of F, and the two constants are read off from the value and derivative of f at the normalization point z₀.