The half-strip end of a logarithmic Schwarz--Christoffel image

When the total turning exponent is -1, the two outer boundary rays are horizontal, point to the right, and have heights im c and im c + π, where c is the logarithmic constant at infinity. The boundary agrees with these two lines sufficiently far to the right, without any simplicity assumption.

If the boundary is simple, the image of the upper half-plane agrees there with the open strip between those lines. Thus the direct mapping theorem gives a polygonal domain with an actual half-strip end, rather than only a complementary-component description.

References

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

theorem TauCeti.exists_mem_range_schwarzChristoffelBoundary_iff_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hsum : ∑ i : ι, e i = -1) : ∃ (R : ℝ), ∀ (w : ℂ), R < w.re → (w ∈ Set.range (schwarzChristoffelBoundary a e z₀) ↔ w.im = (schwarzChristoffelLogConstantAtInfinity a e z₀).im ∨ w.im = (schwarzChristoffelLogConstantAtInfinity a e z₀).im + Real.pi)

With total exponent -1, sufficiently far to the right the real boundary range is exactly the pair of horizontal lines at heights im c and im c + π. Repeated prevertices and nonsimple boundary chains are allowed.

theorem TauCeti.exists_mem_image_schwarzChristoffelPrimitive_iff_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hsum : ∑ i : ι, e i = -1) (hinj : Function.Injective (schwarzChristoffelBoundary a e z₀)) : ∃ (R : ℝ), ∀ (w : ℂ), R < w.re → (w ∈ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ↔ (schwarzChristoffelLogConstantAtInfinity a e z₀).im < w.im ∧ w.im < (schwarzChristoffelLogConstantAtInfinity a e z₀).im + Real.pi)

The half-strip end of a simple logarithmic Schwarz--Christoffel map. For integrable finite prevertices, total exponent -1, and an injective real boundary parametrization, the image sufficiently far to the right is exactly the open strip of width π between the heights im c and im c + π. No ordering or sign assumption on the finite data is needed.