The convex Schwarz--Christoffel polygon mapping theorem

For strictly ordered real prevertices and turning exponents in (-1, 0) summing to -2, the Schwarz--Christoffel primitive maps the upper half-plane bijectively onto the interior of the closed convex hull of its polygonal boundary.

The supporting-line inequalities for the bounded and closing sides show that this convex interior does not meet the polygonal boundary. It is simply connected because it is nonempty and convex. The primitive is a covering map away from its compactified boundary path, so the covering is trivial over this interior and gives the desired bijection.

Main results

• TauCeti.disjoint_interior_closedConvexHull_schwarzChristoffelPolygon_boundary -- the convex polygon interior misses its boundary.
• TauCeti.bijOn_schwarzChristoffelPrimitive_interior_closedConvexHull -- the primitive maps the upper half-plane bijectively onto that interior.

References

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

theorem TauCeti.disjoint_interior_closedConvexHull_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) : Disjoint (interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)))) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀))

The convex Schwarz--Christoffel polygon interior is disjoint from its boundary. The interior is represented as the interior of the closed convex hull of the polygonal boundary.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_interior_closedConvexHull {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.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet (interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀))))

The Schwarz--Christoffel primitive maps the upper half-plane bijectively onto its convex polygon interior. The target is the interior of the closed convex hull of the polygonal boundary.