Integrating the Schwarz--Christoffel differential equation

The pre-Schwarzian differential equation

F'' / F' = ∑ i, e i / (z - a i)

determines a locally conformal holomorphic map of the upper half-plane up to an affine postcomposition. Indeed, the right-hand side is the pre-Schwarzian derivative of the normalized Schwarz--Christoffel primitive. Equality of the two logarithmic derivatives first identifies their first derivatives up to a nonzero constant, and connectedness then identifies the functions up to an additive constant.

This is the integration step in the converse Schwarz--Christoffel theorem. Once reflection and partial fractions identify the pre-Schwarzian of a polygon map with the displayed sum, the result here recovers the map itself as an affine image of the normalized primitive.

Main result

• TauCeti.exists_eqOn_const_mul_schwarzChristoffelPrimitive_add_iff -- a locally conformal holomorphic map solves the Schwarz--Christoffel pre-Schwarzian equation exactly when it is A * primitive + B for a nonzero A.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_logDeriv_deriv_eqOn -- the same integration result with A and B read off from the value and derivative at the normalization point.

References

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

theorem TauCeti.exists_eqOn_const_mul_schwarzChristoffelPrimitive_add_iff {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0) : (∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.EqOn f (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet) ↔ Set.EqOn (logDeriv (deriv f)) (fun (z : ℂ) => ∑ i : ι, ↑(e i) / (z - ↑(a i))) UpperHalfPlane.upperHalfPlaneSet

Integration of the Schwarz--Christoffel differential equation. A holomorphic function f with holomorphic, nonvanishing derivative on the upper half-plane has pre-Schwarzian ∑ i, e i / (z - a i) exactly when it is A * F + B for a nonzero constant A, where F is the normalized Schwarz--Christoffel primitive for the prevertices a and exponents e.

No separate regularity assumption is needed for deriv f: complex differentiability on an open set already implies complex differentiability of the derivative there.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_logDeriv_deriv_eqOn {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0) (hpre : Set.EqOn (logDeriv (deriv f)) (fun (z : ℂ) => ∑ i : ι, ↑(e i) / (z - ↑(a i))) UpperHalfPlane.upperHalfPlaneSet) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

Normalized integration of the Schwarz--Christoffel differential equation. If the pre-Schwarzian of f is the Schwarz--Christoffel partial-fraction sum, then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * primitive(z) + f(z₀).

Thus the value and derivative at the primitive's base point determine the two constants. The denominator is nonzero because the Schwarz--Christoffel integrand has no zeros in the upper half-plane.