The Schwarz--Christoffel vertex at infinity

The real axis is only part of the boundary of the upper half-plane: the prevertices divide it into finitely many bounded intervals and two unbounded ones, and the two unbounded ones are a single boundary arc through the point at infinity. The polygon a Schwarz--Christoffel map is meant to parametrize can therefore close up only if the map has a limit at infinity, and this file proves that it does, under the hypothesis that the total turning exponent ∑ i, e i is less than -1. That hypothesis is the classical closing condition: for a bounded polygon with interior angles α i and no prevertex at infinity, e i = α i / π - 1 and the angle sum forces ∑ i, e i = -2.

Far from all the prevertices, dist z (a i) is caught between ‖z‖ / 2 and 2 ‖z‖, so the integrand ∏ i, (z - a i) ^ (e i) is bounded by C * ‖z‖ ^ ∑ i, e i (TauCeti.exists_norm_schwarzChristoffelIntegrand_le_of_le_norm), for any exponents whatever. Only the sign of ∑ i, e i makes that a decay estimate, and with ∑ i, e i < -1 the dominating function is integrable along a vertical ray, and the map is estimated between any two far-away points of the half-plane by running up a vertical ray from the first, across a horizontal segment at the common height ‖z‖ + ‖w‖, and back down to the second: all three pieces stay far from the prevertices, and all three contributions are O(R ^ (∑ i, e i + 1)) when both points have norm at least R. That is the Cauchy criterion along cobounded ℂ ⊓ 𝓟 upperHalfPlaneSet, and completeness of ℂ turns it into the limit TauCeti.schwarzChristoffelVertexAtInfinity.

The boundary consequence is TauCeti.tendsto_schwarzChristoffelBoundaryValue_atInfinity: any family of boundary values of the map along the real axis converges to that same point as the real parameter leaves every bounded set. Applied to the two unbounded boundary intervals it says that the two unbounded image edges run to one and the same point, which is what closes the boundary path up into a polygon; identifying the closed path with a prescribed polygon, and the image of the half-plane with its interior, is left to later work.

Main definitions

• TauCeti.schwarzChristoffelVertexAtInfinity -- the boundary value of the Schwarz--Christoffel primitive at the point at infinity.

Main results

• TauCeti.exists_norm_schwarzChristoffelIntegrand_le_of_le_norm -- far from every prevertex the integrand is dominated by a constant multiple of ‖z‖ ^ ∑ i, e i.
• TauCeti.tendsto_schwarzChristoffelPrimitive_atInfinity -- the map converges to schwarzChristoffelVertexAtInfinity along the upper half-plane at infinity.
• TauCeti.schwarzChristoffelVertexAtInfinity_change_base -- changing the base point translates that boundary value by the same constant as every other one.
• TauCeti.tendsto_schwarzChristoffelBoundaryValue_atInfinity -- boundary values along the real axis converge to it, and hence TauCeti.tendsto_limUnder_schwarzChristoffelPrimitive_atTop and TauCeti.tendsto_limUnder_schwarzChristoffelPrimitive_atBot: the two unbounded image edges close up at one point.

References

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

The size of the integrand at infinity

theorem TauCeti.exists_norm_schwarzChristoffelIntegrand_le_of_le_norm {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : ∃ C > 0, ∃ R > 0, ∀ (z : ℂ), R ≤ ‖z‖ → ‖schwarzChristoffelIntegrand a e z‖ ≤ C * ‖z‖ ^ ∑ i : ι, e i

The Schwarz--Christoffel integrand is bounded by a multiple of ‖z‖ ^ ∑ i, e i at infinity. Once ‖z‖ is large compared with the prevertices, every distance dist z (a i) lies between ‖z‖ / 2 and 2 ‖z‖, so each factor dist z (a i) ^ e i differs from ‖z‖ ^ e i by at most the fixed factor 2 ^ |e i|. No sign hypothesis is placed on e, so the bound is a genuine decay estimate only when ∑ i, e i < 0.

Displacement along segments of the half-plane

The limit at infinity

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

The Schwarz--Christoffel vertex at infinity: the boundary value at the point at infinity of the primitive normalized at z₀. It is a genuine limit when the total turning exponent ∑ i, e i is less than -1, which is the classical condition for the image polygon to close up.

Equations

• TauCeti.schwarzChristoffelVertexAtInfinity a e z₀ = (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet).limUnder (TauCeti.schwarzChristoffelPrimitive a e z₀)

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

The Schwarz--Christoffel primitive converges to schwarzChristoffelVertexAtInfinity along the upper half-plane at infinity.

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

Changing the base point translates the Schwarz--Christoffel vertex at infinity by the same constant as every finite boundary value.

Closing the boundary path up

theorem TauCeti.tendsto_schwarzChristoffelBoundaryValue_atInfinity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hS : ∑ i : ι, e i < -1) {l : Filter ℝ} {L : ℝ → ℂ} (hl : Filter.Tendsto (fun (x : ℝ) => |x|) l Filter.atTop) (hL : ∀ᶠ (x : ℝ) in l, Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds (L x))) : Filter.Tendsto L l (nhds (schwarzChristoffelVertexAtInfinity a e z₀))

Boundary values of the Schwarz--Christoffel map converge to its vertex at infinity. If L x is the boundary value at the real point x — the limit of the map along the upper half-plane at x — for all x in a filter along which |x| tends to infinity, then L tends to schwarzChristoffelVertexAtInfinity along that filter.

theorem TauCeti.tendsto_limUnder_schwarzChristoffelPrimitive_atTop {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hS : ∑ i : ι, e i < -1) : Filter.Tendsto (fun (x : ℝ) => (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet).limUnder (schwarzChristoffelPrimitive a e z₀)) Filter.atTop (nhds (schwarzChristoffelVertexAtInfinity a e z₀))

The right-hand unbounded image edge of the Schwarz--Christoffel map runs to its vertex at infinity. Beyond every prevertex the map has a boundary value at each real point, by the straight-edge continuation, and those values converge to the vertex at infinity.

theorem TauCeti.tendsto_limUnder_schwarzChristoffelPrimitive_atBot {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hS : ∑ i : ι, e i < -1) : Filter.Tendsto (fun (x : ℝ) => (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet).limUnder (schwarzChristoffelPrimitive a e z₀)) Filter.atBot (nhds (schwarzChristoffelVertexAtInfinity a e z₀))

The left-hand unbounded image edge of the Schwarz--Christoffel map runs to its vertex at infinity. Together with tendsto_limUnder_schwarzChristoffelPrimitive_atTop this closes the boundary path up: the two unbounded image edges have one and the same endpoint.