Documentation

TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Vertex

The vertices of the Schwarz--Christoffel map #

The Schwarz--Christoffel primitive is holomorphic on the open upper half-plane, and the polygon it is meant to parametrize would be read off from its boundary values at the real prevertices. This file shows that those boundary values exist as limits; identifying the image of the map as a polygon, and these limits as its corners, is left to later work.

Write p = a j for a prevertex and t for the total turning exponent carried by it, that is the sum of the e i over all i with a i = p. Near p the integrand has norm ∏ i, dist z (a i) ^ e i, which is dist z p ^ t times a factor that stays bounded, so it is dominated by C * dist z p ^ t. When -1 < t this dominating function is integrable along any segment ending at p, uniformly enough that the primitive satisfies the Cauchy criterion at p; completeness of ℂ then produces the limit. For pairwise distinct prevertices t is a single exponent e j, and the classical choice e i = α i / π - 1 coming from an interior angle α i ∈ (0, 2 π) satisfies -1 < t automatically; when several prevertices coincide their exponents add up, and -1 < t is then a genuine hypothesis on the sum.

The quantitative heart is the segment estimate Complex.integral_dist_rpow_segment_le: integrating dist ⬝ p ^ u along a segment of length L gives at most 2 / (u + 1) * L ^ (u + 1) for -1 < u ≤ 0. Fed into the segment displacement bound TauCeti.norm_schwarzChristoffelPrimitive_sub_le_integral it turns into a Hölder bound ‖F z - F w‖ ≤ C * (2 / (u + 1)) * ‖z - w‖ ^ (u + 1) for z, w in a small half-disc, which is what forces the Cauchy criterion.

Main definitions #

Main results #

References #

The local bound at a prevertex #

source
theorem TauCeti.exists_norm_schwarzChristoffelIntegrand_le {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (p : ℝ) :
∃ C > 0, ∀ᶠ (z : ℂ) in nhdsWithin ↑p {↑p}ᶜ, ‖schwarzChristoffelIntegrand a e z‖ ≤ C * dist z ↑p ^ ∑ i : ι with a i = p, e i

Near a real prevertex p, the Schwarz--Christoffel integrand is dominated by a constant multiple of dist z p ^ t, where t = ∑ i with a i = p, e i is the total turning exponent carried by the indices sitting at p. The prevertex itself is excluded because both sides are totalized there and carry no analytic information.

A Hölder estimate near a prevertex #

Existence of the vertex #

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

The Schwarz--Christoffel vertex attached to the prevertex a j: the boundary value at a j of the primitive normalized at z₀. It is a genuine limit when the total turning exponent at a j exceeds -1.

Equations
Instances For
    source
    theorem TauCeti.schwarzChristoffelVertex_congr {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {j k : ι} (h : a j = a k) :
    schwarzChristoffelVertex a e z₀ j = schwarzChristoffelVertex a e z₀ k

    Coincident prevertices carry the same vertex: schwarzChristoffelVertex depends on the index j only through the prevertex a j.

    source
    theorem TauCeti.tendsto_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j : ι) (he : -1 < ∑ i : ι with a i = a j, e i) :
    Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑(a j)) UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelVertex a e z₀ j))

    The Schwarz--Christoffel primitive converges to schwarzChristoffelVertex at the prevertex.

    source
    theorem TauCeti.schwarzChristoffelVertex_change_base {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (b c : UpperHalfPlane) (j : ι) (he : -1 < ∑ i : ι with a i = a j, e i) :
    schwarzChristoffelVertex a e b j = schwarzChristoffelVertex a e c j - schwarzChristoffelPrimitive a e c ↑b

    Changing the base point translates every Schwarz--Christoffel boundary value by one and the same constant.