Global turning of the Schwarz--Christoffel boundary

For strictly ordered prevertices, the direction angle on the interval following the i-th prevertex is π times the sum of the exponents at all later prevertices. Consequently negative exponents make these angles strictly increase as the boundary is traversed from left to right.

Under the classical closing condition ∑ i, e i = -2, every edge angle at an indexed prevertex lies in the fundamental interval (-2π, 0], so the angle increase between distinct indexed finite prevertices i < j lies strictly between zero and 2π. All finite edge directions are therefore distinct, while the angles on the two unbounded intervals differ by exactly 2π. This is the global turning-order input for separating nonadjacent sides of the Schwarz--Christoffel polygon; the local fact that consecutive sides form genuine corners is proved in SchwarzChristoffel.Turning.

Main results

• TauCeti.schwarzChristoffelEdgeAngle_comp_strictMono -- negative exponents make the edge angles at successive prevertices strictly increase.
• TauCeti.schwarzChristoffelEdgeAngle_sub_mem_Ioo_two_pi -- the angle increase between distinct indexed finite prevertices i < j lies in (0, 2π) when the total exponent is -2.
• TauCeti.exp_schwarzChristoffelEdgeAngle_prevertex_injective -- the finite edge directions are pairwise distinct.
• TauCeti.schwarzChristoffelEdgeAngle_eq_neg_two_pi_of_lt_first and TauCeti.schwarzChristoffelEdgeAngle_eq_zero_of_last_le -- the two unbounded edge angles are -2π and zero.

References

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

theorem TauCeti.schwarzChristoffelEdgeAngle_mem_Ioc {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (he : ∀ (i : ι), e i < 0) (hsum : ∑ i : ι, e i = -2) (i : ι) : schwarzChristoffelEdgeAngle a e (a i) ∈ Set.Ioc (-2 * Real.pi) 0

Under negative exponents summing to -2, every indexed-prevertex edge angle lies in the half-open fundamental interval (-2π, 0]. The angle can equal zero when no prevertex lies strictly to its right, while -2π occurs only before every prevertex.

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_pi_mul_sum_Ioi {ι : Type u_1} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrderTop ι] (a e : ι → ℝ) (ha : StrictMono a) (i : ι) : schwarzChristoffelEdgeAngle a e (a i) = Real.pi * ∑ k > i, e k

For strictly ordered prevertices, the edge angle following the i-th prevertex is π times the sum of the exponents at the later prevertices.

theorem TauCeti.schwarzChristoffelEdgeAngle_sub_eq_neg_pi_mul_sum_Ioc {ι : Type u_1} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrder ι] (a e : ι → ℝ) (ha : StrictMono a) {i j : ι} (hij : i ≤ j) : schwarzChristoffelEdgeAngle a e (a j) - schwarzChristoffelEdgeAngle a e (a i) = -Real.pi * ∑ k ∈ Finset.Ioc i j, e k

The increase in edge angle between two indexed prevertices is -π times the sum of the exponents in the corresponding right-closed index interval.

theorem TauCeti.schwarzChristoffelEdgeAngle_comp_strictMono {ι : Type u_1} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrder ι] (a e : ι → ℝ) (ha : StrictMono a) (he : ∀ (i : ι), e i < 0) : StrictMono fun (i : ι) => schwarzChristoffelEdgeAngle a e (a i)

Strictly ordered prevertices carrying negative exponents have strictly increasing Schwarz--Christoffel edge angles.

theorem TauCeti.schwarzChristoffelEdgeAngle_sub_mem_Ioo_two_pi {ι : Type u_1} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrder ι] (a e : ι → ℝ) (ha : StrictMono a) (he : ∀ (i : ι), e i < 0) (hsum : ∑ i : ι, e i = -2) {i j : ι} (hij : i < j) : schwarzChristoffelEdgeAngle a e (a j) - schwarzChristoffelEdgeAngle a e (a i) ∈ Set.Ioo 0 (2 * Real.pi)

Under the closing condition ∑ i, e i = -2, the edge-angle increase along any nonempty proper index interval lies strictly between zero and 2π.

The upper bound is strict because both endpoint angles lie in the fundamental interval (-2π, 0] of schwarzChristoffelEdgeAngle_mem_Ioc.

theorem TauCeti.exp_schwarzChristoffelEdgeAngle_prevertex_injective {ι : Type u_1} [Fintype ι] [LinearOrder ι] [LocallyFiniteOrder ι] (a e : ι → ℝ) (ha : StrictMono a) (he : ∀ (i : ι), e i < 0) (hsum : ∑ i : ι, e i = -2) : Function.Injective fun (i : ι) => Complex.exp (↑(schwarzChristoffelEdgeAngle a e (a i)) * Complex.I)

Under negative exponents summing to -2, the direction constants on the intervals following distinct finite prevertices are distinct. Thus no two of those directed sides have the same orientation; the repeated direction occurs only across the two ends of the compactified real line.

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_neg_two_pi_of_lt_first {n : ℕ} (a e : Fin (n + 1) → ℝ) (ha : Monotone a) (hsum : ∑ i : Fin (n + 1), e i = -2) {c : ℝ} (hc : c < a 0) : schwarzChristoffelEdgeAngle a e c = -2 * Real.pi

With total exponent -2, the Schwarz--Christoffel edge angle before the first ordered prevertex is -2π.

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_zero_of_last_le {n : ℕ} (a e : Fin (n + 1) → ℝ) (ha : Monotone a) {c : ℝ} (hc : a (Fin.last n) ≤ c) : schwarzChristoffelEdgeAngle a e c = 0

The Schwarz--Christoffel edge angle at or beyond the last ordered prevertex is zero.