Turning at Schwarz--Christoffel vertices

The direction of a Schwarz--Christoffel boundary edge is exp (schwarzChristoffelEdgeAngle a e p * I). When two consecutive edge intervals meet at a prevertex q, their angle difference is -π times the total exponent at q. Thus an exponent in (-1, 0) makes the boundary turn strictly through an angle less than π. More generally, any nonzero exponent in (-1, 1) gives a noncollinear corner, including an inward turn.

This file combines that angle calculation with the straight-edge description of SchwarzChristoffel.ClosedEdge. The main result says that the boundary values at three consecutive prevertices are affinely independent. In particular, the middle vertex is a genuine corner rather than a subdivision point of a straight side. This is the local nondegeneracy input for proving that a Schwarz--Christoffel boundary chain is a simple polygon.

Main results

• TauCeti.schwarzChristoffelEdgeAngle_mem_Ioo_of_adjacent -- the right-hand edge direction at a convex prevertex lies strictly between the left-hand direction and its half-turn.
• TauCeti.affineIndependent_schwarzChristoffelBoundary_of_adjacent -- three consecutive boundary values around a nonflat convex or reentrant prevertex are affinely independent.
• TauCeti.affineIndependent_schwarzChristoffelVertex_of_adjacent -- the corresponding indexed prevertex statement.
• TauCeti.affineIndependent_schwarzChristoffelVertex_of_consecutive_of_ne_zero -- the consecutive-index corner statement.
• TauCeti.schwarzChristoffelVertex_adjacent_segments_inter_eq -- adjacent sides meet only at their common vertex.
• TauCeti.affineIndependent_schwarzChristoffelBoundary_left_endpoint and TauCeti.affineIndependent_schwarzChristoffelBoundary_right_endpoint -- the first and last finite boundary vertices remain genuine corners where the boundary meets its closing sides.

References

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

theorem TauCeti.schwarzChristoffelEdgeAngle_mem_Ioo_of_adjacent {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q : ℝ} (hpq : p < q) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hq : ∑ i : ι with a i = q, e i ∈ Set.Ioo (-1) 0) : schwarzChristoffelEdgeAngle a e q ∈ Set.Ioo (schwarzChristoffelEdgeAngle a e p) (schwarzChristoffelEdgeAngle a e p + Real.pi)

At two adjacent prevertices, a middle exponent in (-1, 0) makes the boundary edge angle increase strictly by less than π from the left-hand edge to the right-hand edge.

The exponent is the sum over every index carried by the right endpoint, so the statement also covers coincident prevertices without selecting a distinguished representative.

theorem TauCeti.affineIndependent_schwarzChristoffelBoundary_of_adjacent {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q r : ℝ} (hpq : p < q) (hqr : q < r) (hpqFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hqrFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo q r) (hp : -1 < ∑ i : ι with a i = p, e i) (hq : -1 < ∑ i : ι with a i = q, e i) (hqSin : Real.sin (Real.pi * ∑ i : ι with a i = q, e i) ≠ 0) (hr : -1 < ∑ i : ι with a i = r, e i) : AffineIndependent ℝ ![schwarzChristoffelBoundary a e z₀ p, schwarzChristoffelBoundary a e z₀ q, schwarzChristoffelBoundary a e z₀ r]

Three consecutive Schwarz--Christoffel boundary values around a non-flat prevertex are affinely independent.

The hypotheses ask that the open intervals (p, q) and (q, r) contain no prevertex with nonzero exponent, that the endpoint exponent sums at p and r exceed -1, and that the middle exponent sum exceeds -1 with a nonzero sine of its π multiple. The three boundary values are therefore not collinear, so schwarzChristoffelBoundary a e z₀ q is a genuine corner of the boundary chain.

