The compactified Schwarz--Christoffel boundary

When the total Schwarz--Christoffel exponent is less than -1, the two ends of the real boundary have the same finite image. This file therefore joins the ordinary boundary map on ℝ with its value at infinity to give a map on the real projective line OnePoint ℝ.

If every finite prevertex is integrable, the compactified boundary map is continuous. Its exact injectivity criterion separates the remaining global simplicity problem into two concrete claims: the finite boundary map has no self-intersections, and it never passes through the vertex at infinity. Once those claims hold, its range is a Jordan curve. This is the topological boundary object used to identify the image of a Schwarz--Christoffel primitive with a polygonal domain.

Main definitions

• TauCeti.schwarzChristoffelCompactifiedBoundary -- the Schwarz--Christoffel boundary on OnePoint ℝ.

Main results

• TauCeti.continuous_schwarzChristoffelCompactifiedBoundary -- integrable finite prevertices and decay at infinity make the compactified boundary continuous.
• TauCeti.schwarzChristoffelCompactifiedBoundary_injective_iff -- exact global simplicity criterion in terms of the finite boundary and the vertex at infinity.
• TauCeti.isJordanCurve_range_schwarzChristoffelCompactifiedBoundary -- an injective compactified boundary traces a Jordan curve.

References

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

noncomputable def TauCeti.schwarzChristoffelCompactifiedBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : OnePoint ℝ → ℂ

The Schwarz--Christoffel boundary on the real projective line. It agrees with schwarzChristoffelBoundary at every finite real point and sends the compactifying point to the common boundary value schwarzChristoffelVertexAtInfinity.

Equations

• TauCeti.schwarzChristoffelCompactifiedBoundary a e z₀ x = x.elim (TauCeti.schwarzChristoffelVertexAtInfinity a e z₀) (TauCeti.schwarzChristoffelBoundary a e z₀)

@[simp]

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_infty {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : schwarzChristoffelCompactifiedBoundary a e z₀ OnePoint.infty = schwarzChristoffelVertexAtInfinity a e z₀

The compactified Schwarz--Christoffel boundary takes the prescribed value at infinity.

@[simp]

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_coe {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (x : ℝ) : schwarzChristoffelCompactifiedBoundary a e z₀ ↑x = schwarzChristoffelBoundary a e z₀ x

At a finite point, the compactified Schwarz--Christoffel boundary is the ordinary boundary value.

theorem TauCeti.continuous_schwarzChristoffelCompactifiedBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : Continuous (schwarzChristoffelCompactifiedBoundary a e z₀)

The compactified Schwarz--Christoffel boundary is continuous when every prevertex has integrable total exponent and the primitive has a finite limit at infinity.

The first hypothesis supplies continuity of the boundary map on ℝ. The inequality on the total exponent supplies convergence to the same vertex along the cocompact filter, which is exactly continuity at the added point of OnePoint ℝ.

theorem TauCeti.schwarzChristoffelCompactifiedBoundary_injective_iff {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀) ↔ Function.Injective (schwarzChristoffelBoundary a e z₀) ∧ ∀ (x : ℝ), schwarzChristoffelBoundary a e z₀ x ≠ schwarzChristoffelVertexAtInfinity a e z₀

The compactified boundary is injective exactly when its finite part is injective and no finite boundary value equals the vertex at infinity. Thus the global boundary-simplicity problem has no hidden condition at the compactification point.

theorem TauCeti.isJordanCurve_range_schwarzChristoffelCompactifiedBoundary {ι : 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₀)) : IsJordanCurve (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))

An injective compactified Schwarz--Christoffel boundary traces a Jordan curve. Continuity is supplied by integrability at every finite prevertex and decay at infinity; injectivity is left in the exact form characterized by schwarzChristoffelCompactifiedBoundary_injective_iff.