Short-turn separation of Schwarz--Christoffel sides

The bounded sides of a Schwarz--Christoffel polygon are positive multiples of unit vectors whose arguments are the Schwarz--Christoffel edge angles. If i + 1 < j and the edge angles from i through j are strictly increasing by less than π, then the intermediate chord from vertex i + 1 to vertex j lies strictly on one side of the supporting line of side i. Consequently the first and last sides cannot meet when at least one complete side lies between them.

This file records that geometric part of the global boundary-simplicity argument. It is stated in terms of strict monotonicity of the edge angles along the chain and a short-turn bound, so that the analytic angle calculation and the planar separation argument remain independent. The complementary case, where the direct boundary arc turns by at least π, can use the same idea on the other arc through the closing side.

Main results

• TauCeti.schwarzChristoffelVertex_succ_sub_eq_norm_mul identifies each bounded side vector.
• TauCeti.im_exp_neg_mul_schwarzChristoffelVertex_sub_pos_of_short_turn puts the intermediate chord from vertex i + 1 to vertex j strictly to the left of side i when i + 1 < j and the edge angles are strictly ordered with total turn less than π.
• TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_of_short_turn separates two nonadjacent bounded polygon sides whenever the intervening turn is less than π.

References

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

theorem TauCeti.schwarzChristoffelPolygon_bounded_edgeSet_inter_subset_vertex_of_adjacent {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : Monotone a) (i j : Fin n) (hadj : ↑i + 1 = ↑j) (hi : a i.castSucc < a i.succ) (hj : a j.castSucc < a j.succ) (hleft : -1 < ∑ l : Fin (n + 1) with a l = a i.castSucc, e l) (hcorner : ∑ l : Fin (n + 1) with a l = a i.succ, e l ∈ Set.Ioo (-1) 1) (hcorner0 : ∑ l : Fin (n + 1) with a l = a i.succ, e l ≠ 0) (hright : -1 < ∑ l : Fin (n + 1) with a l = a j.succ, e l) : Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc ∩ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc ⊆ {schwarzChristoffelVertex a e z₀ i.succ}

Adjacent bounded sides meet only at their common vertex when the prevertices are nondecreasing, both sides have distinct endpoints, the endpoint exponent sums exceed -1, and the corner exponent sum lies in (-1, 1) and is nonzero.

theorem TauCeti.schwarzChristoffelVertex_succ_sub_eq_norm_mul {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i : Fin n) (hfinite_left : -1 < ∑ k : Fin (n + 1) with a k = a i.castSucc, e k) (hfinite_right : -1 < ∑ k : Fin (n + 1) with a k = a i.succ, e k) : schwarzChristoffelVertex a e z₀ i.succ - schwarzChristoffelVertex a e z₀ i.castSucc = ↑‖schwarzChristoffelVertex a e z₀ i.succ - schwarzChristoffelVertex a e z₀ i.castSucc‖ * Complex.exp (↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I)

The vector of a bounded Schwarz--Christoffel side is its length times the unit vector whose argument is the edge angle at the side's left prevertex.

The prevertices are strictly ordered, and integrability is required only at the two endpoints of the side. These are exactly the hypotheses needed to apply the closed-edge direction formula to consecutive indexed prevertices.

theorem TauCeti.im_exp_neg_mul_schwarzChristoffelVertex_sub_pos_of_short_turn {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i j : Fin n) (hangle : StrictMonoOn (fun (k : Fin (n + 1)) => schwarzChristoffelEdgeAngle a e (a k)) (Set.Icc i.castSucc j.castSucc)) (hfinite : ∀ k ∈ Set.Icc i.succ j.castSucc, -1 < ∑ l : Fin (n + 1) with a l = a k, e l) (hij : ↑i + 1 < ↑j) (hshort : schwarzChristoffelEdgeAngle a e (a j.castSucc) < schwarzChristoffelEdgeAngle a e (a i.castSucc) + Real.pi) : 0 < (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (schwarzChristoffelVertex a e z₀ j.castSucc - schwarzChristoffelVertex a e z₀ i.succ)).im

A chord across a nonempty part of a short-turn Schwarz--Christoffel side chain lies strictly to the left of the first side.

Here i + 1 < j, so the chord from vertex i + 1 to vertex j contains at least one complete side. After rotating the direction of side i to the positive real axis, every side in that chord has positive imaginary part: strict angle monotonicity along the chain gives the lower bound and hshort keeps the final angle below the opposite direction.

theorem TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_of_short_turn {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i j : Fin n) (hangle : StrictMonoOn (fun (k : Fin (n + 1)) => schwarzChristoffelEdgeAngle a e (a k)) (Set.Icc i.castSucc j.castSucc)) (hfinite : ∀ k ∈ Set.Icc i.castSucc j.succ, -1 < ∑ l : Fin (n + 1) with a l = a k, e l) (hij : ↑i + 1 < ↑j) (hshort : schwarzChristoffelEdgeAngle a e (a j.castSucc) < schwarzChristoffelEdgeAngle a e (a i.castSucc) + Real.pi) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc)

Two nonadjacent bounded sides of a Schwarz--Christoffel polygon are disjoint when their edge angles are strictly ordered along the intervening chain and the directions from the first through the last side turn through less than π. The index condition excludes adjacent sides and the closing side.