The image of the Schwarz--Christoffel primitive and its boundary

Let F = schwarzChristoffelPrimitive a e z₀ and let P be the range of the compactified boundary map schwarzChristoffelCompactifiedBoundary a e z₀, the closed boundary path through all the finite vertices and the vertex at infinity. For a monotone family of prevertices, range_schwarzChristoffelCompactifiedBoundary identifies P with the boundary of schwarzChristoffelPolygon.

This file locates the image F '' upperHalfPlaneSet relative to P, assuming only that every finite prevertex is integrable and that the total exponent is less than -1. These results do not assume simplicity of P or injectivity of F. The image is open because F has a nonvanishing derivative. It is bounded, and its closure is exactly the image together with P: every point of P is a boundary limit of F. Every limit of F from the upper half-plane is either an interior value, a finite boundary value or the vertex at infinity. Hence the frontier of the image is P minus the image.

Two consequences describe the image by the components of the complement of P. The image lies in filledHull P: it misses the unbounded complementary component. And a complementary component that meets the image is contained in it. Away from P, the image is therefore a union of bounded complementary components of P; identifying it with the inside of the polygon further requires knowing those components and showing that the image does not meet P. In the same direction, a preconnected set avoiding P and containing the image is equal to the image.

The primitive is also proper over the complement of P: the points of the upper half-plane that it sends into a closed set avoiding P form a compact set. Near the real axis and near infinity the primitive is close to its boundary values, which all lie on P.

The continuous extension to the closed upper half-plane and convergence to the vertex at infinity are also available separately. They control preimages near a specified boundary value.

Main results

• TauCeti.isOpen_image_schwarzChristoffelPrimitive -- the primitive maps open subsets of the upper half-plane to open sets.
• TauCeti.isBounded_image_schwarzChristoffelPrimitive -- the image of the upper half-plane is bounded.
• TauCeti.closure_image_schwarzChristoffelPrimitive -- its closure is the image together with the compactified boundary path.
• TauCeti.continuousOn_extendFrom_schwarzChristoffelPrimitive -- the extension is continuous on the closed upper half-plane.
• TauCeti.exists_forall_dist_schwarzChristoffelPrimitive_le -- the primitive approaches its vertex at infinity uniformly outside a large ball.
• TauCeti.frontier_image_schwarzChristoffelPrimitive -- its frontier is the part of the boundary path outside the image.
• TauCeti.image_schwarzChristoffelPrimitive_subset_filledHull -- the image lies in the filled hull of the boundary path.
• TauCeti.image_schwarzChristoffelPrimitive_subset_interior_closedConvexHull -- the image lies in the interior of the closed convex hull of the boundary path.
• TauCeti.connectedComponentIn_subset_image_schwarzChristoffelPrimitive -- a complementary component of the boundary path meeting the image lies in the image.
• TauCeti.image_schwarzChristoffelPrimitive_eq_of_subset -- a preconnected set avoiding the boundary path and containing the image is the image.
• TauCeti.isClosed_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive -- under integrability at the finite prevertices alone, the preimage of a closed set avoiding the boundary values on ℝ is closed.
• TauCeti.isCompact_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive -- the preimage of a closed set avoiding the boundary path is compact.

References

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

theorem TauCeti.isOpen_image_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {s : Set ℂ} (hs : IsOpen s) (hsH : s ⊆ UpperHalfPlane.upperHalfPlaneSet) : IsOpen (schwarzChristoffelPrimitive a e z₀ '' s)

The Schwarz--Christoffel primitive is an open map on the upper half-plane. Its derivative is the integrand, which never vanishes there, so the inverse function theorem makes the image of every neighbourhood a neighbourhood.

theorem TauCeti.continuousOn_extendFrom_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) : ContinuousOn (extendFrom UpperHalfPlane.upperHalfPlaneSet (schwarzChristoffelPrimitive a e z₀)) (closure UpperHalfPlane.upperHalfPlaneSet)

The extendFrom extension of the primitive to the closed upper half-plane is continuous there, under integrability at every finite prevertex.

theorem TauCeti.exists_forall_dist_schwarzChristoffelPrimitive_le {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hinfty : ∑ i : ι, e i < -1) {ε : ℝ} (hε : 0 < ε) : ∃ (R : ℝ), ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, R ≤ ‖z‖ → dist (schwarzChristoffelPrimitive a e z₀ z) (schwarzChristoffelVertexAtInfinity a e z₀) ≤ ε

Far out in the upper half-plane the primitive stays within any prescribed distance of the vertex at infinity.

theorem TauCeti.isBounded_image_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : Bornology.IsBounded (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet)

The image of the Schwarz--Christoffel primitive is bounded when every finite prevertex is integrable and the total exponent is less than -1.

theorem TauCeti.closure_image_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : closure (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) = schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ∪ Set.range (schwarzChristoffelCompactifiedBoundary a e z₀)

The closure of the image of the Schwarz--Christoffel primitive is the image together with the compactified boundary path. Every point of the path is a limit of the primitive from the upper half-plane, and conversely every limit point of the image outside it lies on the path.

theorem TauCeti.frontier_image_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : frontier (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) = Set.range (schwarzChristoffelCompactifiedBoundary a e z₀) \ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet

The frontier of the image of the Schwarz--Christoffel primitive is the part of the compactified boundary path that the image does not cover.

theorem TauCeti.image_schwarzChristoffelPrimitive_subset_filledHull {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ filledHull (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))

The image of the Schwarz--Christoffel primitive misses the unbounded complementary component of its boundary path: it lies in the filled hull of that path.

theorem TauCeti.image_schwarzChristoffelPrimitive_subset_interior_closedConvexHull {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ interior ((closedConvexHull ℝ) (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀)))

The image of the Schwarz--Christoffel primitive lies in the interior of the closed convex hull of its compactified boundary path. The filled hull of a nonempty set lies in its closed convex hull. Since the primitive has open image, that containment automatically improves to containment in the interior.

theorem TauCeti.connectedComponentIn_subset_image_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) {w : ℂ} (hw : w ∈ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (hwP : w ∉ Set.range (schwarzChristoffelCompactifiedBoundary a e z₀)) : connectedComponentIn (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))ᶜ w ⊆ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet

A complementary component of the boundary path that meets the image lies in the image. The component is preconnected and avoids the path, which contains the frontier of the open image.

theorem TauCeti.image_schwarzChristoffelPrimitive_eq_of_subset {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) {W : Set ℂ} (hW : IsPreconnected W) (hWP : Disjoint W (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))) (hFW : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ W) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet = W

A preconnected set avoiding the boundary path and containing the image is the image.

theorem TauCeti.isClosed_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) {K : Set ℂ} (hK : IsClosed K) (hKB : Disjoint K (Set.range (schwarzChristoffelBoundary a e z₀))) : IsClosed (UpperHalfPlane.upperHalfPlaneSet ∩ schwarzChristoffelPrimitive a e z₀ ⁻¹' K)

The points of the upper half-plane sent into a closed set avoiding the boundary are a closed set. If every finite prevertex is integrable and K is a closed set disjoint from the range of the boundary map on ℝ, then upperHalfPlaneSet ∩ F ⁻¹' K is closed in ℂ.

theorem TauCeti.isCompact_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) {K : Set ℂ} (hK : IsClosed K) (hKP : Disjoint K (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))) : IsCompact (UpperHalfPlane.upperHalfPlaneSet ∩ schwarzChristoffelPrimitive a e z₀ ⁻¹' K)

The Schwarz--Christoffel primitive is proper over the complement of its boundary path. The points of the upper half-plane that the primitive sends into a closed set K avoiding the compactified boundary path form a compact set.