Injectivity of the bounded Schwarz--Christoffel boundary arc

The boundary values between the first and last prevertices trace the finite sides of the Schwarz--Christoffel polygon. If distinct sides meet only at their common endpoint when they are consecutive, this parametrization is injective. The hypothesis is phrased entirely in terms of the polygon's side segments, so it applies equally to convex and reentrant polygons. In the nonconvex case it is the bridge from side-separation criteria to a simple compactified boundary.

This gives a bounded-arc injectivity criterion in terms of side intersections, including for polygons with reentrant corners. No condition on the sum of the turning exponents at infinity is needed for this bounded arc.

References

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

theorem TauCeti.schwarzChristoffelBoundary_injOn_prevertex_interval_of_edge_intersections {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (k : Fin (n + 1)), -1 < ∑ l : Fin (n + 1) with a l = a k, e l) (hinter : ∀ (i j : Fin n), i < j → ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc → ↑j = ↑i + 1 ∧ z = schwarzChristoffelVertex a e z₀ i.succ) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Icc (a 0) (a (Fin.last n)))

If finite polygon sides meet only at the vertex shared by consecutive sides, the Schwarz--Christoffel boundary is injective between its first and last finite prevertices. The exponents need only be integrable at the finite prevertices.