The Schwarz--Christoffel image and the closing side

For strictly ordered prevertices with exponents in (-1, 0) summing to -2, the Schwarz--Christoffel polygon lies in the closed half-plane above its horizontal closing side. The filled-hull bound for the primitive therefore puts its entire upper-half-plane image in the same closed half-plane. Since that image is open, it actually lies in the corresponding open half-plane and misses both pieces of the closing side.

This is one part of identifying the image with the polygon interior. Bounded-side avoidance is proved using supporting lines, and the resulting global image and injectivity statements are assembled in TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Polygon.Mapping.

Main results

• TauCeti.schwarzChristoffelPolygon_boundary_subset_halfSpace -- the polygon boundary lies on or above its closing line.
• TauCeti.im_schwarzChristoffelVertex_zero_lt_of_mem_interior_closedConvexHull_boundary -- the polygon interior lies strictly above its closing line.
• TauCeti.im_schwarzChristoffelVertex_zero_lt_primitive -- every value of the primitive in the upper half-plane lies strictly above the closing line.
• TauCeti.disjoint_image_schwarzChristoffelPrimitive_closingSides -- the image misses both pieces of the closing side.

References

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

theorem TauCeti.schwarzChristoffelPolygon_boundary_subset_halfSpace {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) : Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀) ⊆ {z : ℂ | (schwarzChristoffelVertex a e z₀ 0).im ≤ z.im}

The Schwarz--Christoffel polygon boundary lies on or above its closing line. The two closing edges lie on the line, while the finite vertices and hence every bounded edge lie in its upper closed half-plane.

theorem TauCeti.im_schwarzChristoffelVertex_zero_lt_of_mem_interior_closedConvexHull_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) {z : ℂ} (hz : z ∈ interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)))) : (schwarzChristoffelVertex a e z₀ 0).im < z.im

The convex Schwarz--Christoffel polygon interior lies strictly above its closing line. Here the polygon interior is represented by the interior of the closed convex hull of its boundary.

theorem TauCeti.disjoint_interior_closedConvexHull_schwarzChristoffelPolygon_closingSides {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) : Disjoint (interior ((closedConvexHull ℝ) (Polygon.boundary ℝ (schwarzChristoffelPolygon a e z₀)))) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last n).castSucc ∪ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)))

The convex Schwarz--Christoffel polygon interior misses its closing sides. Here the polygon interior is represented by the interior of the closed convex hull of its boundary.

theorem TauCeti.im_schwarzChristoffelVertex_zero_lt_primitive {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) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : (schwarzChristoffelVertex a e z₀ 0).im < (schwarzChristoffelPrimitive a e z₀ z).im

Every value of the Schwarz--Christoffel primitive lies strictly above the closing line. The image lies in the filled hull of the polygon boundary, hence in its closed convex hull and in the closed half-plane above the closing side. Openness of the image upgrades the weak inequality to a strict one.

theorem TauCeti.disjoint_image_schwarzChristoffelPrimitive_closingSides {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) : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last n).castSucc ∪ Polygon.edgeSet ℝ (schwarzChristoffelPolygon a e z₀) (Fin.last (n + 1)))

The upper-half-plane image misses the closing sides of the Schwarz--Christoffel polygon. Both closing segments lie on the horizontal line through the first finite vertex, while every interior value lies strictly above that line.