Quadratic growth of Schwarz--Christoffel primitives and ends of opening 2π

Write M = ∑ i, e i * a i and C = (M ^ 2 - ∑ i, e i * a i ^ 2) / 2. When the total turning exponent is 1, the Schwarz--Christoffel primitive has the expansion

F(z) = z ^ 2 / 2 - M * z + C * log z + c + o(1)

as z tends to infinity through the whole upper half-plane, including tangential approaches to the real axis. After subtracting these three terms, the primitive is holomorphic in the reciprocal coordinate -1 / z at zero.

The same expansion holds for the canonical boundary values on the real axis beyond every prevertex, with log x on the right and log (-x) + π * I on the left. Consequently the two outer sides of the normalized boundary are horizontal rays pointing to the right, at the heights im c and im c + π * C. They are disjoint exactly when C ≠ 0; when C = 0 they overlap, as for the slit plane z ↦ z ^ 2. Thus π * C is the signed distance between the supporting lines of the two parallel outer sides of an end of opening 2π, and C ≠ 0 replaces the outer-ray disjointness condition of the boundary-simplicity criterion.

When C < 0, far out in the upper half-plane, the comparison function z ^ 2 / 2 - M * z + C * log z takes no value with real part greater than 1 / 2 in a band strictly between the heights π * C and 0 that stays a fixed distance away from both.

References

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

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

The constant term of a Schwarz--Christoffel primitive at infinity after subtracting its quadratic, linear and logarithmic terms. 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_quadratic_atInfinity_of_sum_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hsum : ∑ i : ι, e i = 1) : Filter.Tendsto (fun (z : ℂ) => schwarzChristoffelPrimitive a e z₀ z - (z ^ 2 / 2 - (∑ i : ι, ↑(e i) * ↑(a i)) * z + ((∑ i : ι, ↑(e i) * ↑(a i)) ^ 2 - ∑ i : ι, ↑(e i) * ↑(a i) ^ 2) / 2 * Complex.log z)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelQuadraticConstantAtInfinity a e z₀))

Quadratic asymptotic at infinity. If the total turning exponent is 1, then F(z) - (z ^ 2 / 2 - M * z + C * log z) has a finite limit through the entire upper half-plane, where M = ∑ i, e i * a i and C = (M ^ 2 - ∑ i, e i * a i ^ 2) / 2.

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

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

Quadratic asymptotics on the boundary

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

On the right outer edge, the normalized Schwarz--Christoffel boundary with total exponent one has the asymptotic x ^ 2 / 2 - M * x + C * log x + c, where c is the quadratic constant at infinity.

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

On the left outer edge, the normalized Schwarz--Christoffel boundary with total exponent one has the asymptotic x ^ 2 / 2 - M * x + C * log (-x) + c + C * π * I. The extra term comes from the argument π of the principal logarithm's boundary value from the upper half-plane on the negative real axis.

The outer sides of an end of opening 2π

theorem TauCeti.im_schwarzChristoffelBoundary_of_forall_le_of_sum_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hsum : ∑ i : ι, e i = 1) : (schwarzChristoffelBoundary a e z₀ p).im = (schwarzChristoffelQuadraticConstantAtInfinity a e z₀).im

The right outer side of a Schwarz--Christoffel boundary with total exponent one lies exactly at the height of the quadratic constant at infinity. Only integrability at its finite endpoint is needed.

theorem TauCeti.im_schwarzChristoffelBoundary_of_forall_ge_of_sum_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hsum : ∑ i : ι, e i = 1) : (schwarzChristoffelBoundary a e z₀ p).im = (schwarzChristoffelQuadraticConstantAtInfinity a e z₀).im + Real.pi * (((∑ i : ι, e i * a i) ^ 2 - ∑ i : ι, e i * a i ^ 2) / 2)

The left outer side of a Schwarz--Christoffel boundary with total exponent one lies exactly π * C above the height of the quadratic constant at infinity, where C = ((∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2) / 2. Only integrability at its finite endpoint is needed.

theorem TauCeti.disjoint_schwarzChristoffelBoundary_outer_images_iff_of_sum_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) (hleft : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hright : ∀ (i : ι), e i ≠ 0 → a i ≤ q) (hsum : ∑ i : ι, e i = 1) : Disjoint (schwarzChristoffelBoundary a e z₀ '' Set.Iic p) (schwarzChristoffelBoundary a e z₀ '' Set.Ici q) ↔ (∑ i : ι, e i * a i) ^ 2 ≠ ∑ i : ι, e i * a i ^ 2

The outer sides of an end of opening 2π. When the total exponent is one, the two outer images of the Schwarz--Christoffel boundary are disjoint exactly when the logarithmic coefficient C = ((∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2) / 2 is nonzero. Both are horizontal rays pointing to the right, at heights differing by π * C; when C = 0 they overlap. The finite prevertices need not be ordered or distinct.

theorem TauCeti.schwarzChristoffelBoundary_injective_of_edge_intersections_of_sum_eq_one {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (hfinite : ∀ (k : Fin (n + 2)), -1 < ∑ l : Fin (n + 2) with a l = a k, e l) (hsum : ∑ k : Fin (n + 2), e k = 1) (hC : (∑ k : Fin (n + 2), e k * a k) ^ 2 ≠ ∑ k : Fin (n + 2), e k * a k ^ 2) (hinter : ∀ (i j : Fin (n + 1)), i < j → ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc → ↑j = ↑i + 1 ∧ z = schwarzChristoffelVertex a e z₀ i.succ) (hleft : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ 0 + ↑t) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ 0) (hright : ∀ (i : Fin (n + 1)), ∀ z ∈ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc, z ∈ (fun (t : ℝ) => schwarzChristoffelVertex a e z₀ (Fin.last (n + 1)) + ↑t) '' Set.Ici 0 → z = schwarzChristoffelVertex a e z₀ (Fin.last (n + 1))) : Function.Injective (schwarzChristoffelBoundary a e z₀)

When the total exponent is one and the logarithmic coefficient ((∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2) / 2 is nonzero, a Schwarz--Christoffel boundary is simple if bounded sides meet only at consecutive vertices and each outer ray meets the bounded sides only at its finite endpoint. No additional intersection condition between the outer rays is needed.

theorem TauCeti.exists_forall_im_quadratic_log_notMem_Ioo {M C η : ℝ} (hC : C < 0) (hη : 0 < η) : ∃ (R : ℝ), ∀ (z : ℂ), 0 < z.im → R ≤ ‖z‖ → 1 / 2 < (z ^ 2 / 2 - ↑M * z + ↑C * Complex.log z).re → (z ^ 2 / 2 - ↑M * z + ↑C * Complex.log z).im ∉ Set.Ioo (Real.pi * C + η) (-η)

The band omitted by the quadratic comparison function. For real M and C < 0, far out in the upper half-plane, the comparison function z ^ 2 / 2 - M * z + C * log z takes no value with real part greater than 1 / 2 and height strictly between π * C + η and -η. Its imaginary part is (re z - M) * im z + C * arg z; inside the band im z is bounded, so Jordan's inequality puts arg z near 0 or π, which pushes the imaginary part out of the band.