A vertex separation criterion for a Schwarz--Christoffel boundary arc

For a polygon with reentrant corners, ordered prevertices and integrable exponents alone do not make its boundary simple. The criterion here checks the bounded arc using only the finite Schwarz--Christoffel vertices. At each nonadjacent pair of sides, the two endpoints of the later side must lie strictly on the same side of the earlier side's supporting line. With strictly ordered prevertices, turning exponents in (-1, 1) \ {0} at the interior vertices make each adjacent pair meet only at its common vertex.

The criterion is sufficient for injectivity between the first and last prevertices. To obtain a simple compactified boundary, the two sides incident to infinity must also be checked.

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_vertex_separation {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), -1 < e k) (hcorner : ∀ (k : Fin n), ↑k + 1 < n → e k.succ < 1) (hne : ∀ (k : Fin n), ↑k + 1 < n → e k.succ ≠ 0) (hsep : ∀ (i j : Fin n), ↑i + 1 < ↑j → have c := Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I); have u := schwarzChristoffelVertex a e z₀ i.castSucc; have v := schwarzChristoffelVertex a e z₀ j.castSucc; have w := schwarzChristoffelVertex a e z₀ j.succ; 0 < (c * (v - u)).im ∧ 0 < (c * (w - u)).im ∨ (c * (v - u)).im < 0 ∧ (c * (w - u)).im < 0) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Icc (a 0) (a (Fin.last n)))

Strict signed heights at the endpoints of every nonadjacent later side, together with strictly ordered prevertices and turning exponents in (-1, 1) \ {0} at the interior vertices, make the bounded Schwarz--Christoffel boundary arc injective. Heights are measured after rotating each earlier side to the real axis. The condition allows both positive and negative turning exponents.