The infinite rays of a Schwarz--Christoffel boundary

When the total turning exponent is at least -1, the two outer boundary edges have infinite length. Each traces an entire closed ray from its finite endpoint: the right ray points in the positive real direction, and the left ray points in direction -exp (π * (∑ i, e i) * I). The local exponent sum at the finite endpoint must exceed -1, so that the endpoint is attained.

For ordered prevertices, these two rays and the segments between consecutive finite vertices give the complete range of the boundary map. This identifies the polygonal chain parametrized by that map; it does not assert simplicity, interior injectivity, or equality with the frontier of the interior image.

Main results

• TauCeti.schwarzChristoffelBoundary_image_Ici_eq_ray and TauCeti.schwarzChristoffelBoundary_image_Iic_eq_ray identify the two outer edge images.
• TauCeti.range_schwarzChristoffelBoundary_of_neg_one_le_sum identifies the entire boundary range as the union of the finite sides and the two infinite rays.

References

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

theorem TauCeti.schwarzChristoffelBoundary_image_Ici_eq_ray {ι : 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 : -1 ≤ ∑ i : ι, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Ici p = (fun (t : ℝ) => schwarzChristoffelBoundary a e z₀ p + ↑t) '' Set.Ici 0

The right outer Schwarz--Christoffel edge is an infinite ray. If the total exponent is at least -1, all prevertices with nonzero exponent lie at or to the left of p, and the exponent sum at p is greater than -1, the boundary map on Ici p traces the full positive horizontal ray starting at its value at p.

theorem TauCeti.schwarzChristoffelBoundary_image_Ici_eq_ray_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 : -1 ≤ ∑ i : ι, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Ici (a j) = (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ j + ↑t) '' Set.Ici 0

The right outer ray based at a prevertex starts at its corresponding Schwarz--Christoffel vertex.

theorem TauCeti.schwarzChristoffelBoundary_image_Iic_eq_ray {ι : 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 : -1 ≤ ∑ i : ι, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Iic p = (fun (t : ℝ) => schwarzChristoffelBoundary a e z₀ p - ↑t * Complex.exp (↑Real.pi * ↑(∑ i : ι, e i) * Complex.I)) '' Set.Ici 0

The left outer Schwarz--Christoffel edge is an infinite ray. If the total exponent is at least -1, all prevertices with nonzero exponent lie at or to the right of p, and the exponent sum at p is greater than -1, the boundary map on Iic p traces the full ray from its value at p in direction -exp (π * (∑ i, e i) * I).

theorem TauCeti.schwarzChristoffelBoundary_image_Iic_eq_ray_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 : -1 ≤ ∑ i : ι, e i) : schwarzChristoffelBoundary a e z₀ '' Set.Iic (a j) = (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ j - ↑t * Complex.exp (↑Real.pi * ↑(∑ i : ι, e i) * Complex.I)) '' Set.Ici 0

The left outer ray based at a prevertex starts at its corresponding Schwarz--Christoffel vertex.

theorem TauCeti.range_schwarzChristoffelBoundary_of_neg_one_le_sum {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (j : Fin (n + 1)), -1 < ∑ i : Fin (n + 1) with a i = a j, e i) (hS : -1 ≤ ∑ i : Fin (n + 1), e i) : Set.range (schwarzChristoffelBoundary a e z₀) = ((fun (t : ℝ) => schwarzChristoffelVertex a e z₀ 0 - ↑t * Complex.exp (↑Real.pi * ↑(∑ i : Fin (n + 1), e i) * Complex.I)) '' Set.Ici 0 ∪ ⋃ (i : Fin n), segment ℝ (schwarzChristoffelVertex a e z₀ i.castSucc) (schwarzChristoffelVertex a e z₀ i.succ)) ∪ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ (Fin.last n) + ↑t) '' Set.Ici 0

An unbounded Schwarz--Christoffel boundary is a chain of finite sides and two rays. For ordered prevertices with integrable finite exponent sums and total exponent at least -1, the complete boundary range consists of the consecutive vertex segments, a horizontal ray from the last vertex, and a ray from the first vertex in direction -exp (π * (∑ i, e i) * I). The formula does not require the chain to be simple.