Recovering side intersections from a simple Schwarz--Christoffel boundary

For ordered prevertices, every bounded polygon side is the image of its closed prevertex interval. The two closing sides are the images of the unbounded real intervals, together with their common endpoint at infinity. Injectivity of the compactified boundary therefore forces nonadjacent sides to be disjoint and adjacent sides to meet only at their shared vertex. This is the converse of the side-intersection criterion for a simple Schwarz--Christoffel boundary.

References

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

theorem TauCeti.schwarzChristoffelPolygon_bounded_edges_adjacent_and_eq_vertex_of_injOn {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) (hinj : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Icc (a 0) (a (Fin.last (n + 1))))) (i j : Fin (n + 1)) (hij : i < j) (z : ℂ) (hzi : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzj : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc) : ↑j = ↑i + 1 ∧ z = schwarzChristoffelVertex a e z₀ i.succ

If the Schwarz--Christoffel boundary is injective between the first and last prevertices, two distinct bounded sides can meet only when consecutive, at their common finite vertex.

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_last_eq_first_vertex_of_injective {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) (hinfty : ∑ k : Fin (n + 2), e k < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) (i : Fin (n + 1)) (z : ℂ) (hzi : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzleft : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 2))) : z = schwarzChristoffelVertex a e z₀ 0

A bounded Schwarz--Christoffel side can meet the left closing side only at the first finite vertex when the compactified boundary is injective.

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_last_prevertex_eq_last_vertex_of_injective {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) (hinfty : ∑ k : Fin (n + 2), e k < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) (i : Fin (n + 1)) (z : ℂ) (hzi : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (hzright : z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)).castSucc) : z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))

A bounded Schwarz--Christoffel side can meet the right closing side only at the last finite vertex when the compactified boundary is injective.

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective_iff_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) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀) ↔ (∀ (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) ∧ (∀ (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) ∧ ∀ (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))

The compactified Schwarz--Christoffel boundary is simple exactly when its bounded sides and closing sides have the indicated finite intersections.