Disc Schwarz--Christoffel maps with a vertex at infinity

An unbounded polygonal Jordan domain that agrees at infinity with a sector of opening β * π has a disc Schwarz--Christoffel representation with one additional prevertex at 1. Its exponent is -β - 1, whereas the finite vertices retain the exponents given by their interior angles. Thus the sum of all disc exponents is -2, even though the finite half-plane exponents sum to β - 1.

The representation below includes the limits at every finite vertex and divergence at 1. In particular, its added exponent is allowed to be less than -1: that prevertex maps to infinity, rather than to a finite corner. The finite prevertices are the Cayley images of distinct real prevertices, so none equals 1.

References

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

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_of_isJordanCurve_insert_infty {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {β : ℝ} (hβ : β ∈ Set.Ioo 0 2) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ |((z - c) / b).arg| < β * Real.pi / 2)) : ∃ (a : ι → ℝ), Function.Injective a ∧ ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (ζ : ℂ) => A * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-β - 1) e) ζ + B) (Metric.ball 0 1) U ∧ (∀ (i : ι), Filter.Tendsto (fun (ζ : ℂ) => A * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (j : ι) => boundaryCayley (a j)) (Option.elim' (-β - 1) e) ζ + B) (nhdsWithin (↑(boundaryCayley (a i))) (Metric.ball 0 1)) (nhds (v i))) ∧ Filter.Tendsto (fun (ζ : ℂ) => A * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-β - 1) e) ζ + B) (nhdsWithin 1 (Metric.ball 0 1)) (Bornology.cobounded ℂ)

The disc Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain. Suppose a connected open set has Jordan frontier on the Riemann sphere, finitely many distinct corners of angles (e i + 1) * π, straight sides away from those corners, and a sector of opening β * π at infinity. Then it is the bijective image of the unit disc under an affine image of a disc Schwarz--Christoffel primitive. The finite prevertices have exponents e i and tend to the prescribed vertices; the additional prevertex 1 has exponent -β - 1 and tends to infinity.