Finite boundary values of a Schwarz--Christoffel map with several ends

A logarithmic prevertex is a boundary parameter whose image in the Riemann sphere is infinity. When every finite prevertex exponent sum is at least -1, the finite spherical boundary values are precisely the ordinary values at integrable real parameters, together with the value at parameter infinity when the total exponent is less than -1. This description makes the exceptional set in the multiple-end covering theorem explicit in the complex plane.

References

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

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

The finite boundary trace: ordinary boundary values at integrable real parameters, with the vertex at parameter infinity included exactly when it is finite.

@[simp]

theorem TauCeti.mem_schwarzChristoffelFiniteBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (w : ℂ) : w ∈ schwarzChristoffelFiniteBoundary a e z₀ ↔ (∃ (p : ℝ), -1 < ∑ i : ι with a i = p, e i ∧ schwarzChristoffelBoundary a e z₀ p = w) ∨ ∑ i : ι, e i < -1 ∧ w = schwarzChristoffelVertexAtInfinity a e z₀

Membership in the finite boundary trace is an ordinary boundary value at an integrable parameter, or the vertex at infinity when that vertex is finite.

theorem TauCeti.schwarzChristoffelFiniteBoundary_change_base {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (b c : UpperHalfPlane) : schwarzChristoffelFiniteBoundary a e b = (fun (w : ℂ) => w - schwarzChristoffelPrimitive a e c ↑b) '' schwarzChristoffelFiniteBoundary a e c

Changing the base point translates every finite boundary value by the same constant.

theorem TauCeti.schwarzChristoffelFiniteBoundary_eq_preimage_range {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) : schwarzChristoffelFiniteBoundary a e z₀ = OnePoint.some ⁻¹' Set.range (schwarzChristoffelSphereBoundary a e z₀)

The finite trace is exactly the preimage in ℂ of the sphere-valued boundary range. Logarithmic prevertices contribute no finite value.

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

When every boundary value is finite, the finite trace is the range of the complex-valued compactified boundary.

theorem TauCeti.isClosed_schwarzChristoffelFiniteBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) : IsClosed (schwarzChristoffelFiniteBoundary a e z₀)

The finite boundary trace is closed, even when several real parameters map to infinity.

theorem TauCeti.closure_image_schwarzChristoffelPrimitive_eq_union_finiteBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) : closure (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) = schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ∪ schwarzChristoffelFiniteBoundary a e z₀

The closure of the primitive image consists of the image and its finite boundary trace. This holds with any number of logarithmic prevertices, including when the parameter at infinity also maps to infinity.

theorem TauCeti.frontier_image_schwarzChristoffelPrimitive_eq_finiteBoundary_diff_image {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) : frontier (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) = schwarzChristoffelFiniteBoundary a e z₀ \ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet

The frontier consists of finite boundary values that the primitive does not also take in the open upper half-plane. Thus an image-avoidance theorem makes the entire finite trace the frontier, including for polygons with several ends.