A Schwarz--Christoffel map onto a nonconvex polygon

Finite signed-height checks on the Schwarz--Christoffel vertices certify that the bounded sides do not cross and that the bounded arc stays above the closing side. With interior turning exponents in (-1, 1) \ {0}, endpoint exponents greater than -1, and total exponent -2, these checks make the compactified boundary a Jordan curve. The primitive then maps the upper half-plane bijectively onto the filled interior of that polygon. Positive exponents, and hence reentrant corners, are allowed.

References

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

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective_of_vertex_separation_of_vertex_heights {n : ℕ} (a e : Fin (n + 3) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 3)), -1 < e k) (hsum : ∑ k : Fin (n + 3), e k = -2) (hcorner : ∀ (k : Fin (n + 2)), ↑k + 1 < n + 2 → e k.succ < 1) (hne : ∀ (k : Fin (n + 2)), ↑k + 1 < n + 2 → e k.succ ≠ 0) (hsep : ∀ (i j : Fin (n + 2)), ↑i + 1 < ↑j → have c := Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I); have u := schwarzChristoffelVertex a e z₀ i.castSucc; have v := schwarzChristoffelVertex a e z₀ j.castSucc; have w := schwarzChristoffelVertex a e z₀ j.succ; 0 < (c * (v - u)).im ∧ 0 < (c * (w - u)).im ∨ (c * (v - u)).im < 0 ∧ (c * (w - u)).im < 0) (hheight : ∀ (k : Fin (n + 3)), k ≠ 0 → k ≠ Fin.last (n + 2) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)

Signed vertex separation for nonadjacent bounded sides, together with strict heights above the closing line, makes the entire compactified Schwarz--Christoffel boundary injective.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_filledHull_sdiff_of_vertex_separation_of_vertex_heights {n : ℕ} (a e : Fin (n + 3) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 3)), -1 < e k) (hsum : ∑ k : Fin (n + 3), e k = -2) (hcorner : ∀ (k : Fin (n + 2)), ↑k + 1 < n + 2 → e k.succ < 1) (hne : ∀ (k : Fin (n + 2)), ↑k + 1 < n + 2 → e k.succ ≠ 0) (hsep : ∀ (i j : Fin (n + 2)), ↑i + 1 < ↑j → have c := Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I); have u := schwarzChristoffelVertex a e z₀ i.castSucc; have v := schwarzChristoffelVertex a e z₀ j.castSucc; have w := schwarzChristoffelVertex a e z₀ j.succ; 0 < (c * (v - u)).im ∧ 0 < (c * (w - u)).im ∨ (c * (v - u)).im < 0 ∧ (c * (w - u)).im < 0) (hheight : ∀ (k : Fin (n + 3)), k ≠ 0 → k ≠ Fin.last (n + 2) → (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet (filledHull (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)) \ Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀))

Under finite vertex-separation and closing-height checks, the Schwarz--Christoffel primitive maps the upper half-plane bijectively onto the filled polygon interior. The exponents may be positive at reentrant corners.