Separation of Schwarz--Christoffel sides from the closing side

With the total exponent -2, the two unbounded pieces of the Schwarz--Christoffel boundary both run in the positive real direction (schwarzChristoffelBoundary_lt_vertexAtInfinity and schwarzChristoffelVertexAtInfinity_lt_boundary): the last finite vertex, the vertex at infinity and the first finite vertex lie on one horizontal line in this order.

Under the classical convex-polygon hypotheses (strictly ordered prevertices and exponents in (-1, 0)), every other finite vertex lies strictly above that line. The bounded side vectors have arguments strictly increasing in (-2π, 0), so the heights of the vertices first increase and then decrease; since the first and last vertices have equal heights, all intermediate heights are larger.

Consequently a bounded side meets the closing line at most in an endpoint shared with the closing side, and nonadjacent bounded and closing polygon sides are disjoint. Together with the separation of nonadjacent bounded sides, this is the input for global simplicity of the Schwarz--Christoffel polygon.

Main results

• TauCeti.im_schwarzChristoffelVertex_zero_lt -- every finite vertex other than the first and the last lies strictly above the closing line.
• TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_last_prevertex and TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_last -- bounded sides are disjoint from the nonadjacent closing sides.

References

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

theorem TauCeti.schwarzChristoffelVertex_last_lt_vertexAtInfinity_lt_vertex_zero {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (he : ∀ (k : Fin (n + 1)), -1 < e k) (hsum : ∑ k : Fin (n + 1), e k = -2) : schwarzChristoffelVertex a e z₀ (Fin.last n) < schwarzChristoffelVertexAtInfinity a e z₀ ∧ schwarzChristoffelVertexAtInfinity a e z₀ < schwarzChristoffelVertex a e z₀ 0

The closing side runs from the last finite vertex through the vertex at infinity to the first finite vertex, horizontally and in the positive real direction.

@[simp]

theorem TauCeti.im_schwarzChristoffelVertexAtInfinity_eq_im_zero {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) : (schwarzChristoffelVertexAtInfinity a e z₀).im = (schwarzChristoffelVertex a e z₀ 0).im

The vertex at infinity lies on the closing line. Its imaginary part equals that of the first finite vertex.

@[simp]

theorem TauCeti.im_schwarzChristoffelVertex_last_eq_im_zero {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) : (schwarzChristoffelVertex a e z₀ (Fin.last n)).im = (schwarzChristoffelVertex a e z₀ 0).im

The first and last finite vertices lie on the same closing line. Their imaginary parts agree.

theorem TauCeti.im_schwarzChristoffelVertex_zero_lt {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) {k : Fin (n + 1)} (hk₀ : k ≠ 0) (hkn : k ≠ Fin.last n) : (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelVertex a e z₀ k).im

The finite vertices lie above the closing line. For strictly ordered prevertices with exponents in (-1, 0) summing to -2, every finite Schwarz--Christoffel vertex other than the first and the last lies strictly above the horizontal line through the first vertex, which also contains the last vertex and the vertex at infinity.

theorem TauCeti.im_schwarzChristoffelVertex_zero_le {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) (k : Fin (n + 1)) : (schwarzChristoffelVertex a e z₀ 0).im ≤ (schwarzChristoffelVertex a e z₀ k).im

Every finite Schwarz--Christoffel vertex lies on or above the closing line. The line is identified by the imaginary part of the first finite vertex.

theorem TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_last_prevertex {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 : Fin n) (hi : ↑i + 1 < n) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last n).castSucc)

A bounded side misses the nonadjacent right-hand closing side. Under the classical convex-polygon hypotheses, the bounded side from vertex i to vertex i + 1, where i + 1 is not the last finite vertex, is disjoint from the polygon side joining the last finite vertex to the vertex at infinity.

theorem TauCeti.disjoint_schwarzChristoffelPolygon_edgeSet_last {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 : Fin n) (hi : 0 < ↑i) : Disjoint (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)))

A bounded side misses the nonadjacent left-hand closing side. Under the classical convex-polygon hypotheses, the bounded side from vertex i to vertex i + 1, where i is not the first finite vertex, is disjoint from the polygon side joining the vertex at infinity to the first finite vertex.

theorem TauCeti.im_schwarzChristoffelBoundary_first_lt {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) {x : ℝ} (hx : x ∈ Set.Ioo (a 0) (a (Fin.last n))) : (schwarzChristoffelBoundary a e z₀ (a 0)).im < (schwarzChristoffelBoundary a e z₀ x).im

The bounded Schwarz--Christoffel boundary arc lies strictly above the closing line, except at its first and last prevertices.