The second correction to the Schwarz--Christoffel integrand at infinity

Write S = ∑ i, e i, M = ∑ i, e i * a i, and C = (M ^ 2 - ∑ i, e i * a i ^ 2) / 2. The normalized integrand has expansion

integrand(z) / z ^ S = 1 - M / z + C / z ^ 2 + o(1 / z ^ 2).

The limit holds through the whole upper half-plane, including tangential approaches to the real axis. No ordering, distinctness, integrability, or sign conditions on the finite data are required.

At total exponent S = 1, this gives integrand(z) = z - M + C / z + o(1 / z). The coefficient C is therefore the logarithmic coefficient when the primitive's quadratic and linear leading terms are removed. This is the analytic input for separating the parallel outer sides of a polygonal end of opening 2π; the leading quadratic term alone does not distinguish their supporting lines. No asymptotic for the primitive or boundary separation is claimed here.

References

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

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

Second correction at infinity. The quadratic coefficient of the normalized Schwarz--Christoffel integrand is half the difference between the square of the first weighted moment and the second weighted moment of the prevertices. The limit is uniform in direction within the upper half-plane.

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

The integrand at an end of opening 2π. At total exponent one, subtracting the linear and constant terms leaves a 1 / z term with the explicit real coefficient displayed in the conclusion. This coefficient becomes a logarithmic term after integration.