Complex asymptotics of the Schwarz--Christoffel integrand at infinity

Writing S = ∑ i, e i, the integrand has the expansion

schwarzChristoffelIntegrand a e z / z ^ S = 1 - (∑ i, e i * a i) / z + o(1 / z)

as z tends to infinity through the whole upper half-plane. In particular, the normalized integrand tends to one, with error O(1 / z). These estimates retain the complex phase, even for approaches arbitrarily close to the negative real axis. They provide derivative estimates for the power-law growth of the primitive and for properness of unbounded polygonal maps.

The normalization equals ∏ i, (1 - a i / z) ^ e i on the upper half-plane. This product is holomorphic as a function of 1 / z near zero; its value and derivative there give the two terms. No ordering, distinctness, integrability, or sign conditions on the data are needed.

References

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

theorem TauCeti.schwarzChristoffelIntegrand_div_cpow_eq_prod {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelIntegrand a e z / z ^ ↑(∑ i : ι, e i) = ∏ i : ι, (1 - ↑(a i) * z⁻¹) ^ ↑(e i)

Dividing the Schwarz--Christoffel integrand by its total power gives a product in the reciprocal coordinate. This identity uses the principal branches on the upper half-plane.

theorem TauCeti.tendsto_mul_schwarzChristoffelIntegrand_div_cpow_sub_one_atInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : Filter.Tendsto (fun (z : ℂ) => z * (schwarzChristoffelIntegrand a e z / z ^ ↑(∑ i : ι, e i) - 1)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (-∑ i : ι, ↑(e i) * ↑(a i)))

First correction at infinity. The coefficient of 1 / z in the normalized Schwarz--Christoffel integrand is the negative weighted sum of the real prevertices. The limit holds uniformly over all directions in the upper half-plane.

theorem TauCeti.tendsto_schwarzChristoffelIntegrand_div_cpow_atInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : Filter.Tendsto (fun (z : ℂ) => schwarzChristoffelIntegrand a e z / z ^ ↑(∑ i : ι, e i)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds 1)

Complex leading term at infinity. The Schwarz--Christoffel integrand divided by z ^ (∑ i, e i) tends to one through the entire upper half-plane.

theorem TauCeti.isBigO_schwarzChristoffelIntegrand_div_cpow_sub_one_atInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : (fun (z : ℂ) => schwarzChristoffelIntegrand a e z / z ^ ↑(∑ i : ι, e i) - 1) =O[Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet] fun (z : ℂ) => z⁻¹

The relative error of the leading power of the Schwarz--Christoffel integrand is O(1 / z) throughout the upper half-plane at infinity.