Documentation

TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Univalence

An exponent criterion for Schwarz--Christoffel univalence #

If the total absolute turning exponent satisfies ∑ i, |e i| ≤ 1, the Schwarz--Christoffel primitive is injective on the upper half-plane. The exponents may have both signs, so the criterion permits reentrant corners. It imposes no separation or simplicity condition on the boundary, and does not require distinct or ordered prevertices.

The argument of each factor z - a i lies strictly between 0 and π. Centering these arguments at π / 2 shows that rotation by exp (-π / 2 * (∑ i, e i) * I) puts the integrand in the open right half-plane. The strict interior bound also handles equality in the coefficient criterion. The Noshiro--Warschawski criterion then gives global injectivity.

This is a sufficient criterion for unbounded Schwarz--Christoffel maps. It does not apply to the classical bounded-polygon data ∑ i, e i = -2.

References #

theorem TauCeti.re_exp_mul_schwarzChristoffelIntegrand_pos_of_sum_abs_le_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (he : ∑ i : ι, |e i| ≤ 1) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) :
0 < (Complex.exp (-↑(Real.pi / 2 * ∑ i : ι, e i) * Complex.I) * schwarzChristoffelIntegrand a e z).re

If the absolute turning exponents sum to at most one, a fixed rotation places the Schwarz--Christoffel integrand strictly in the right half-plane.

An exponent criterion for Schwarz--Christoffel univalence. If the total absolute turning exponent is at most one, the primitive is injective on the upper half-plane, including when positive exponents produce reentrant corners. No hypothesis on the boundary curve is needed.