Simplicity of the convex Schwarz--Christoffel boundary

Strictly ordered prevertices and exponents in (-1, 0) summing to -2 give an injective compactified Schwarz--Christoffel boundary. Nonadjacent bounded sides are disjoint, adjacent bounded sides meet only at their common corner, and the bounded boundary arc lies strictly above the horizontal closing side except at its endpoints. The two unbounded arcs occupy opposite sides of the vertex at infinity. Thus the complete polygon boundary is a Jordan curve.

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 {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Icc (a 0) (a (Fin.last n)))

The Schwarz--Christoffel boundary is injective between its first and last finite prevertices under the classical convex-polygon hypotheses.

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)

Strictly ordered prevertices with exponents in (-1, 0) summing to -2 give an injective Schwarz--Christoffel boundary on the one-point compactification of the real line.

theorem TauCeti.isJordanCurve_schwarzChristoffelPolygon_boundary {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) : IsJordanCurve (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀))

The polygon traced by a convex Schwarz--Christoffel boundary is a Jordan curve. The vertex at infinity may subdivide a straight side; it need not be a genuine corner.