Bounded Schwarz--Christoffel sides are supporting lines

Under the classical convex-polygon hypotheses (strictly ordered prevertices, exponents in (-1, 0) and total exponent -2), the line through each bounded side of the Schwarz--Christoffel polygon supports the whole polygon: after rotating the side's direction to the positive real axis, every point of the polygon boundary lies on or above the rotated line through the side.

The argument follows the boundary once around, starting at the side. Measured from the side's direction, the directions of the successive sides and of the closing side increase through less than one full turn. Hence the rotated height first increases and then decreases along the boundary, and since it returns to zero it is nonnegative throughout.

Combined with the fact that the image of the upper half-plane under the Schwarz--Christoffel primitive is open and lies in the filled hull of the polygon boundary, this puts the image in the open half-plane on the interior side of each bounded side. In particular the image misses every bounded side.

Main results

• TauCeti.im_exp_neg_mul_sub_schwarzChristoffelVertex_nonneg_of_mem_boundary -- the polygon boundary lies on the interior side of the line through a bounded side.
• TauCeti.im_exp_neg_mul_sub_schwarzChristoffelVertex_pos_of_mem_interior_closedConvexHull -- the polygon interior lies strictly on the interior side of the line through a bounded side.
• TauCeti.im_exp_neg_mul_schwarzChristoffelPrimitive_sub_pos -- every value of the primitive lies strictly on the interior side of that line.
• TauCeti.disjoint_image_schwarzChristoffelPrimitive_edgeSet_castSucc_castSucc -- the image of the upper half-plane misses every bounded side.

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_sub_schwarzChristoffelVertex_nonneg_of_mem_boundary {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) {z : ℂ} (hz : z ∈ Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)) : 0 ≤ (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (z - schwarzChristoffelVertex a e z₀ i.castSucc)).im

The Schwarz--Christoffel polygon lies on the interior side of each bounded side. Under the classical convex-polygon hypotheses, rotate the direction of the bounded side from vertex i to vertex i + 1 to the positive real axis. Then every point of the polygon boundary lies on or above the rotated line through that side.

theorem TauCeti.im_exp_neg_mul_sub_schwarzChristoffelVertex_pos_of_mem_interior_closedConvexHull {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) {z : ℂ} (hz : z ∈ interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)))) : 0 < (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (z - schwarzChristoffelVertex a e z₀ i.castSucc)).im

The convex Schwarz--Christoffel polygon interior lies strictly on the interior side of each bounded side. Rotate the bounded side from vertex i to vertex i + 1 to the positive real axis. Every point in the interior of the closed convex hull of the polygon boundary then has strictly positive imaginary part relative to the rotated supporting line.

theorem TauCeti.im_exp_neg_mul_schwarzChristoffelPrimitive_sub_pos {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) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : 0 < (Complex.exp (-↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I) * (schwarzChristoffelPrimitive a e z₀ z - schwarzChristoffelVertex a e z₀ i.castSucc)).im

The Schwarz--Christoffel image lies strictly on the interior side of each bounded side. Under the classical convex-polygon hypotheses, rotate the direction of the bounded side from vertex i to vertex i + 1 to the positive real axis. Then every value of the primitive on the upper half-plane lies strictly above the rotated line through that side.

theorem TauCeti.disjoint_interior_closedConvexHull_schwarzChristoffelPolygon_edgeSet_castSucc_castSucc {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) : Disjoint (interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)))) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc)

The convex Schwarz--Christoffel polygon interior misses each bounded side. Here the polygon interior is represented by the interior of the closed convex hull of its boundary.

theorem TauCeti.disjoint_image_schwarzChristoffelPrimitive_edgeSet_castSucc_castSucc {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) : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) i.castSucc.castSucc)

The Schwarz--Christoffel image misses every bounded side. Under the classical convex-polygon hypotheses, the image of the upper half-plane under the primitive is disjoint from the bounded side from vertex i to vertex i + 1.