The image bounded by a simple unbounded Schwarz--Christoffel chain

For integrable finite prevertices and total exponent in [-1, 1), an injective real boundary parametrization forces the primitive's interior image to avoid the boundary. Consequently the primitive maps the upper half-plane bijectively onto the complementary component containing the base-point image, and its frontier is the whole boundary chain. This gives the direct mapping theorem for simple unbounded polygons, including parallel-ended polygons.

The same holds at total exponent 1, an end of opening 2π, when the logarithmic coefficient ((∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2) / 2 is negative. Some sign condition is needed there: with exponents -1 / 2 at -1 and 3 / 2 at 1 the boundary is a simple chain of two parallel rays joined by a segment, but the corner of opening 5π / 2 makes the image overlap its boundary.

Inversion about an exterior point reduces separation to the planar Jordan curve theorem: the inverted image is bounded, its frontier lies on the inverted boundary together with 0, and an open subset of the filled hull of a Jordan curve cannot meet that curve.

References

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

theorem TauCeti.disjoint_image_schwarzChristoffelPrimitive_range_of_neg_one_le_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hlow : -1 ≤ ∑ i : ι, e i) (hhigh : ∑ i : ι, e i < 1 ∨ ∑ i : ι, e i = 1 ∧ (∑ i : ι, e i * a i) ^ 2 < ∑ i : ι, e i * a i ^ 2) (hinj : Function.Injective (schwarzChristoffelBoundary a e z₀)) : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (Set.range (schwarzChristoffelBoundary a e z₀))

A simple proper Schwarz--Christoffel boundary is disjoint from the image of the open upper half-plane, if the end at infinity has opening less than 2π, or opening 2π with negative logarithmic coefficient. The total exponents -1 and 1 include parallel outer sides.

theorem TauCeti.image_schwarzChristoffelPrimitive_eq_connectedComponentIn_of_neg_one_le_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hlow : -1 ≤ ∑ i : ι, e i) (hhigh : ∑ i : ι, e i < 1 ∨ ∑ i : ι, e i = 1 ∧ (∑ i : ι, e i * a i) ^ 2 < ∑ i : ι, e i * a i ^ 2) (hinj : Function.Injective (schwarzChristoffelBoundary a e z₀)) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet = connectedComponentIn (Set.range (schwarzChristoffelBoundary a e z₀))ᶜ (schwarzChristoffelPrimitive a e z₀ ↑z₀)

The image of a primitive with a simple proper boundary is the complementary component containing its base-point image, for total exponent in [-1, 1), or total exponent 1 with negative logarithmic coefficient.

@[simp]

theorem TauCeti.frontier_image_schwarzChristoffelPrimitive_eq_range_of_neg_one_le_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hlow : -1 ≤ ∑ i : ι, e i) (hhigh : ∑ i : ι, e i < 1 ∨ ∑ i : ι, e i = 1 ∧ (∑ i : ι, e i * a i) ^ 2 < ∑ i : ι, e i * a i ^ 2) (hinj : Function.Injective (schwarzChristoffelBoundary a e z₀)) : frontier (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) = Set.range (schwarzChristoffelBoundary a e z₀)

The frontier of the primitive image is the entire simple proper boundary chain.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_of_simple_boundary_of_neg_one_le_sum {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hlow : -1 ≤ ∑ i : ι, e i) (hhigh : ∑ i : ι, e i < 1 ∨ ∑ i : ι, e i = 1 ∧ (∑ i : ι, e i * a i) ^ 2 < ∑ i : ι, e i * a i ^ 2) (hinj : Function.Injective (schwarzChristoffelBoundary a e z₀)) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet (connectedComponentIn (Set.range (schwarzChristoffelBoundary a e z₀))ᶜ (schwarzChristoffelPrimitive a e z₀ ↑z₀))

A Schwarz--Christoffel primitive with a simple proper boundary and total exponent in [-1, 1), or total exponent 1 with negative logarithmic coefficient ((∑ i, e i * a i) ^ 2 - ∑ i, e i * a i ^ 2) / 2, maps the upper half-plane bijectively onto the complementary region containing its base-point image. This allows reentrant finite corners, parallel outer sides, and ends of opening 2π.