The unbounded Schwarz--Christoffel boundary edges

Assume that all prevertices having nonzero exponent lie on one side of a real point p, and that the sum of the exponents at p is greater than -1. The canonical boundary map then follows one straight edge on the corresponding half-line. If the total exponent is less than -1, the edge has a finite endpoint at schwarzChristoffelVertexAtInfinity; together with the local exponent-sum hypothesis, its image is the segment from the value at p to that endpoint, with the endpoint at infinity omitted from the image.

This result supplies the boundary-edge description used when assembling the boundary of an unbounded Schwarz--Christoffel polygon. The endpoint at infinity is identified with the common limit of the boundary map along the two unbounded real rays; the theorem records that this endpoint is approached but not reached at a finite parameter.

Main results

• TauCeti.schwarzChristoffelBoundary_image_Ici and TauCeti.schwarzChristoffelBoundary_image_Iic -- the right- and left-hand unbounded boundary edges are half-open segments from their finite endpoints to the vertex at infinity.
• TauCeti.schwarzChristoffelBoundary_injOn_Ici and TauCeti.schwarzChristoffelBoundary_injOn_Iic -- the two unbounded boundary maps are injective on their finite parameters.
• TauCeti.schwarzChristoffelVertexAtInfinity_sub_boundary_eq_norm_mul and TauCeti.schwarzChristoffelBoundary_sub_vertexAtInfinity_eq_norm_mul -- the endpoint vectors of the two unbounded sides have the expected directions.
• TauCeti.schwarzChristoffelBoundary_image_Ici_prevertex and TauCeti.schwarzChristoffelBoundary_image_Iic_prevertex -- the same edge descriptions with the finite endpoints expressed as Schwarz--Christoffel vertices.
• TauCeti.schwarzChristoffelBoundary_ne_vertexAtInfinity_of_forall_le and TauCeti.schwarzChristoffelBoundary_ne_vertexAtInfinity_of_forall_ge -- the finite endpoint of either unbounded edge differs from its endpoint at infinity.
• TauCeti.schwarzChristoffelBoundary_lt_vertexAtInfinity and TauCeti.schwarzChristoffelVertexAtInfinity_lt_boundary -- the right-hand edge, and the left-hand edge when the total exponent is -2, run in the positive real direction: their finite endpoints lie respectively left and right of the vertex at infinity on a horizontal line (in the order ComplexOrder).

References

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

theorem TauCeti.continuousOn_schwarzChristoffelBoundary_Ici {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) : ContinuousOn (schwarzChristoffelBoundary a e z₀) (Set.Ici p)

The boundary map is continuous on a right outer edge with an integrable finite endpoint, independently of the total exponent.

theorem TauCeti.schwarzChristoffelBoundary_sub_eq_norm_mul_of_forall_le {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p x : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hx : p ≤ x) : schwarzChristoffelBoundary a e z₀ x - schwarzChristoffelBoundary a e z₀ p = ↑‖schwarzChristoffelBoundary a e z₀ x - schwarzChristoffelBoundary a e z₀ p‖ * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)

On a right outer edge, distance from the finite endpoint parametrizes the boundary map in the edge direction, independently of the total exponent.

theorem TauCeti.schwarzChristoffelBoundary_injOn_Ici {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Ici p)

The Schwarz--Christoffel boundary map is injective on a right-hand unbounded edge. Under -1 < ∑ i with a i = p, e i and ∀ i, e i ≠ 0 → a i ≤ p, distinct finite parameters in Ici p have distinct boundary values.

theorem TauCeti.schwarzChristoffelVertexAtInfinity_sub_boundary_eq_norm_mul {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelVertexAtInfinity a e z₀ - schwarzChristoffelBoundary a e z₀ p = ↑‖schwarzChristoffelVertexAtInfinity a e z₀ - schwarzChristoffelBoundary a e z₀ p‖ * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)

The vector from the finite endpoint of a right-hand unbounded Schwarz--Christoffel edge to its vertex at infinity has the direction of that edge.

theorem TauCeti.schwarzChristoffelBoundary_image_Ici {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ '' Set.Ici p = segment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelVertexAtInfinity a e z₀) \ {schwarzChristoffelVertexAtInfinity a e z₀}

The image of the right-hand unbounded boundary edge is the segment from its finite endpoint to the vertex at infinity, with the latter not attained at a finite boundary parameter.

theorem TauCeti.schwarzChristoffelBoundary_image_Ici_prevertex {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j : ι) (hj : -1 < ∑ i : ι with a i = a j, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ a j) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ '' Set.Ici (a j) = segment ℝ (schwarzChristoffelVertex a e z₀ j) (schwarzChristoffelVertexAtInfinity a e z₀) \ {schwarzChristoffelVertexAtInfinity a e z₀}