theorem TauCeti.affineIndependent_schwarzChristoffelVertex_of_adjacent {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (j k l : ι) (hjk : a j < a k) (hkl : a k < a l) (hjkFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo (a j) (a k)) (hklFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo (a k) (a l)) (hj : -1 < ∑ i : ι with a i = a j, e i) (hk : -1 < ∑ i : ι with a i = a k, e i) (hkSin : Real.sin (Real.pi * ∑ i : ι with a i = a k, e i) ≠ 0) (hl : -1 < ∑ i : ι with a i = a l, e i) : AffineIndependent ℝ ![schwarzChristoffelVertex a e z₀ j, schwarzChristoffelVertex a e z₀ k, schwarzChristoffelVertex a e z₀ l]

Three indexed Schwarz--Christoffel vertices at consecutive ordered prevertices are affinely independent when the total exponent at the middle prevertex exceeds -1 and its π multiple has nonzero sine.

theorem TauCeti.affineIndependent_schwarzChristoffelVertex_of_consecutive_of_ne_zero {m : ℕ} (a e : Fin m → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) {j k l : Fin m} (hjk : ↑j + 1 = ↑k) (hkl : ↑k + 1 = ↑l) (hj : -1 < e j) (hk : e k ∈ Set.Ioo (-1) 1) (hk0 : e k ≠ 0) (hl : -1 < e l) : AffineIndependent ℝ ![schwarzChristoffelVertex a e z₀ j, schwarzChristoffelVertex a e z₀ k, schwarzChristoffelVertex a e z₀ l]

Three vertices at consecutive strictly ordered prevertices form a noncollinear corner provided the middle turning exponent is nonzero and all three exponent singularities are integrable. Positive middle exponents, corresponding to reentrant corners, are allowed.

theorem TauCeti.schwarzChristoffelVertex_adjacent_segments_inter_eq {m : ℕ} (a e : Fin m → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) {j k l : Fin m} (hjk : ↑j + 1 = ↑k) (hkl : ↑k + 1 = ↑l) (hj : -1 < e j) (hk : e k ∈ Set.Ioo (-1) 1) (hk0 : e k ≠ 0) (hl : -1 < e l) : segment ℝ (schwarzChristoffelVertex a e z₀ j) (schwarzChristoffelVertex a e z₀ k) ∩ segment ℝ (schwarzChristoffelVertex a e z₀ k) (schwarzChristoffelVertex a e z₀ l) = {schwarzChristoffelVertex a e z₀ k}

The two sides at a nonflat finite corner of a Schwarz--Christoffel polygon intersect only at their common vertex, even when the corner is reentrant.

Corners beside the vertex at infinity

theorem TauCeti.affineIndependent_schwarzChristoffelBoundary_left_endpoint {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (hpq : p < q) (ha : ∀ (i : ι), e i ≠ 0 → p ≤ a i) (hpqFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hp : ∑ i : ι with a i = p, e i ∈ Set.Ioo (-1) 0) (hq : -1 < ∑ i : ι with a i = q, e i) (hS : ∑ i : ι, e i < -1) : AffineIndependent ℝ ![schwarzChristoffelVertexAtInfinity a e z₀, schwarzChristoffelBoundary a e z₀ p, schwarzChristoffelBoundary a e z₀ q]

The first finite Schwarz--Christoffel boundary vertex is a genuine corner. The left-hand unbounded edge joins the vertex at infinity to B p, while the next finite edge joins B p to B q; if the total exponent at p lies in (-1, 0), these three points are affinely independent.

The hypothesis ha says that p is the leftmost prevertex with nonzero exponent.

theorem TauCeti.affineIndependent_schwarzChristoffelBoundary_right_endpoint {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {q p : ℝ} (hqp : q < p) (ha : ∀ (i : ι), e i ≠ 0 → a i ≤ p) (hqpFree : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo q p) (hq : -1 < ∑ i : ι with a i = q, e i) (hp : ∑ i : ι with a i = p, e i ∈ Set.Ioo (-1) 0) (hS : ∑ i : ι, e i < -1) : AffineIndependent ℝ ![schwarzChristoffelBoundary a e z₀ q, schwarzChristoffelBoundary a e z₀ p, schwarzChristoffelVertexAtInfinity a e z₀]

The last finite Schwarz--Christoffel boundary vertex is a genuine corner. The preceding finite edge joins B q to B p, while the right-hand unbounded edge joins B p to the vertex at infinity; if the total exponent at p lies in (-1, 0), these three points are affinely independent.

The hypothesis ha says that p is the rightmost prevertex with nonzero exponent.