The Schwarz--Christoffel compactified boundary is polygonal

For a nondecreasing finite family of prevertices, the real projective line splits into the two unbounded intervals and the intervals between consecutive prevertices. The Schwarz--Christoffel boundary map carries each finite interval onto its bounded side. The real points in the two unbounded intervals trace the two sides incident to the common vertex at infinity with that vertex omitted; compactification supplies the omitted vertex.

Consequently the range of the compactified boundary map is exactly the boundary of the packaged polygon. This identification does not require the polygon to be simple; proving that distinct nonadjacent sides do not meet is the separate global injectivity problem.

Main result

• TauCeti.range_schwarzChristoffelCompactifiedBoundary -- the compactified boundary map traces exactly the boundary of schwarzChristoffelPolygon.

References

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

theorem TauCeti.range_schwarzChristoffelCompactifiedBoundary {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (j : Fin (n + 1)), -1 < ∑ i : Fin (n + 1) with a i = a j, e i) (hinfty : ∑ i : Fin (n + 1), e i < -1) : Set.range (schwarzChristoffelCompactifiedBoundary a e z₀) = Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)

The compactified Schwarz--Christoffel boundary traces the polygon boundary. For ordered prevertices, integrability at every finite prevertex and decay at infinity make each closed finite interval map onto its corresponding bounded side. Each unbounded interval traces its side with the common vertex at infinity omitted, and the compactified point supplies that vertex. Their union is the complete boundary of schwarzChristoffelPolygon.

No simplicity hypothesis is needed: this is an equality of ranges even when nonadjacent polygon sides intersect.