Normalized Schwarz--Christoffel parameters

Positive affine changes of the real line do not change the polygonal domain represented by a Schwarz--Christoffel map. This file uses that covariance to remove the two real affine degrees of freedom from the prevertices: one chosen prevertex is placed at 0, and the distance to a second chosen prevertex is normalized to 1. Its sign is the remaining real-order choice under this positive affine normalization.

The main theorem gives this normalization for the Schwarz--Christoffel representation of a bounded polygonal Jordan domain. Thus the remaining parameters live in a finite-dimensional slice rather than carrying a redundant translation and positive scaling.

Main results

• TauCeti.exists_bijOn_normalized_schwarzChristoffelPrimitive_of_isJordanCurve_frontier -- the Schwarz--Christoffel representation of a polygonal Jordan domain can be chosen with one prevertex equal to 0 and a second at distance 1.

References

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

theorem TauCeti.exists_bijOn_normalized_schwarzChristoffelPrimitive_of_isJordanCurve_frontier {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (k : ι), e k ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {v : ι → ℂ} (hv : Function.Injective v) (hside : ∀ w ∈ frontier U, (∀ (k : ι), w ≠ v k) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (k : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v k) ρ, z ≠ v k → (z ∈ U ↔ |((z - v k) / b).arg| < (e k + 1) * Real.pi / 2)) (i j : ι) (hij : i ≠ j) : ∃ (a : ι → ℝ), Function.Injective a ∧ a i = 0 ∧ |a j| = 1 ∧ ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U ∧ ∀ (k : ι), A * schwarzChristoffelVertex a e z₀ k + B = v k

Normalized Schwarz--Christoffel parameters for a polygonal Jordan domain.

Under the polygonal boundary hypotheses, choose two distinct labelled vertices i and j. There is a Schwarz--Christoffel representation of the domain whose i-th prevertex is 0 and whose j-th prevertex has absolute value 1. Its sign is the remaining real-order choice under positive affine normalization.