The right-hand unbounded edge based at a prevertex starts at its corresponding Schwarz--Christoffel vertex.

theorem TauCeti.schwarzChristoffelBoundary_ne_vertexAtInfinity_of_forall_le {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ p ≠ schwarzChristoffelVertexAtInfinity a e z₀

The finite endpoint of a right-hand unbounded Schwarz--Christoffel edge differs from its endpoint at infinity. Thus the segment traced by the edge is nondegenerate.

theorem TauCeti.schwarzChristoffelBoundary_lt_vertexAtInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ p < schwarzChristoffelVertexAtInfinity a e z₀

The right-hand unbounded edge runs in the positive real direction. If all prevertices with nonzero exponent lie at or to the left of p, the boundary value at p lies strictly to the left of the vertex at infinity on a horizontal line, in the sense of ComplexOrder.

The left-hand edge

theorem TauCeti.continuousOn_schwarzChristoffelBoundary_Iic {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) : ContinuousOn (schwarzChristoffelBoundary a e z₀) (Set.Iic p)

The boundary map is continuous on a left outer edge with an integrable finite endpoint, independently of the total exponent.

theorem TauCeti.schwarzChristoffelBoundary_sub_eq_norm_mul_of_forall_ge {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p x : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hx : x ≤ p) : schwarzChristoffelBoundary a e z₀ p - schwarzChristoffelBoundary a e z₀ x = ↑‖schwarzChristoffelBoundary a e z₀ p - schwarzChristoffelBoundary a e z₀ x‖ * Complex.exp (↑Real.pi * ↑(∑ i : ι, e i) * Complex.I)

On a left outer edge, distance from the finite endpoint parametrizes the boundary map in direction -exp (π * (∑ i, e i) * I), independently of the total exponent.

theorem TauCeti.schwarzChristoffelBoundary_injOn_Iic {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Iic p)

The Schwarz--Christoffel boundary map is injective on a left-hand unbounded edge. Under -1 < ∑ i with a i = p, e i and ∀ i, e i ≠ 0 → p ≤ a i, distinct finite parameters in Iic p have distinct boundary values.

theorem TauCeti.schwarzChristoffelBoundary_sub_vertexAtInfinity_eq_norm_mul {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ p - schwarzChristoffelVertexAtInfinity a e z₀ = ↑‖schwarzChristoffelBoundary a e z₀ p - schwarzChristoffelVertexAtInfinity a e z₀‖ * Complex.exp (↑Real.pi * ↑(∑ i : ι, e i) * Complex.I)

The vector from the vertex at infinity of a left-hand unbounded Schwarz--Christoffel edge to its finite endpoint has the direction of that edge.

theorem TauCeti.schwarzChristoffelBoundary_image_Iic {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ '' Set.Iic p = segment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelVertexAtInfinity a e z₀) \ {schwarzChristoffelVertexAtInfinity a e z₀}

The image of the left-hand unbounded boundary edge is the segment from its finite endpoint to the vertex at infinity, with the latter not attained at a finite boundary parameter.

theorem TauCeti.schwarzChristoffelBoundary_image_Iic_prevertex {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j : ι) (hj : -1 < ∑ i : ι with a i = a j, e i) (ha : ∀ (i : ι), e i ≠ 0 → a j ≤ a i) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ '' Set.Iic (a j) = segment ℝ (schwarzChristoffelVertex a e z₀ j) (schwarzChristoffelVertexAtInfinity a e z₀) \ {schwarzChristoffelVertexAtInfinity a e z₀}

The left-hand unbounded edge based at a prevertex starts at its corresponding Schwarz--Christoffel vertex.

theorem TauCeti.schwarzChristoffelBoundary_ne_vertexAtInfinity_of_forall_ge {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hS : ∑ i : ι, e i < -1) : schwarzChristoffelBoundary a e z₀ p ≠ schwarzChristoffelVertexAtInfinity a e z₀

The finite endpoint of a left-hand unbounded Schwarz--Christoffel edge differs from its endpoint at infinity. Thus the segment traced by the edge is nondegenerate.

theorem TauCeti.schwarzChristoffelVertexAtInfinity_lt_boundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hsum : ∑ i : ι, e i = -2) : schwarzChristoffelVertexAtInfinity a e z₀ < schwarzChristoffelBoundary a e z₀ p

The left-hand unbounded edge runs in the positive real direction. If all prevertices with nonzero exponent lie at or to the right of p and the total exponent is -2, the vertex at infinity lies strictly to the left of the boundary value at p on a horizontal line, in the sense of ComplexOrder.