The combinatorial polygon of Schwarz--Christoffel boundary values

A finite indexed family of Schwarz--Christoffel prevertices supplies a list of complex boundary values. This file appends the common boundary value at infinity and packages the resulting cyclic list as Mathlib's Polygon. The indexing here is purely combinatorial: no ordering or distinctness assumption is imposed on the prevertices.

When the indices list distinct prevertices in increasing order and the relevant integrability and decay hypotheses hold, the extra vertex at infinity records the subdivision of the closing boundary side into the two unbounded real intervals. For the classical exponent sum -2 it need not be a geometric corner: the two adjacent polygon edges may be collinear.

The edge formulas below separate the three positions in the index list. There is one edge between each pair of index-successive finite vertices, one edge from the last-indexed finite vertex to infinity, and one from infinity to the first-indexed finite vertex. Their union is the polygon boundary. Under the ordering and analytic hypotheses above, these are the three kinds of boundary interval. The formulas are the finite combinatorial interface used to identify the range of the compactified Schwarz--Christoffel boundary with a polygonal boundary.

Main definitions

• TauCeti.schwarzChristoffelPolygon -- the polygon whose vertices are the finite Schwarz--Christoffel vertices followed by the vertex at infinity.

Main results

• TauCeti.schwarzChristoffelPolygon_edgeSet_castSucc_castSucc -- the bounded edges join consecutive finite vertices.
• TauCeti.schwarzChristoffelPolygon_edgeSet_last_prevertex -- the penultimate edge joins the last finite vertex to the vertex at infinity.
• TauCeti.schwarzChristoffelPolygon_edgeSet_last -- the final edge joins the vertex at infinity back to the first finite vertex.
• TauCeti.schwarzChristoffelPolygon_boundary -- the polygon boundary is the union of those three kinds of edge.

References

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

noncomputable def TauCeti.schwarzChristoffelPolygon {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) : Polygon ℂ (n + 2)

The polygon formed by the Schwarz--Christoffel boundary values at a nonempty, finitely indexed family of prevertices, with the common boundary value at infinity appended as the final vertex.

The prevertices are indexed by Fin (n + 1), so there is always a first and a last finite vertex. The resulting polygon has n + 2 vertices. As with the underlying total definitions, its finite vertices and its vertex at infinity represent actual limits under the corresponding integrability and decay hypotheses.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.schwarzChristoffelPolygon_apply_castSucc {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (i : Fin (n + 1)) : (schwarzChristoffelPolygon a e z₀).vertices i.castSucc = schwarzChristoffelVertex a e z₀ i

A finite vertex of the Schwarz--Christoffel polygon is the boundary value at the corresponding prevertex.

@[simp]

theorem TauCeti.schwarzChristoffelPolygon_apply_last {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) : (schwarzChristoffelPolygon a e z₀).vertices (Fin.last (n + 1)) = schwarzChristoffelVertexAtInfinity a e z₀

The final vertex of the Schwarz--Christoffel polygon is its common boundary value at infinity.

theorem TauCeti.schwarzChristoffelPolygon_apply_castSucc_eq_boundary {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (i : Fin (n + 1)) (hi : -1 < ∑ j : Fin (n + 1) with a j = a i, e j) : (schwarzChristoffelPolygon a e z₀).vertices i.castSucc = schwarzChristoffelBoundary a e z₀ (a i)

When a finite prevertex has integrable total exponent, the corresponding polygon vertex is the canonical boundary value of the Schwarz--Christoffel map there.

The three kinds of edge

@[simp]

theorem TauCeti.schwarzChristoffelPolygon_edgeSet_castSucc_castSucc {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (i : Fin n) : Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc = segment ℝ (schwarzChristoffelVertex a e z₀ i.castSucc) (schwarzChristoffelVertex a e z₀ i.succ)

A bounded edge of the Schwarz--Christoffel polygon joins the vertices at two consecutive indices.

@[simp]

theorem TauCeti.schwarzChristoffelPolygon_edgeSet_last_prevertex {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) : Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last n).castSucc = segment ℝ (schwarzChristoffelVertex a e z₀ (Fin.last n)) (schwarzChristoffelVertexAtInfinity a e z₀)

The edge after the last finite prevertex joins its boundary value to the common value at infinity.

@[simp]

theorem TauCeti.schwarzChristoffelPolygon_edgeSet_last {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) : Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)) = segment ℝ (schwarzChristoffelVertexAtInfinity a e z₀) (schwarzChristoffelVertex a e z₀ 0)

The final edge of the Schwarz--Christoffel polygon joins the common value at infinity back to the first finite boundary value.

The complete polygon boundary

theorem TauCeti.schwarzChristoffelPolygon_boundary {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) : Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀) = (⋃ (i : Fin n), segment ℝ (schwarzChristoffelVertex a e z₀ i.castSucc) (schwarzChristoffelVertex a e z₀ i.succ)) ∪ segment ℝ (schwarzChristoffelVertex a e z₀ (Fin.last n)) (schwarzChristoffelVertexAtInfinity a e z₀) ∪ segment ℝ (schwarzChristoffelVertexAtInfinity a e z₀) (schwarzChristoffelVertex a e z₀ 0)

The boundary of the Schwarz--Christoffel polygon is the union of the bounded edges between successive finite vertices and the two edges incident to the vertex at infinity.