Local continuation across a regular Schwarz--Christoffel edge #
At a real point away from the turning prevertices, the Schwarz--Christoffel primitive extends holomorphically through the edge. Its derivative on the edge is the positive boundary density times the edge direction, so the extension is locally injective. This gives the local sheet of the primitive needed to determine the degree of its covering of a simple polygonal domain.
References #
- L. Ahlfors, Complex Analysis, Ch. 6, Section 2.
- T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.
theorem
TauCeti.exists_injOn_schwarzChristoffelPrimitive_continuation
{ι : Type u_1}
[Fintype ι]
(a e : ι → ℝ)
(z₀ : UpperHalfPlane)
{p q x : ℝ}
(ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q)
(hx : x ∈ Set.Ioo p q)
:
∃ (U : Set ℂ),
IsOpen U ∧ ↑x ∈ U ∧ ∃ (G : ℂ → ℂ),
Set.EqOn G (schwarzChristoffelPrimitive a e z₀) (U ∩ UpperHalfPlane.upperHalfPlaneSet) ∧ Set.InjOn G U ∧ G ↑x = schwarzChristoffelBoundary a e z₀ x ∧ ∀ z ∈ U,
HasDerivAt G
(Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I) * schwarzChristoffelContinuedIntegrand a e p z)
z
At a point of a prevertex-free boundary interval, the Schwarz--Christoffel primitive has a holomorphic continuation which is injective on a neighbourhood of that point. Its value at the point is the canonical boundary value, and its derivative throughout the neighbourhood is the continued integrand times the fixed edge direction.