Schwarz--Christoffel coverings with several ends

If every finite prevertex has total exponent at least -1, the Schwarz--Christoffel primitive has a continuous extension to the compactified closed upper half-plane. Logarithmic prevertices map to infinity; they need not be distinct as sphere-valued boundary points. Compactness of this extension makes the primitive proper over the complement of its finite spherical boundary values, and hence a covering map there.

Consequently, a simply connected region avoiding those boundary values and containing the image is mapped onto bijectively. This is the covering criterion for polygonal images with several logarithmic ends. It does not assume boundary simplicity, impose a bound on the total exponent, or assert that the image avoids its boundary values automatically.

References

• L. Ahlfors, Complex Analysis, Chapter 6, Section 2.
• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Chapter 2.
• O. Forster, Lectures on Riemann Surfaces, Section 4.

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

The spherical closure of the image consists of the image together with the spherical boundary values. Logarithmic ends, including several parameters mapping to infinity, are allowed.

theorem TauCeti.isCompact_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive_of_neg_one_le_prevertex_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {K : Set ℂ} (hK : IsCompact K) (hKB : Disjoint (OnePoint.some '' K) (Set.range (schwarzChristoffelSphereBoundary a e z₀))) : IsCompact (UpperHalfPlane.upperHalfPlaneSet ∩ schwarzChristoffelPrimitive a e z₀ ⁻¹' K)

Compact sets avoiding the finite spherical boundary values have compact preimages in the upper half-plane, even when finite prevertices are logarithmic ends.

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

The primitive is a covering map over the complement of the finite spherical boundary values. Every finite prevertex may be integrable or logarithmic, and the total exponent is unrestricted.

theorem TauCeti.image_schwarzChristoffelPrimitive_eq_of_subset_of_neg_one_le_prevertex_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {W : Set ℂ} (hW : IsPreconnected W) (hWB : Disjoint (OnePoint.some '' W) (Set.range (schwarzChristoffelSphereBoundary a e z₀))) (hFW : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ W) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet = W

A preconnected region avoiding the finite spherical boundary values and containing the image is exactly the image, including for data with several logarithmic ends.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_of_subset_of_neg_one_le_prevertex_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {W : Set ℂ} [SimplyConnectedSpace ↑W] (hWB : Disjoint (OnePoint.some '' W) (Set.range (schwarzChristoffelSphereBoundary a e z₀))) (hFW : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ W) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet W

Univalence criterion with multiple logarithmic ends. If the image lies in a simply connected region avoiding the finite spherical boundary values, the Schwarz--Christoffel primitive maps the upper half-plane bijectively onto that region. Boundary injectivity is not assumed.