The Schwarz--Christoffel image of a simple boundary polygon

Let F = schwarzChristoffelPrimitive a e z₀ and let P be the range of the compactified boundary path schwarzChristoffelCompactifiedBoundary a e z₀, under the standing assumptions of TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Image: every finite prevertex is integrable and the total exponent is less than -1. No convexity is assumed: the turning exponents may have either sign, so the polygon may have reentrant corners.

When the compactified boundary path is injective, P is a Jordan curve, and the image of the upper half-plane does not meet P: the image is open and lies in the filled hull of P, and an open set in the filled hull of a Jordan curve misses the curve (TauCeti.IsJordanCurve.disjoint_of_isOpen_of_subset_filledHull). Consequently the image is exactly one complementary component of P, and its frontier is all of P.

Over that component, TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive therefore exhibits the whole upper half-plane as a covering space. For convex data the covering is a bijection onto the interior of the polygon, TauCeti.bijOn_schwarzChristoffelPrimitive_interior_closedConvexHull.

Main results

• TauCeti.disjoint_image_schwarzChristoffelPrimitive_range — the image of the upper half-plane misses a simple compactified boundary path.
• TauCeti.image_schwarzChristoffelPrimitive_eq_connectedComponentIn — the image is the component of the complement of the path containing F z₀.
• TauCeti.frontier_image_schwarzChristoffelPrimitive_eq_range — the frontier of the image is the whole path.
• TauCeti.exists_ball_preimage_schwarzChristoffelPrimitive_subset_of_boundary_injective — preimages of values near a simple boundary point lie near its unique boundary preimage.

References

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

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

The Schwarz--Christoffel image misses a simple boundary path. If every finite prevertex is integrable, the total exponent is less than -1, and the compactified boundary path is injective, then the primitive sends no point of the upper half-plane onto that path.

theorem TauCeti.image_schwarzChristoffelPrimitive_eq_connectedComponentIn {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet = connectedComponentIn (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))ᶜ (schwarzChristoffelPrimitive a e z₀ ↑z₀)

The Schwarz--Christoffel image is a complementary component of a simple boundary path. Under the hypotheses of TauCeti.disjoint_image_schwarzChristoffelPrimitive_range, the image of the upper half-plane is the component of the complement of the compactified boundary path containing the image of the base point.

@[simp]

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

The frontier of the Schwarz--Christoffel image is a simple boundary path. Under the hypotheses of TauCeti.disjoint_image_schwarzChristoffelPrimitive_range, the frontier of the image of the upper half-plane is the whole range of the compactified boundary path.

theorem TauCeti.exists_ball_preimage_schwarzChristoffelPrimitive_subset_of_boundary_injective {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) (x : ℝ) {U : Set ℂ} (hU : IsOpen U) (hxU : ↑x ∈ U) : ∃ ε > 0, ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, schwarzChristoffelPrimitive a e z₀ z ∈ Metric.ball (schwarzChristoffelBoundary a e z₀ x) ε → z ∈ U

Near a point of a simple compactified boundary, every preimage under the primitive lies near its unique boundary preimage. This includes preimages tending to infinity: the limit there is the value at the compactification point, which is distinct from the chosen boundary value.