Separation of bounded Schwarz--Christoffel sides

Two nonadjacent bounded sides of a Schwarz--Christoffel polygon can be separated by following either of the two boundary arcs between them. Polygon.ShortTurn treats the direct arc when its directions turn through less than π. This file treats the complementary arc through the vertex at infinity when the direct turn is at least π. The closing condition makes its two unbounded pieces point in the same direction, and the complementary turn is at most π.

Combining the two cases shows that every pair of nonadjacent bounded sides is disjoint under the classical convex-polygon hypotheses: strictly ordered prevertices, exponents in (-1, 0), and total exponent -2. These lemmas supply the bounded-side part of the global boundary-simplicity argument.

Main results

• TauCeti.im_exp_neg_mul_schwarzChristoffelVertex_sub_pos_of_long_turn puts the chord along the complementary boundary arc strictly to one side of the later bounded edge.
• TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_of_long_turn separates nonadjacent bounded sides when their direct turn is at least π.
• TauCeti.disjoint_schwarzChristoffelPolygon_bounded_edgeSet separates every pair of nonadjacent bounded sides.

References

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

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

After rotating by -θ, the height of a bounded Schwarz--Christoffel side vector is its length times the sine of its edge angle measured from θ.

theorem TauCeti.im_exp_neg_mul_schwarzChristoffelVertex_sub_pos_of_long_turn {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) (i j : Fin n) (hij : ↑i + 1 < ↑j) (hlong : schwarzChristoffelEdgeAngle a e (a i.castSucc) + Real.pi ≤ schwarzChristoffelEdgeAngle a e (a j.castSucc)) : 0 < (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a j.castSucc)) * Complex.I) * (schwarzChristoffelVertex a e z₀ i.castSucc - schwarzChristoffelVertex a e z₀ j.succ)).im

If the direct turn from bounded side i to bounded side j is at least π, the chord from the end of side j to the start of side i, following the complementary boundary arc through infinity, lies strictly to the left of side j.

The index condition leaves at least one complete bounded side on the direct arc. The exponent conditions make all edge directions strictly ordered through one full turn, while the total exponent -2 identifies the two unbounded pieces as a single positive-direction closing side.

theorem TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_of_long_turn {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) (i j : Fin n) (hij : ↑i + 1 < ↑j) (hlong : schwarzChristoffelEdgeAngle a e (a i.castSucc) + Real.pi ≤ schwarzChristoffelEdgeAngle a e (a j.castSucc)) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc)

Two nonadjacent bounded Schwarz--Christoffel sides are disjoint when their direct edge-angle turn is at least π. The separating chord follows the complementary boundary arc through the vertex at infinity, whose turn is at most π.

theorem TauCeti.disjoint_schwarzChristoffelPolygon_bounded_edgeSet {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), e k ∈ Set.Ioo (-1) 0) (hsum : ∑ k : Fin (n + 1), e k = -2) (i j : Fin n) (hij : ↑i + 1 < ↑j) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) j.castSucc.castSucc)

Under the classical convex Schwarz--Christoffel hypotheses, every two nonadjacent bounded sides are disjoint. The proof uses the direct boundary arc when its turn is less than π and the complementary arc through infinity otherwise.