Corner asymptotics of the Schwarz--Christoffel map

At a real boundary point p carrying total exponent t > -1, the Schwarz--Christoffel integrand is asymptotic to C * (z - p) ^ t, where C is the nonzero prevertex coefficient. This file integrates that derivative asymptotic and identifies the first-order power law of the normalized primitive:

F z - F p ~ (C / (t + 1)) * (z - p) ^ (t + 1).

The limit is taken through the whole upper half-plane. In particular, it records both the vanishing order at the corner and its leading direction, information needed to identify the boundary chain of a Schwarz--Christoffel map with a polygon.

Main result

• TauCeti.tendsto_schwarzChristoffelPrimitive_sub_boundary_div_cpow -- the normalized primitive has the expected leading power at an integrable real boundary point.
• TauCeti.tendsto_schwarzChristoffelPrimitive_sub_vertex_div_cpow -- the corresponding indexed prevertex form.

References

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

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_sub_boundary_div_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (p : ℝ) (he : -1 < ∑ i : ι with a i = p, e i) : Filter.Tendsto (fun (z : ℂ) => (schwarzChristoffelPrimitive a e z₀ z - schwarzChristoffelBoundary a e z₀ p) / (z - ↑p) ^ ↑(∑ i : ι with a i = p, e i + 1)) (nhdsWithin (↑p) UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelPrevertexCoefficient a e p / (↑(∑ i : ι with a i = p, e i) + 1)))

Leading boundary asymptotic of the Schwarz--Christoffel primitive. At a real point whose total exponent t is greater than -1, subtracting its boundary value and dividing by (z - p) ^ (t + 1) tends, through the whole upper half-plane, to the integrand's nonzero leading coefficient divided by t + 1. Coincident prevertices contribute through the sum of all their exponents at p.

Thus the primitive has the expected power law F z - F p ~ (C / (t + 1)) * (z - p) ^ (t + 1) at the corner.

theorem TauCeti.tendsto_schwarzChristoffelPrimitive_sub_vertex_div_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j : ι) (he : -1 < ∑ i : ι with a i = a j, e i) : Filter.Tendsto (fun (z : ℂ) => (schwarzChristoffelPrimitive a e z₀ z - schwarzChristoffelVertex a e z₀ j) / (z - ↑(a j)) ^ ↑(∑ i : ι with a i = a j, e i + 1)) (nhdsWithin (↑(a j)) UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelPrevertexCoefficient a e (a j) / (↑(∑ i : ι with a i = a j, e i) + 1)))

Leading corner asymptotic of the Schwarz--Christoffel primitive. At an indexed prevertex whose total exponent is greater than -1, the canonical boundary value in tendsto_schwarzChristoffelPrimitive_sub_boundary_div_cpow is its Schwarz--Christoffel vertex.