The Schwarz--Christoffel primitive onto an unbounded polygon

Let F = schwarzChristoffelPrimitive a e z₀ and B = schwarzChristoffelBoundary a e z₀. When every finite prevertex is integrable and the total exponent ∑ i, e i is at least -1, the point at infinity of the upper half-plane is sent to infinity: B escapes every bounded set at both ends of the real axis, and F escapes every bounded set uniformly in the upper half-plane. The candidate polygon is then unbounded, and its boundary is the range of B, which is closed because B is proper.

This file develops, in that regime, the counterpart of the bounded image and covering theory of TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Image and TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Covering. The primitive is proper over the complement of range B: the points of the upper half-plane sent into a compact set avoiding range B form a compact set. Consequently the closure of the image is the image together with range B, the primitive is a covering map over the complement of range B, and it maps the upper half-plane bijectively onto any simply connected set that avoids range B and contains the image. Unlike in the bounded case only compact, rather than closed, sets have compact preimages, since the image is unbounded.

Main results

• TauCeti.isCompact_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive_of_neg_one_le_sum -- the preimage of a compact set avoiding the boundary values is compact.
• TauCeti.closure_image_schwarzChristoffelPrimitive_of_neg_one_le_sum -- the closure of the image is the image together with the boundary values.
• TauCeti.frontier_image_schwarzChristoffelPrimitive_of_neg_one_le_sum -- its frontier is the set of boundary values outside the image.
• TauCeti.image_schwarzChristoffelPrimitive_eq_of_subset_of_neg_one_le_sum -- a preconnected set avoiding the boundary values and containing the image is the image.
• TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive_of_neg_one_le_sum -- on ℍ, the primitive is a covering map over the complement of the boundary values.
• TauCeti.bijOn_schwarzChristoffelPrimitive_of_subset_of_neg_one_le_sum -- the primitive maps the upper half-plane bijectively onto every simply connected set that avoids the boundary values and contains the image.

References

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

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

The Schwarz--Christoffel primitive is proper over the complement of its boundary values when every finite prevertex is integrable and the total exponent is at least -1. The points of the upper half-plane that the primitive sends into a compact set K avoiding the range of the boundary map form a compact set.

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

The closure of the image of the Schwarz--Christoffel primitive is the image together with the boundary values, when every finite prevertex is integrable and the total exponent is at least -1.

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

The frontier of the image of the Schwarz--Christoffel primitive is the set of boundary values that the image does not cover, when every finite prevertex is integrable and the total exponent is at least -1.

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

A preconnected set avoiding the boundary values and containing the image is the image, when every finite prevertex is integrable and the total exponent is at least -1.

theorem TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive_of_neg_one_le_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hsum : -1 ≤ ∑ i : ι, e i) : IsCoveringMapOn (fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) (Set.range (schwarzChristoffelBoundary a e z₀))ᶜ

The Schwarz--Christoffel primitive is a covering map off its boundary values when every finite prevertex is integrable and the total exponent is at least -1. Viewed as a map on ℍ, it is a covering map over the complement of the range of the boundary map.

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

The Schwarz--Christoffel primitive is a bijection onto a simply connected region avoiding its boundary values, when every finite prevertex is integrable and the total exponent is at least -1. If the image of the upper half-plane lies in a simply connected set W disjoint from the range of the boundary map, then the primitive maps the upper half-plane bijectively onto W.