Logarithmic Schwarz--Christoffel ends at finite prevertices

A real prevertex with total exponent -1 represents an end at infinity, not a finite polygon vertex. If C is its nonzero prevertex coefficient, the normalized primitive has local form C * log (z - p) + H z, with H holomorphic across p. In particular the primitive escapes to infinity along every approach to p through the upper half-plane, including tangential approaches. The normalized remainder commutes with conjugation, which gives a real-symmetric exponential coordinate at the end.

These local ends allow Schwarz--Christoffel data to describe polygons with several vertices at infinity. The results impose no integrability conditions at the other prevertices, and coincident prevertices are handled by summing their exponents. They do not assert global univalence or identify the image domain.

References

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

theorem TauCeti.exists_analyticOnNhd_eq_schwarzChristoffelPrimitive_sub_log_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : ∑ i : ι with a i = p, e i = -1) : ∃ (H : ℂ → ℂ) (r : ℝ), 0 < r ∧ AnalyticOnNhd ℂ H (Metric.ball (↑p) r) ∧ (∀ z ∈ Metric.ball (↑p) r, (H ((starRingEnd ℂ) z) - H ↑p) / schwarzChristoffelPrevertexCoefficient a e p = (starRingEnd ℂ) ((H z - H ↑p) / schwarzChristoffelPrevertexCoefficient a e p)) ∧ ∀ z ∈ Metric.ball (↑p) r ∩ UpperHalfPlane.upperHalfPlaneSet, schwarzChristoffelPrimitive a e z₀ z - schwarzChristoffelPrevertexCoefficient a e p * Complex.log (z - ↑p) = H z

At a real prevertex with total exponent -1, subtracting the prevertex coefficient times log (z - p) from the Schwarz--Christoffel primitive gives a holomorphic function across that prevertex. The equality holds on an entire upper half-disc, not just along a ray. After subtracting its value at p and dividing by the coefficient, the holomorphic remainder commutes with conjugation on the full disc.

theorem TauCeti.tendsto_re_schwarzChristoffelPrimitive_div_coefficient_atBot_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : ∑ i : ι with a i = p, e i = -1) : Filter.Tendsto (fun (z : ℂ) => (schwarzChristoffelPrimitive a e z₀ z / schwarzChristoffelPrevertexCoefficient a e p).re) (nhdsWithin (↑p) UpperHalfPlane.upperHalfPlaneSet) Filter.atBot

After dividing by its nonzero prevertex coefficient, a logarithmic Schwarz--Christoffel end has real part tending to negative infinity, uniformly over upper-half-plane approaches.

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_cobounded_of_prevertex_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : ∑ i : ι with a i = p, e i = -1) : Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑p) UpperHalfPlane.upperHalfPlaneSet) (Bornology.cobounded ℂ)

Escape at a logarithmic prevertex. If the total exponent at a real point is -1, the Schwarz--Christoffel primitive tends to infinity there through the whole upper half-plane. No assumptions on the other exponents or on global injectivity are needed.