A single boundary sheet for Schwarz--Christoffel maps with several ends

A finite boundary value with just one spherical boundary parameter confines all nearby interior preimages to that parameter, provided the value is not attained in the interior. At a regular edge, holomorphic continuation is locally injective, so this confinement produces a globally singleton interior fiber.

If the image avoids the finite boundary trace, constancy of the sheet count then makes the primitive globally injective and a bijection onto a complementary component. Only one regular boundary value must have a unique parameter. In particular, logarithmic ends may all map to infinity, and other boundary values may have several parameters. Boundary avoidance is still necessary and is not inferred from the local edge geometry.

Local injectivity comes from exists_injOn_schwarzChristoffelPrimitive_continuation in TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.RegularEdge.

References

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

theorem TauCeti.exists_ball_preimage_schwarzChristoffelPrimitive_subset_of_unique_boundary_value {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) (x : ℝ) (hx : -1 < ∑ i : ι with a i = x, e i) (hnot : schwarzChristoffelBoundary a e z₀ x ∉ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (hunique : ∀ (t : OnePoint ℝ), schwarzChristoffelSphereBoundary a e z₀ t = schwarzChristoffelSphereBoundary a e z₀ ↑x → t = ↑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 finite boundary value with a unique spherical boundary parameter, all interior preimages lie in any prescribed neighborhood of that parameter. The chosen boundary value must not be attained in the interior; other boundary values may be attained there.

theorem TauCeti.exists_schwarzChristoffelPrimitive_fiber_eq_singleton_of_unique_boundary_value {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q) (hnot : schwarzChristoffelBoundary a e z₀ x ∉ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (hunique : ∀ (t : OnePoint ℝ), schwarzChristoffelSphereBoundary a e z₀ t = schwarzChristoffelSphereBoundary a e z₀ ↑x → t = ↑x) : ∃ (τ : UpperHalfPlane), (fun (z : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑z) ⁻¹' {schwarzChristoffelPrimitive a e z₀ ↑τ} = {τ}

A regular boundary value with one spherical boundary parameter and no interior preimage produces a globally singleton interior fiber. No global boundary avoidance or injectivity is required. Logarithmic ends elsewhere are allowed.

theorem TauCeti.injOn_schwarzChristoffelPrimitive_of_unique_boundary_value {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) (havoid : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (schwarzChristoffelFiniteBoundary a e z₀)) {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q) (hunique : ∀ (t : OnePoint ℝ), schwarzChristoffelSphereBoundary a e z₀ t = schwarzChristoffelSphereBoundary a e z₀ ↑x → t = ↑x) : Set.InjOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet

One boundary sheet implies global univalence. If the image avoids its finite boundary trace, a single uniquely parametrized regular boundary value forces injectivity throughout the upper half-plane. The spherical boundary need not be injective at any other value.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_connectedComponentIn_of_unique_boundary_value {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) (havoid : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (schwarzChristoffelFiniteBoundary a e z₀)) {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q) (hunique : ∀ (t : OnePoint ℝ), schwarzChristoffelSphereBoundary a e z₀ t = schwarzChristoffelSphereBoundary a e z₀ ↑x → t = ↑x) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet (connectedComponentIn (schwarzChristoffelFiniteBoundary a e z₀)ᶜ (schwarzChristoffelPrimitive a e z₀ ↑z₀))

The component mapping theorem from one boundary sheet. Under boundary avoidance, one uniquely parametrized regular boundary value makes the primitive a bijection onto the complementary component of the finite boundary trace containing its base-point image. Neither simple connectivity of that component nor global boundary injectivity is assumed.