Logarithmic growth of Schwarz--Christoffel primitives

When the total turning exponent is -1, the Schwarz--Christoffel primitive grows logarithmically. Subtracting the principal logarithm leaves a function holomorphic in the reciprocal coordinate at zero for points in the upper half-plane. Consequently the difference has a finite limit at infinity, with first correction (∑ i, e i * a i) / z, and the primitive escapes every bounded set. All limits hold through the whole upper half-plane, including tangential approaches to its real boundary. This is the logarithmic endpoint of the growth estimates used to establish properness of maps onto unbounded polygonal domains.

The same asymptotic holds for the canonical boundary values on the real axis beyond every prevertex: the right end is asymptotic to log x + c and the left end to log (-x) + c + pi * I, where c is the logarithmic constant at infinity. The term pi * I is for the normalized primitive, whose integrand has leading coefficient one at infinity; an affine postcomposition rotates and rescales it.

References

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

noncomputable def TauCeti.schwarzChristoffelLogConstantAtInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : ℂ

The constant term after subtracting the principal logarithm from the Schwarz--Christoffel primitive at infinity. It is a genuine limit through the upper half-plane when the total turning exponent is -1.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_sub_log_atInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (fun (z : ℂ) => schwarzChristoffelPrimitive a e z₀ z - Complex.log z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelLogConstantAtInfinity a e z₀))

The logarithmic remainder tends to its constant term through the entire upper half-plane.

theorem TauCeti.tendsto_mul_schwarzChristoffelPrimitive_sub_log_sub_logConstantAtInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (fun (z : ℂ) => z * (schwarzChristoffelPrimitive a e z₀ z - Complex.log z - schwarzChristoffelLogConstantAtInfinity a e z₀)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (∑ i : ι, ↑(e i) * ↑(a i)))

The first correction to the logarithmic asymptotic is the weighted sum of prevertices, uniformly over all directions in the upper half-plane.

theorem TauCeti.schwarzChristoffelLogConstantAtInfinity_change_base {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (b c : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : schwarzChristoffelLogConstantAtInfinity a e b = schwarzChristoffelLogConstantAtInfinity a e c - schwarzChristoffelPrimitive a e c ↑b

Changing the base point translates the logarithmic constant by the same constant as the primitive.

theorem TauCeti.tendsto_re_schwarzChristoffelPrimitive_atTop_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (fun (z : ℂ) => (schwarzChristoffelPrimitive a e z₀ z).re) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) Filter.atTop

In the logarithmic case the real part of the Schwarz--Christoffel primitive tends to positive infinity through the entire upper half-plane.

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_atInfinity_cobounded_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (Bornology.cobounded ℂ)

Uniform escape in the logarithmic case. A Schwarz--Christoffel primitive with total turning exponent -1 tends to infinity through the entire upper half-plane.

Logarithmic asymptotics on the boundary

theorem TauCeti.tendsto_schwarzChristoffelBoundary_sub_log_atTop_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (fun (x : ℝ) => schwarzChristoffelBoundary a e z₀ x - ↑(Real.log x)) Filter.atTop (nhds (schwarzChristoffelLogConstantAtInfinity a e z₀))

On the right outer edge, the normalized Schwarz--Christoffel boundary has the asymptotic log x + c, where c is its logarithmic constant at infinity.

theorem TauCeti.tendsto_schwarzChristoffelBoundary_sub_log_neg_atBot_of_sum_eq_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = -1) : Filter.Tendsto (fun (x : ℝ) => schwarzChristoffelBoundary a e z₀ x - ↑(Real.log (-x))) Filter.atBot (nhds (schwarzChristoffelLogConstantAtInfinity a e z₀ + ↑Real.pi * Complex.I))

On the left outer edge, the normalized Schwarz--Christoffel boundary has the asymptotic log (-x) + c + pi * I. The extra term comes from the argument pi of the principal logarithm's boundary value from the upper half-plane on the negative real axis.