Sphere-valued Schwarz--Christoffel boundary extension

Schwarz--Christoffel primitives with integrable finite vertices and logarithmic ends extend continuously to the closed upper half-plane in the Riemann sphere. This includes the parameter at infinity, whether its image is finite or infinite. Restricting this extension to the real projective line gives a continuous boundary parametrization for data with several ends.

Finite prevertices of total exponent greater than -1 retain their ordinary boundary values; those of exponent -1 map to infinity. The parameter at infinity has a finite image in the decaying range of the total exponent, and maps to infinity otherwise. No global injectivity or boundary simplicity is assumed. In particular, several parameters can map to infinity, so continuity does not assert that this parametrization is a Jordan curve.

The construction uses Mathlib's extendFrom into OnePoint ℂ to assemble the finite-vertex, logarithmic-end and infinity limits of the primitive.

References

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

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

The canonical sphere-valued extension of the Schwarz--Christoffel primitive from the upper half-plane. Its values on the compactified closed upper half-plane are genuine limits when every finite prevertex has total exponent at least -1.

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

The sphere-valued Schwarz--Christoffel boundary on the real projective line, including finite parameters representing logarithmic ends.

@[simp]

theorem TauCeti.schwarzChristoffelSphereBoundary_apply {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (x : OnePoint ℝ) : schwarzChristoffelSphereBoundary a e z₀ x = schwarzChristoffelSphereExtension a e z₀ (OnePoint.map Complex.ofReal x)

The sphere boundary evaluates the sphere extension on the compactified real axis.

@[simp]

theorem TauCeti.schwarzChristoffelSphereExtension_coe_of_im_pos {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {z : ℂ} (hz : 0 < z.im) : schwarzChristoffelSphereExtension a e z₀ ↑z = ↑(schwarzChristoffelPrimitive a e z₀ z)

On the open upper half-plane, the sphere extension agrees with the primitive.

@[simp]

theorem TauCeti.schwarzChristoffelSphereExtension_coe_of_exponent_sum_gt_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : -1 < ∑ i : ι with a i = p, e i) : schwarzChristoffelSphereExtension a e z₀ ↑↑p = ↑(schwarzChristoffelBoundary a e z₀ p)

At an integrable real parameter, the sphere extension retains the finite boundary value.

@[simp]

theorem TauCeti.schwarzChristoffelSphereExtension_coe_of_exponent_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : ∑ i : ι with a i = p, e i = -1) : schwarzChristoffelSphereExtension a e z₀ ↑↑p = OnePoint.infty

A logarithmic real prevertex maps to infinity in the sphere extension.

theorem TauCeti.tendsto_onePoint_map_schwarzChristoffelPrimitive_infty {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : Filter.Tendsto (OnePoint.map (schwarzChristoffelPrimitive a e z₀)) (nhdsWithin OnePoint.infty (OnePoint.some '' UpperHalfPlane.upperHalfPlaneSet)) (nhds (if ∑ i : ι, e i < -1 then ↑(schwarzChristoffelVertexAtInfinity a e z₀) else OnePoint.infty))

At parameter infinity, the sphere-valued primitive approaches the finite vertex in the decaying range and infinity otherwise. This needs no assumptions on finite prevertices.

@[simp]

theorem TauCeti.schwarzChristoffelSphereExtension_infty {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : schwarzChristoffelSphereExtension a e z₀ OnePoint.infty = if ∑ i : ι, e i < -1 then ↑(schwarzChristoffelVertexAtInfinity a e z₀) else OnePoint.infty

At parameter infinity, the sphere extension has the finite vertex in the decaying range and the point at infinity otherwise. This needs no assumptions on finite prevertices.

@[simp]

theorem TauCeti.schwarzChristoffelSphereBoundary_coe_of_exponent_sum_gt_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : -1 < ∑ i : ι with a i = p, e i) : schwarzChristoffelSphereBoundary a e z₀ ↑p = ↑(schwarzChristoffelBoundary a e z₀ p)

At an integrable real parameter, the sphere boundary retains the finite boundary value.

@[simp]

theorem TauCeti.schwarzChristoffelSphereBoundary_coe_of_exponent_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : ∑ i : ι with a i = p, e i = -1) : schwarzChristoffelSphereBoundary a e z₀ ↑p = OnePoint.infty

A logarithmic real prevertex maps to infinity in the sphere boundary.

@[simp]

theorem TauCeti.schwarzChristoffelSphereBoundary_infty {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : schwarzChristoffelSphereBoundary a e z₀ OnePoint.infty = if ∑ i : ι, e i < -1 then ↑(schwarzChristoffelVertexAtInfinity a e z₀) else OnePoint.infty

The value of the sphere boundary at the compactifying parameter.

theorem TauCeti.schwarzChristoffelSphereBoundary_eq_coe_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) : schwarzChristoffelSphereBoundary a e z₀ = OnePoint.some ∘ schwarzChristoffelCompactifiedBoundary a e z₀

When all finite prevertices are integrable and the vertex at infinity is finite, the sphere boundary is the complex-valued compactified boundary embedded in the sphere.

theorem TauCeti.preimage_range_schwarzChristoffelSphereBoundary_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) : OnePoint.some ⁻¹' Set.range (schwarzChristoffelSphereBoundary a e z₀) = Set.range (schwarzChristoffelBoundary a e z₀)

When finite prevertices are integrable and the parameter at infinity maps to infinity, the finite spherical boundary values are exactly the ordinary boundary values.

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_sphereBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : -1 ≤ ∑ i : ι with a i = p, e i) : Filter.Tendsto (fun (z : ℂ) => ↑(schwarzChristoffelPrimitive a e z₀ z)) (nhdsWithin (↑p) UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelSphereBoundary a e z₀ ↑p))

The primitive approaches the sphere boundary from the whole upper half-plane, including at logarithmic ends.

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

Continuous spherical extension with multiple logarithmic ends. If every finite prevertex has total exponent at least -1, the sphere extension is continuous on the compactified closed upper half-plane. Neither ordering nor global univalence is required.

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

Continuous sphere boundary for several ends. Integrable finite vertices and any number of logarithmic prevertices assemble into a continuous map on the real projective line. The total exponent is unrestricted, so its compactifying parameter may have finite or infinite image.