Side lengths in the Schwarz--Christoffel formula

The bounded side between two consecutive prevertices has length equal to the integral of the absolute value of the Schwarz--Christoffel integrand over the interval between them. This file packages that integral as TauCeti.schwarzChristoffelSideIntegral and identifies it with the distance between the corresponding vertices.

This is the real equation in the Schwarz--Christoffel parameter problem: after the turning exponents have fixed the directions of the sides, the prevertices must be chosen so that these integrals have the prescribed side-length ratios. The proof also records interval integrability of the density. The only singularities on a bounded side occur at its endpoints; separating those two factors reduces integrability to Euler's beta integral.

Main results

• TauCeti.intervalIntegrable_schwarzChristoffelDensity -- the density is integrable between consecutive prevertices.
• TauCeti.schwarzChristoffelSideIntegral_pos -- every such side integral is positive.
• TauCeti.dist_schwarzChristoffelVertex_succ_eq_sideIntegral -- the integral is the geometric length of the corresponding polygon side.

References

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

noncomputable def TauCeti.schwarzChristoffelSideIntegral {n : ℕ} (a e : Fin (n + 1) → ℝ) (i : Fin n) : ℝ

The oriented candidate side-length integral between consecutive prevertices a i and a (i + 1). For strictly ordered prevertices and integrable endpoint singularities it is positive and equals the geometric side length, as proved below.

Equations

• TauCeti.schwarzChristoffelSideIntegral a e i = ∫ (x : ℝ) in a i.castSucc..a i.succ, TauCeti.schwarzChristoffelDensity a e x

theorem TauCeti.intervalIntegrable_schwarzChristoffelDensity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q : ℝ} (hpq : p < q) (ha : ∀ (k : ι), e k ≠ 0 → a k ∉ Set.Ioo p q) (hleft : -1 < ∑ k : ι with a k = p, e k) (hright : -1 < ∑ k : ι with a k = q, e k) : IntervalIntegrable (schwarzChristoffelDensity a e) MeasureTheory.volume p q

The Schwarz--Christoffel density is interval integrable between two distinct endpoints when there is no nonzero-exponent prevertex in the open interval and the total exponent at each endpoint is greater than -1.

theorem TauCeti.intervalIntegrable_schwarzChristoffelDensity_succ {n : ℕ} (a e : Fin (n + 1) → ℝ) (ha : StrictMono a) (i : Fin n) (hleft : -1 < e i.castSucc) (hright : -1 < e i.succ) : IntervalIntegrable (schwarzChristoffelDensity a e) MeasureTheory.volume (a i.castSucc) (a i.succ)

For strictly ordered prevertices, the density is integrable between consecutive prevertices when the two endpoint exponents are greater than -1.

theorem TauCeti.schwarzChristoffelVertex_succ_sub_eq_sideIntegral_mul {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i : Fin n) (hleft : -1 < e i.castSucc) (hright : -1 < e i.succ) : schwarzChristoffelVertex a e z₀ i.succ - schwarzChristoffelVertex a e z₀ i.castSucc = ↑(schwarzChristoffelSideIntegral a e i) * Complex.exp (↑(schwarzChristoffelEdgeAngle a e (a i.castSucc)) * Complex.I)

The vector of a bounded Schwarz--Christoffel side is its density integral times the unit vector in the side's fixed direction.

theorem TauCeti.schwarzChristoffelSideIntegral_pos {n : ℕ} (a e : Fin (n + 1) → ℝ) (ha : StrictMono a) (i : Fin n) (hleft : -1 < e i.castSucc) (hright : -1 < e i.succ) : 0 < schwarzChristoffelSideIntegral a e i

Every bounded Schwarz--Christoffel side has positive integral length when its endpoint singularities are integrable.

theorem TauCeti.dist_schwarzChristoffelVertex_succ_eq_sideIntegral {n : ℕ} (a e : Fin (n + 1) → ℝ) (z₀ : UpperHalfPlane) (ha : StrictMono a) (i : Fin n) (hleft : -1 < e i.castSucc) (hright : -1 < e i.succ) : dist (schwarzChristoffelVertex a e z₀ i.succ) (schwarzChristoffelVertex a e z₀ i.castSucc) = schwarzChristoffelSideIntegral a e i

The side-length integral is the Euclidean distance between the corresponding consecutive Schwarz--Christoffel vertices.