Intersection of the two Schwarz--Christoffel closing sides

When the exponent sum is -2, the final finite vertex, the common value at infinity, and the first finite vertex occur in strict order on a horizontal line. Consequently the two closing sides meet exactly at their shared endpoint. Their finite boundary parametrizations omit that endpoint, so the two unbounded real rays have disjoint images. This is the separation at infinity needed to check that a nonconvex Schwarz--Christoffel boundary is simple.

References

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

theorem TauCeti.schwarzChristoffelPolygon_closingSides_inter {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), -1 < e k) (hsum : ∑ k : Fin (n + 1), e k = -2) : Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last n).castSucc ∩ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)) = {schwarzChristoffelVertexAtInfinity a e z₀}

The two closing sides of a Schwarz--Christoffel polygon meet only at their shared endpoint, the boundary value at infinity. No upper bound on the individual exponents is needed.

@[simp]

theorem TauCeti.disjoint_schwarzChristoffelBoundary_unbounded_images {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), -1 < e k) (hsum : ∑ k : Fin (n + 1), e k = -2) : Disjoint (schwarzChristoffelBoundary a e z₀ '' Set.Iic (a 0)) (schwarzChristoffelBoundary a e z₀ '' Set.Ici (a (Fin.last n)))

The finite parts of the two unbounded Schwarz--Christoffel boundary rays are disjoint. Their segment closures touch at the value at infinity, which neither finite ray attains.