The closed edges of the Schwarz--Christoffel map are segments

The boundary values of the Schwarz--Christoffel map along a real interval free of prevertices with nonzero exponent are collinear and injective on the open interval. This file pins down the whole closed arc: the image of a closed prevertex-free interval is exactly the segment joining the two boundary values at its endpoints, and the image of the open interval is the corresponding open segment. When the endpoints are prevertices, the two boundary values are the Schwarz--Christoffel vertices, so each closed boundary interval is carried injectively onto the straight polygon side joining two consecutive vertices; that side is nondegenerate as soon as the two prevertices themselves are distinct.

All the results below share the same hypotheses on the interval [p, q]: no prevertex of nonzero exponent lies in Ioo p q, and each of p and q carries total exponent greater than -1, which is what makes the boundary map continuous up to that endpoint. Under those hypotheses every increment of the boundary map in the increasing direction is a nonnegative real multiple of the one unimodular direction exp (i * schwarzChristoffelEdgeAngle a e p), so the distance from the left endpoint is an arclength parameter on the arc: TauCeti.schwarzChristoffelBoundary_sub_eq_norm_mul records the direction and TauCeti.norm_schwarzChristoffelBoundary_sub_add records that the distances add. That is the form in which the length of an edge and the direction in which it leaves a vertex are read off.

These results describe the bounded part of the boundary of the Schwarz--Christoffel image edge by edge: over the prevertices ordered along the real line the boundary values run through a chain of straight sides joining consecutive vertices. The two unbounded boundary intervals are not covered here. About those, TauCeti.tendsto_schwarzChristoffelBoundaryValue_atInfinity says only that the boundary values converge to a common vertex at infinity in both directions; identifying the image of either unbounded interval as a segment or a ray remains open.

Main results

• TauCeti.schwarzChristoffelBoundary_sub_eq_norm_mul -- along a closed prevertex-free interval an increment of the boundary map is its own length times the unimodular edge direction.
• TauCeti.norm_schwarzChristoffelBoundary_sub_add -- those lengths add.
• TauCeti.schwarzChristoffelBoundary_injOn_Icc -- the boundary map is injective on the closed interval, endpoints included.
• TauCeti.schwarzChristoffelBoundary_image_Icc and TauCeti.schwarzChristoffelBoundary_image_Ioo -- the closed and the open boundary arcs are the segment and the open segment joining the two endpoint values.
• TauCeti.schwarzChristoffelBoundary_image_Icc_prevertex and TauCeti.schwarzChristoffelBoundary_image_Ioo_prevertex -- between two prevertices the closed and open boundary arcs are the straight side joining the corresponding Schwarz--Christoffel vertices and its interior.
• TauCeti.schwarzChristoffelVertex_ne -- that side is nondegenerate when the two prevertices are distinct.

References

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

theorem TauCeti.schwarzChristoffelBoundary_sub_eq_norm_mul {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) {x y : ℝ} (hx : x ∈ Set.Icc p q) (hy : y ∈ Set.Icc p q) (hyx : y ≤ x) : schwarzChristoffelBoundary a e z₀ x - schwarzChristoffelBoundary a e z₀ y = ↑‖schwarzChristoffelBoundary a e z₀ x - schwarzChristoffelBoundary a e z₀ y‖ * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)

An increment of the Schwarz--Christoffel boundary map along a closed edge is its own length times the edge direction. On a real interval free of prevertices with nonzero exponent, and with both endpoints carrying total exponent greater than -1, the boundary map moves in the increasing direction by exactly ‖B x - B y‖ along the unimodular direction with argument schwarzChristoffelEdgeAngle a e p.

theorem TauCeti.norm_schwarzChristoffelBoundary_sub_add {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) {x y z : ℝ} (hx : x ∈ Set.Icc p q) (hy : y ∈ Set.Icc p q) (hz : z ∈ Set.Icc p q) (hxy : x ≤ y) (hyz : y ≤ z) : ‖schwarzChristoffelBoundary a e z₀ z - schwarzChristoffelBoundary a e z₀ x‖ = ‖schwarzChristoffelBoundary a e z₀ y - schwarzChristoffelBoundary a e z₀ x‖ + ‖schwarzChristoffelBoundary a e z₀ z - schwarzChristoffelBoundary a e z₀ y‖

Lengths add along a closed Schwarz--Christoffel edge. For three points in increasing order in a closed interval free of prevertices with nonzero exponent, and with both endpoints carrying total exponent greater than -1, the distance between the two outer boundary values is the sum of the two distances cut out by the middle one.

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

The Schwarz--Christoffel boundary map is injective on a closed prevertex-free interval. On a real interval free of prevertices with nonzero exponent, both of whose endpoints carry total exponent greater than -1, distinct points have distinct boundary values; this is TauCeti.schwarzChristoffelBoundary_injOn with the two endpoints included, so a closed boundary arc between two prevertices is an embedded straight side.

theorem TauCeti.schwarzChristoffelBoundary_image_Icc {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (hpq : p ≤ q) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Icc p q = segment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelBoundary a e z₀ q)

A closed Schwarz--Christoffel boundary arc is a segment. Over a real interval free of prevertices with nonzero exponent, both of whose endpoints carry total exponent greater than -1, the image of the boundary map is exactly the segment joining its two endpoint values.

theorem TauCeti.schwarzChristoffelBoundary_image_Ioo {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (hpq : p < q) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Ioo p q = openSegment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelBoundary a e z₀ q)

An open Schwarz--Christoffel boundary arc is an open segment. The companion of TauCeti.schwarzChristoffelBoundary_image_Icc that omits the two endpoint values.

theorem TauCeti.schwarzChristoffelBoundary_image_Icc_prevertex {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {j k : ι} (hjk : a j ≤ a k) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo (a j) (a k)) (hj : -1 < ∑ i : ι with a i = a j, e i) (hk : -1 < ∑ i : ι with a i = a k, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Icc (a j) (a k) = segment ℝ (schwarzChristoffelVertex a e z₀ j) (schwarzChristoffelVertex a e z₀ k)

The straight sides of the Schwarz--Christoffel polygon. Between two prevertices with no prevertex of nonzero exponent strictly between them, and with both total exponents greater than -1, the closed boundary arc is exactly the segment joining the two Schwarz--Christoffel vertices.

theorem TauCeti.schwarzChristoffelBoundary_image_Ioo_prevertex {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {j k : ι} (hjk : a j < a k) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo (a j) (a k)) (hj : -1 < ∑ i : ι with a i = a j, e i) (hk : -1 < ∑ i : ι with a i = a k, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Ioo (a j) (a k) = openSegment ℝ (schwarzChristoffelVertex a e z₀ j) (schwarzChristoffelVertex a e z₀ k)

The interiors of the straight sides of the Schwarz--Christoffel polygon. Between two prevertices with no prevertex of nonzero exponent strictly between them, and with both total exponents greater than -1, the open boundary arc is exactly the open segment joining the two Schwarz--Christoffel vertices.

theorem TauCeti.schwarzChristoffelVertex_ne {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {j k : ι} (hjk : a j < a k) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo (a j) (a k)) (hj : -1 < ∑ i : ι with a i = a j, e i) (hk : -1 < ∑ i : ι with a i = a k, e i) : schwarzChristoffelVertex a e z₀ j ≠ schwarzChristoffelVertex a e z₀ k

A Schwarz--Christoffel side is nondegenerate. Two prevertices with no prevertex of nonzero exponent strictly between them, and with both total exponents greater than -1, carry distinct vertices.