Documentation

TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Infinity.Power

Power growth of Schwarz--Christoffel primitives at infinity #

When the total turning exponent S is greater than -1, the Schwarz--Christoffel primitive has the leading asymptotic

F(z) / z ^ (S + 1) → 1 / (S + 1)

as z tends to infinity through the whole upper half-plane. In particular, the primitive escapes every bounded subset of the plane, uniformly even for approaches tangential to the real axis. Together with the logarithmic endpoint S = -1, this supplies the growth estimate used in properness arguments for maps onto unbounded polygonal domains.

The proof integrates the uniform integrand asymptotic along radial segments. Their inner endpoints lie on a fixed upper semicircle, where the primitive is bounded; no integrability condition at the finite prevertices is needed.

References #

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_div_cpow_atInfinity_of_neg_one_lt_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : -1 < ∑ i : ι, e i) :
Filter.Tendsto (fun (z : ℂ) => schwarzChristoffelPrimitive a e z₀ z / z ^ ↑(∑ i : ι, e i + 1)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (↑(∑ i : ι, e i + 1))⁻¹)

Power asymptotic at infinity. If the total turning exponent is greater than -1, the Schwarz--Christoffel primitive is asymptotic to z ^ ((∑ i, e i) + 1) / ((∑ i, e i) + 1) throughout the upper half-plane. No ordering, distinctness, or sign assumptions on the finite data are needed.

Uniform escape in the power-growth case. If the total turning exponent is greater than -1, the Schwarz--Christoffel primitive tends to infinity through the entire upper half-plane.

Uniform escape in the complete nonintegrable range. If the total turning exponent is at least -1, the Schwarz--Christoffel primitive tends to infinity through the entire upper half-plane. The endpoint is logarithmic and the strict range has power growth.