Separation of logarithmic Schwarz--Christoffel ends

When the total turning exponent is -1, assume the left and right finite endpoints bound every prevertex with nonzero exponent from below and above, respectively, and that the exponent sum at each endpoint is greater than -1 (endpoint integrability). Then the two outer sides of the normalized Schwarz--Christoffel boundary are parallel horizontal rays pointing to the right. Their heights are exactly im c and im c + π, where c is the logarithmic constant at infinity. Thus their supporting lines are distinct, with separation π.

The exact heights identify the two levels of a parallel-sided polygonal end. In particular, the outer boundary images are automatically disjoint under these hypotheses. The boundary-simplicity criterion therefore only needs to check intersections among bounded sides and between bounded sides and the outer rays. No simplicity of the bounded chain or interior univalence is inferred from the logarithmic asymptotic alone.

References

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

theorem TauCeti.im_schwarzChristoffelBoundary_of_forall_le_of_sum_eq_neg_one {ι : 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) (hsum : ∑ i : ι, e i = -1) : (schwarzChristoffelBoundary a e z₀ p).im = (schwarzChristoffelLogConstantAtInfinity a e z₀).im

The right outer side in the logarithmic case lies exactly at the height of the logarithmic constant at infinity. Only integrability at its finite endpoint is needed.

theorem TauCeti.im_schwarzChristoffelBoundary_of_forall_ge_of_sum_eq_neg_one {ι : 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 = -1) : (schwarzChristoffelBoundary a e z₀ p).im = (schwarzChristoffelLogConstantAtInfinity a e z₀).im + Real.pi

The left outer side in the logarithmic case lies exactly π above the height of the logarithmic constant at infinity. Only integrability at its finite endpoint is needed.

theorem TauCeti.disjoint_schwarzChristoffelBoundary_outer_images_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) (hleft : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hright : ∀ (i : ι), e i ≠ 0 → a i ≤ q) (hsum : ∑ i : ι, e i = -1) : Disjoint (schwarzChristoffelBoundary a e z₀ '' Set.Iic p) (schwarzChristoffelBoundary a e z₀ '' Set.Ici q)

The outer boundary images are disjoint when the total exponent is -1: they lie on horizontal lines separated by π. The finite prevertices need not be ordered or distinct.

theorem TauCeti.schwarzChristoffelBoundary_injective_of_edge_intersections_of_sum_eq_neg_one {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (k : Fin (n + 2)), -1 < ∑ l : Fin (n + 2) with a l = a k, e l) (hsum : ∑ k : Fin (n + 2), e k = -1) (hinter : ∀ (i j : Fin (n + 1)), i < j → ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc → ↑j = ↑i + 1 ∧ z = schwarzChristoffelVertex a e z₀ i.succ) (hleft : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ 0 + ↑t) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ 0) (hright : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ (Fin.last (n + 1)) + ↑t) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))) : Function.Injective (schwarzChristoffelBoundary a e z₀)

In the logarithmic case, a Schwarz--Christoffel boundary is simple if bounded sides meet only at consecutive vertices and each outer ray meets the bounded sides only at its finite endpoint. No additional intersection condition between the outer rays is needed.