The filled interior of a simple Schwarz--Christoffel polygon #
A simple compactified Schwarz--Christoffel boundary is a Jordan curve. Its regular edge is locally straight, so its bounded complementary component is the filled hull of the boundary minus the boundary itself. The Schwarz--Christoffel primitive maps the upper half-plane bijectively onto this filled interior. This identifies the target of the direct map without requiring convexity, including polygons with reentrant corners.
References #
- L. Ahlfors, Complex Analysis, Chapter 6, Section 2.
- T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Chapter 2.
theorem
TauCeti.image_schwarzChristoffelPrimitive_eq_filledHull_sdiff
{ι : 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₀))
:
The image of the Schwarz--Christoffel primitive bounded by a simple compactified boundary is exactly the filled hull of that boundary with the boundary removed.
theorem
TauCeti.bijOn_schwarzChristoffelPrimitive_filledHull_sdiff
{ι : 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₀))
:
A simple compactified Schwarz--Christoffel boundary makes the primitive a bijection from the upper half-plane onto the filled polygon interior.