The Schwarz--Christoffel map of a simple polygon #
When its compactified boundary is a simple curve, the Schwarz--Christoffel primitive maps the upper half-plane bijectively onto the complementary component containing its base-point image. This identifies the image component for simple polygons, including those with reentrant corners.
References #
- L. Ahlfors, Complex Analysis, Chapter 6, Section 2.
- T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Chapter 2.
theorem
TauCeti.bijOn_schwarzChristoffelPrimitive_of_simple_boundary
{ι : Type u_1}
[Fintype ι]
(a e : ι → ℝ)
(z₀ : UpperHalfPlane)
(hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i)
(hinfty : ∑ i : ι, e i < -1)
(hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀))
:
Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet
(connectedComponentIn (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))ᶜ
(schwarzChristoffelPrimitive a e z₀ ↑z₀))
A simple compactified Schwarz--Christoffel boundary makes the primitive a bijection from the upper half-plane onto the complementary component containing its base-point image.