Boundary values of the Schwarz--Christoffel map

The Schwarz--Christoffel primitive has two kinds of boundary point on the real axis. Away from the prevertices it continues holomorphically across a neighbourhood, while at a prevertex it still has a finite limit when the total exponent there is greater than -1. This file packages both cases in a single boundary map.

The canonical value schwarzChristoffelBoundary a e z₀ x is Mathlib's extendFrom extension of the primitive from the upper half-plane. That extension is a genuine limit of the primitive wherever such a limit exists, which is the case whenever the total exponent at x is greater than -1; this includes every point which is not a prevertex. On a prevertex whose total exponent is greater than -1 it agrees with schwarzChristoffelVertex, and on an interval free of nonzero prevertices it is continuous, injective, and has the explicit straight-edge increment formula from the boundary continuation. Thus the boundary map is the common object in which the vertices and the open edges of the eventual polygon meet.

Main definitions

• TauCeti.schwarzChristoffelBoundary -- the boundary value of the Schwarz--Christoffel primitive at a real point.

Main results

• TauCeti.tendsto_schwarzChristoffelPrimitive_boundary -- the primitive tends to the boundary value wherever the total exponent is greater than -1.
• TauCeti.schwarzChristoffelBoundary_apply_prevertex -- at a prevertex whose total exponent is greater than -1, the boundary value is the previously constructed Schwarz--Christoffel vertex.
• TauCeti.schwarzChristoffelBoundary_change_base -- changing the normalization point of the primitive subtracts a constant from the boundary map.
• TauCeti.schwarzChristoffelBoundary_sub_eq -- an increment of the boundary map along an open edge is a real integral times the fixed edge direction.
• TauCeti.schwarzChristoffelBoundary_injOn and TauCeti.collinear_schwarzChristoffelBoundary_image -- an open edge is embedded in a line.

References

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

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

The boundary value of the Schwarz--Christoffel map at a real point: the value at that point of Mathlib's extendFrom extension of the normalized primitive from the upper half-plane. The extension is total, so this is a limit of the primitive only where such a limit exists; that happens whenever the total exponent at the point is greater than -1, by tendsto_schwarzChristoffelPrimitive_boundary, and the value is unspecified elsewhere.

Equations

• TauCeti.schwarzChristoffelBoundary a e z₀ x = extendFrom UpperHalfPlane.upperHalfPlaneSet (TauCeti.schwarzChristoffelPrimitive a e z₀) ↑x

theorem TauCeti.schwarzChristoffelBoundary_eq_of_tendsto {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (x : ℝ) {v : ℂ} (h : Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds v)) : schwarzChristoffelBoundary a e z₀ x = v

A limit of the Schwarz--Christoffel primitive from the upper half-plane is its canonical boundary value.

@[simp]

theorem TauCeti.schwarzChristoffelBoundary_apply_prevertex {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j : ι) (he : -1 < ∑ i : ι with a i = a j, e i) : schwarzChristoffelBoundary a e z₀ (a j) = schwarzChristoffelVertex a e z₀ j

At a prevertex whose total exponent is greater than -1, the canonical Schwarz--Christoffel boundary value is the Schwarz--Christoffel vertex.

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

The Schwarz--Christoffel primitive tends to its canonical boundary value at every real point where the total exponent is greater than -1. At a prevertex this is the integrable-singularity estimate; away from all prevertices the integrand continues holomorphically across a real neighbourhood.

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

Changing the base point of the normalized primitive subtracts, from the canonical Schwarz--Christoffel boundary map, the value of the primitive at the old base point. This is the boundary counterpart of schwarzChristoffelPrimitive_change_base, and holds wherever the total exponent is greater than -1.

theorem TauCeti.continuousOn_schwarzChristoffelBoundary_of_exponent_sum_gt_neg_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {s : Set ℝ} (he : ∀ x ∈ s, -1 < ∑ i : ι with a i = x, e i) : ContinuousOn (schwarzChristoffelBoundary a e z₀) s

The canonical Schwarz--Christoffel boundary map is continuous on any set of real points at which the total exponent is greater than -1. This simultaneously gives continuity along open edges and attachment of those edges to every integrable prevertex.

theorem TauCeti.continuousOn_schwarzChristoffelBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : ContinuousOn (schwarzChristoffelBoundary a e z₀) (Set.Ioo p q)

On a real interval free of prevertices with nonzero exponent, the canonical boundary map is continuous.

theorem TauCeti.schwarzChristoffelBoundary_sub_eq {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) {x y : ℝ} (hx : x ∈ Set.Ioo p q) (hy : y ∈ Set.Ioo p q) : schwarzChristoffelBoundary a e z₀ x - schwarzChristoffelBoundary a e z₀ y = ↑(∫ (t : ℝ) in y..x, schwarzChristoffelDensity a e t) * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)

Along a real interval free of prevertices with nonzero exponent, the increment of the canonical Schwarz--Christoffel boundary map between two points is the real integral of ∏ i, |t - a i| ^ e i between them, times the fixed unimodular direction with argument schwarzChristoffelEdgeAngle a e p.

theorem TauCeti.hasDerivAt_schwarzChristoffelBoundary {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q x : ℝ} (ha : ∀ (k : ι), e k ≠ 0 → a k ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q) : HasDerivAt (schwarzChristoffelBoundary a e z₀) (↑(schwarzChristoffelDensity a e x) * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)) x

On an open boundary interval containing no nonzero prevertex, the derivative of the Schwarz--Christoffel boundary map is the positive density times the fixed edge direction.

theorem TauCeti.schwarzChristoffelBoundary_injOn {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : Set.InjOn (schwarzChristoffelBoundary a e z₀) (Set.Ioo p q)

The canonical Schwarz--Christoffel boundary map is injective on every real interval free of prevertices with nonzero exponent.

theorem TauCeti.collinear_schwarzChristoffelBoundary_image {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : Collinear ℝ (schwarzChristoffelBoundary a e z₀ '' Set.Ioo p q)

The image of a prevertex-free real interval under the canonical Schwarz--Christoffel boundary map is collinear.

theorem TauCeti.continuousOn_schwarzChristoffelBoundary_Icc {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) : ContinuousOn (schwarzChristoffelBoundary a e z₀) (Set.Icc p q)

Between two real endpoints whose total exponents are greater than -1, with no prevertex of nonzero exponent strictly between them, the canonical Schwarz--Christoffel boundary map is continuous on the closed interval. When the endpoints are prevertices, this says that the open straight edge supplied by schwarzChristoffelBoundary_sub_eq attaches continuously to its two vertices.