Simplicity from Schwarz--Christoffel side intersections

The compactified boundary of a Schwarz--Christoffel primitive is injective when its bounded polygon sides intersect only at consecutive vertices and meet each closing side only at that side's finite endpoint. This criterion applies to nonconvex polygons: it reduces the analytic injectivity question to intersections of finitely many straight segments. In conjunction with the polygon mapping theorem, it identifies the image of the upper half-plane with the Jordan interior bounded by these sides.

References

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

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective_of_edge_intersections {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (hfinite : ∀ (k : Fin (n + 2)), -1 < ∑ l : Fin (n + 2) with a l = a k, e l) (hsum : ∑ k : Fin (n + 2), e k = -2) (hinter : ∀ (i j : Fin (n + 1)), 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) (hleft : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 2)) → z = schwarzChristoffelVertex a e z₀ 0) (hright : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)).castSucc → z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)

A side-intersection criterion for simplicity of the compactified Schwarz--Christoffel boundary. The finite prevertices are strictly ordered, their exponents are integrable, and the total exponent is -2. Bounded sides may make reentrant turns. The three intersection hypotheses say that nonadjacent bounded sides are disjoint, adjacent ones meet only at their common vertex, and the bounded arc meets either closing side only at its finite endpoint.