Nondegeneracy of the Schwarz--Christoffel polygon

Strictly ordered prevertices with integrable exponents produce distinct consecutive Schwarz--Christoffel vertices. The two closing sides are nondegenerate as well: their common endpoint at infinity differs from the first and last finite vertices. Consequently every edge of the packaged Schwarz--Christoffel polygon is nondegenerate.

When there are at least two finite prevertices, the turning-exponent condition (-1, 0) also makes the first and last finite vertices genuine corners. These are the endpoint counterparts of the interior-corner theorem in SchwarzChristoffel.Turning. The appended vertex at infinity is not claimed to be a corner: under the classical exponent sum, it can merely subdivide one straight closing side.

Together, these results supply the local nondegeneracy needed before separating nonadjacent sides in the global simplicity argument.

Main results

• TauCeti.affineIndependent_schwarzChristoffelPolygon_first and TauCeti.affineIndependent_schwarzChristoffelPolygon_last -- the two finite endpoint vertices are genuine corners.
• TauCeti.schwarzChristoffelPolygon_hasNondegenerateEdges -- every side of the packaged polygon has distinct endpoints.

References

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

theorem TauCeti.affineIndependent_schwarzChristoffelPolygon_first {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (hfirst : ∑ i : Fin (n + 2) with a i = a 0, e i ∈ Set.Ioo (-1) 0) (hnext : -1 < ∑ i : Fin (n + 2) with a i = a 1, e i) (hS : ∑ i : Fin (n + 2), e i < -1) : AffineIndependent ℝ ![(schwarzChristoffelPolygon a e z₀).vertices (Fin.last (n + 2)), (schwarzChristoffelPolygon a e z₀).vertices (Fin.castSucc 0), (schwarzChristoffelPolygon a e z₀).vertices (Fin.castSucc 1)]

The first finite vertex of a Schwarz--Christoffel polygon is a genuine corner: it is affinely independent from the vertex at infinity and the next finite vertex.

The family has n + 2 finite prevertices so that a next vertex always exists.

theorem TauCeti.affineIndependent_schwarzChristoffelPolygon_last {n : ℕ} (a e : Fin (n + 2) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (hpreceding : -1 < ∑ i : Fin (n + 2) with a i = a (Fin.last n).castSucc, e i) (hlast : ∑ i : Fin (n + 2) with a i = a (Fin.last (n + 1)), e i ∈ Set.Ioo (-1) 0) (hS : ∑ i : Fin (n + 2), e i < -1) : AffineIndependent ℝ ![(schwarzChristoffelPolygon a e z₀).vertices (Fin.last n).castSucc.castSucc, (schwarzChristoffelPolygon a e z₀).vertices (Fin.last (n + 1)).castSucc, (schwarzChristoffelPolygon a e z₀).vertices (Fin.last (n + 2))]

The last finite vertex of a Schwarz--Christoffel polygon is a genuine corner: it is affinely independent from the preceding finite vertex and the vertex at infinity.

The family has n + 2 finite prevertices so that a preceding vertex always exists.

theorem TauCeti.schwarzChristoffelPolygon_hasNondegenerateEdges {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (hfinite : ∀ (j : Fin (n + 1)), -1 < ∑ i : Fin (n + 1) with a i = a j, e i) (hS : ∑ i : Fin (n + 1), e i < -1) : (schwarzChristoffelPolygon a e z₀).HasNondegenerateEdges

Every edge of the Schwarz--Christoffel polygon has distinct endpoints when the finite prevertices are strictly ordered, all their total exponents are integrable, and the primitive decays sufficiently to have a finite vertex at infinity.