The pre-Schwarzian at an end of opening 2 * π

Let f map the upper half-plane conformally onto a domain U, extend to a continuous injection of the closed upper half-plane, and tend to infinity at infinity. Suppose that far out U coincides with the exterior of the closed half-strip {0 ≤ re ζ, 0 ≤ im ζ ≤ π} in the coordinate ζ = (z - c) / b: the two unbounded sides of U are parallel rays pointing in the same direction, and U surrounds the half-strip between them, so its end at infinity has opening 2 * π. Then z * f''(z) / f'(z) → 1 as z tends to infinity in the upper half-plane (TauCeti.tendsto_mul_logDeriv_deriv_upperHalfPlaneSet_of_halfStripExterior).

Unlike a sector or a half-strip, the exterior of a half-strip has no elementary straightening coordinate. Instead f is compared with the explicit model map ζ ↦ ζ ^ 2 / 2 - log ζ + π * I, which carries the far part of the closed upper half-plane injectively into that exterior, with the far positive and negative real axes going to the two sides. The comparison map f⁻¹ ∘ (c + b * model) fixes infinity, is real on the far real axis, and so is conformal across infinity by Schwarz reflection; the model has ζ * model''(ζ) / model'(ζ) → 1, and TauCeti.tendsto_mul_logDeriv_deriv_upperHalfPlaneSet_of_eqOn_comp_neg_inv transfers this limit to f. For a Schwarz--Christoffel map the limit is the sum of the finite turning exponents.

References

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

The model map

The comparison with the model

theorem TauCeti.tendsto_mul_logDeriv_deriv_upperHalfPlaneSet_of_halfStripExterior {U : Set ℂ} {f : ℂ → ℂ} {ρ : ℝ} {c b : ℂ} (hb : b ≠ 0) (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hU : ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ ((z - c) / b).re < 0 ∨ ((z - c) / b).im ∉ Set.Icc 0 Real.pi)) : Filter.Tendsto (fun (z : ℂ) => z * logDeriv (deriv f) z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds 1)

The pre-Schwarzian at an end of opening 2 * π. Let f map the upper half-plane holomorphically onto U, extend to a continuous injection of the closed upper half-plane, and tend to infinity at infinity, and let U coincide far from c with the exterior of the closed half-strip {0 ≤ re ((z - c) / b), 0 ≤ im ((z - c) / b) ≤ π}. Then z * f''(z) / f'(z) → 1 as z tends to infinity in the upper half-plane.

So the two parallel unbounded sides of U bound a vertex at infinity of opening 2 * π, and for a Schwarz--Christoffel map the finite turning exponents then sum to 1.