Simplicity of unbounded Schwarz--Christoffel boundaries

When the total turning exponent is at least -1, a Schwarz--Christoffel boundary consists of finitely many segments and two infinite rays. This file gives a finite geometric criterion for that boundary to be simple: distinct bounded sides meet only at a shared consecutive vertex, each outer ray meets the bounded sides only at its endpoint, and the two outer rays are disjoint.

The conclusion is injectivity of the boundary map on the real axis. Together with its properness, this identifies the boundary as a proper simple polygonal chain and supplies the geometric input for mapping the upper half-plane onto the region on one side of an unbounded polygon.

References

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

theorem TauCeti.schwarzChristoffelBoundary_injective_of_edge_intersections {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (k : Fin (n + 2)), -1 < ∑ l : Fin (n + 2) with a l = a k, e l) (hsum : -1 ≤ ∑ k : Fin (n + 2), e k) (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 ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ 0 - ↑t * Complex.exp (↑Real.pi * ↑(∑ k : Fin (n + 2), e k) * Complex.I)) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ 0) (hright : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ (Fin.last (n + 1)) + ↑t) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))) (houter : Disjoint ((fun (t : ℝ) => schwarzChristoffelVertex a e z₀ 0 - ↑t * Complex.exp (↑Real.pi * ↑(∑ k : Fin (n + 2), e k) * Complex.I)) '' Set.Ici 0) ((fun (t : ℝ) => schwarzChristoffelVertex a e z₀ (Fin.last (n + 1)) + ↑t) '' Set.Ici 0)) : Function.Injective (schwarzChristoffelBoundary a e z₀)

If the bounded sides of an unbounded Schwarz--Christoffel boundary meet only at consecutive vertices, each outer ray meets the bounded sides only at its finite endpoint, and the two outer rays are disjoint, then the boundary map is injective. The exponents need only be integrable at the finite prevertices, with total exponent at least -1 so that the outer edges are rays.