Divergence of Schwarz--Christoffel boundary values at infinity

For Schwarz--Christoffel data with total exponent S = ∑ i, e i, the boundary density is asymptotic to |x| ^ S at either end of the real axis. Consequently, when -1 ≤ S, the two outer boundary edges have infinite length and their boundary values escape every bounded set.

This is the counterpart to the finite vertex-at-infinity theory of TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Infinity.Basic, which applies when S < -1. The two regimes decide whether the point at infinity of the upper half-plane is sent to a finite vertex (S < -1) or to a vertex at infinity (-1 ≤ S, this file).

Main results

• TauCeti.tendsto_schwarzChristoffelDensity_div_rpow_atTop and TauCeti.tendsto_schwarzChristoffelDensity_div_rpow_atBot identify the leading term of the boundary density at both ends of the real axis.
• TauCeti.tendsto_integral_schwarzChristoffelDensity_atTop and TauCeti.tendsto_integral_schwarzChristoffelDensity_atBot show that the two outer boundary edges have infinite length when the total exponent is at least -1.
• TauCeti.tendsto_schwarzChristoffelBoundary_atTop_cobounded and TauCeti.tendsto_schwarzChristoffelBoundary_atBot_cobounded show that the boundary values on those edges tend to the cobounded filter of ℂ.
• TauCeti.isProperMap_schwarzChristoffelBoundary -- when also every finite prevertex is integrable, the boundary map ℝ → ℂ is proper; in particular its range is closed.

References

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

theorem TauCeti.tendsto_schwarzChristoffelDensity_div_rpow_atTop {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : Filter.Tendsto (fun (x : ℝ) => schwarzChristoffelDensity a e x / x ^ ∑ i : ι, e i) Filter.atTop (nhds 1)

Asymptotic boundary density at positive infinity. The Schwarz--Christoffel density is asymptotic to x ^ (∑ i, e i) as x → +∞.

theorem TauCeti.tendsto_schwarzChristoffelDensity_div_rpow_atBot {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : Filter.Tendsto (fun (x : ℝ) => schwarzChristoffelDensity a e x / (-x) ^ ∑ i : ι, e i) Filter.atBot (nhds 1)

Asymptotic boundary density at negative infinity. The Schwarz--Christoffel density is asymptotic to (-x) ^ (∑ i, e i) as x → -∞.

theorem TauCeti.tendsto_integral_schwarzChristoffelDensity_atTop {ι : Type u_1} [Fintype ι] {a e : ι → ℝ} {p : ℝ} (hp : ∀ (i : ι), e i ≠ 0 → a i < p) (hsum : -1 ≤ ∑ i : ι, e i) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in p..x, schwarzChristoffelDensity a e t) Filter.atTop Filter.atTop

The right-hand outer edge has infinite length. If the total turning exponent is at least -1, the integral of the boundary density from any point to the right of every prevertex with a nonzero exponent tends to infinity at positive infinity.

theorem TauCeti.tendsto_integral_schwarzChristoffelDensity_atBot {ι : Type u_1} [Fintype ι] {a e : ι → ℝ} {p : ℝ} (hp : ∀ (i : ι), e i ≠ 0 → p < a i) (hsum : -1 ≤ ∑ i : ι, e i) : Filter.Tendsto (fun (x : ℝ) => ∫ (t : ℝ) in x..p, schwarzChristoffelDensity a e t) Filter.atBot Filter.atTop

The left-hand outer edge has infinite length. If the total turning exponent is at least -1, the integral of the boundary density up to any point to the left of every prevertex with a nonzero exponent tends to infinity at negative infinity.

theorem TauCeti.tendsto_schwarzChristoffelBoundary_atTop_cobounded {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : -1 ≤ ∑ i : ι, e i) : Filter.Tendsto (schwarzChristoffelBoundary a e z₀) Filter.atTop (Bornology.cobounded ℂ)

A Schwarz--Christoffel boundary edge escapes at positive infinity. If the total turning exponent is at least -1, the canonical boundary values on the right-hand outer edge tend to the cobounded filter of the complex plane.

theorem TauCeti.tendsto_schwarzChristoffelBoundary_atBot_cobounded {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : -1 ≤ ∑ i : ι, e i) : Filter.Tendsto (schwarzChristoffelBoundary a e z₀) Filter.atBot (Bornology.cobounded ℂ)

A Schwarz--Christoffel boundary edge escapes at negative infinity. If the total turning exponent is at least -1, the canonical boundary values on the left-hand outer edge tend to the cobounded filter of the complex plane.

theorem TauCeti.isProperMap_schwarzChristoffelBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hsum : -1 ≤ ∑ i : ι, e i) : IsProperMap (schwarzChristoffelBoundary a e z₀)

The Schwarz--Christoffel boundary map is proper when every finite prevertex is integrable and the total turning exponent is at least -1: it is continuous on all of ℝ and escapes every bounded set at both ends of the real axis.