Local straightness of a simple Schwarz--Christoffel boundary #
At a real parameter away from the prevertices, the compactified boundary of a simple Schwarz--Christoffel polygon agrees, in a neighbourhood of its image, with an open straight segment. The global injectivity assumption matters: it prevents another part of the boundary from entering every neighbourhood of the chosen edge point. This local description is an input for identifying the complementary component mapped from the upper half-plane.
References #
- L. Ahlfors, Complex Analysis, Chapter 6, Section 2.
- T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Chapter 2.
theorem
TauCeti.exists_ball_inter_range_schwarzChristoffelCompactifiedBoundary_eq_ball_inter_openSegment
{ι : 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₀))
{p q x : ℝ}
(ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q)
(hx : x ∈ Set.Ioo p q)
:
∃ (ε : ℝ),
0 < ε ∧ Metric.ball (schwarzChristoffelBoundary a e z₀ x) ε ∩ Set.range (schwarzChristoffelCompactifiedBoundary a e z₀) = Metric.ball (schwarzChristoffelBoundary a e z₀ x) ε ∩ openSegment ℝ (schwarzChristoffelBoundary a e z₀ p) (schwarzChristoffelBoundary a e z₀ q)
Near a regular point of a simple compactified Schwarz--Christoffel boundary, the entire boundary curve agrees with the open segment traced by that edge. In particular no other edge enters this ball.