Uniqueness of Schwarz--Christoffel parameters

A Schwarz--Christoffel map A * F + B, where F is the normalized primitive for real prevertices a i, exponents e i and base point z₀, is described by the parameters a, e, A and B. This file shows that, once the prevertices are known and distinct, the map determines the other parameters: on the upper half-plane its derivative A * ∏ i, (z - a i) ^ e i has logarithmic derivative ∑ i, e i / (z - a i), whose coefficients are determined by the function.

Combined with TauCeti.eq_and_eqOn_of_bijOn_schwarzChristoffelPrimitive, this gives the uniqueness theorem for the Schwarz--Christoffel representation of a bounded polygonal Jordan domain: two representations A * F + B and A' * F' + B' with the same vertices that share three prevertices have the same prevertices, the same exponents and A' = A, while B' = A * F z₀' + B accounts for the base points z₀ and z₀'; so B' = B when the base points coincide.

Main results

• TauCeti.eqOn_const_mul_schwarzChristoffelIntegrand_iff -- with distinct prevertices and A ≠ 0, two multiples of Schwarz--Christoffel integrands agree on the upper half-plane exactly when their exponents and their constants agree.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_iff -- the same for affine images of normalized Schwarz--Christoffel primitives, where the additive constants differ by the change of base point.
• TauCeti.param_eq_of_bijOn_schwarzChristoffelPrimitive -- two Schwarz--Christoffel representations of a bounded Jordan domain with the same vertices that share three distinct prevertices satisfy a' = a, e' = e, A' = A and B' = A * F z₀' + B, so B' = B for a common base point.

References

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

theorem TauCeti.eqOn_const_mul_schwarzChristoffelIntegrand_iff {ι : Type u_1} [Fintype ι] {a : ι → ℝ} (ha : Function.Injective a) {e e' : ι → ℝ} {A A' : ℂ} (hA : A ≠ 0) : Set.EqOn (fun (z : ℂ) => A' * schwarzChristoffelIntegrand a e' z) (fun (z : ℂ) => A * schwarzChristoffelIntegrand a e z) UpperHalfPlane.upperHalfPlaneSet ↔ e' = e ∧ A' = A

The integrand determines its exponents and constant. For distinct real prevertices a i and A ≠ 0, two multiples A' * ∏ i, (z - a i) ^ e' i and A * ∏ i, (z - a i) ^ e i of Schwarz--Christoffel integrands agree on the upper half-plane if and only if e' = e and A' = A.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_iff {ι : Type u_1} [Fintype ι] {a : ι → ℝ} (ha : Function.Injective a) {e e' : ι → ℝ} (z₀ z₀' : UpperHalfPlane) {A A' B B' : ℂ} (hA : A ≠ 0) : Set.EqOn (fun (z : ℂ) => A' * schwarzChristoffelPrimitive a e' z₀' z + B') (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet ↔ e' = e ∧ A' = A ∧ B' = A * schwarzChristoffelPrimitive a e z₀ ↑z₀' + B

A Schwarz--Christoffel map determines its exponents and constants. For distinct real prevertices a i and A ≠ 0, the affine images A' * F' + B' and A * F + B of the normalized Schwarz--Christoffel primitives F' for (a, e', z₀') and F for (a, e, z₀) agree on the upper half-plane if and only if e' = e, A' = A and B' = A * F z₀' + B. In particular, with a common base point the two maps agree exactly when all of their parameters do.

theorem TauCeti.param_eq_of_bijOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] {U : Set ℂ} (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {a e a' e' : ι → ℝ} (ha : Function.Injective a) (he : ∀ (i : ι), -1 < ∑ l : ι with a l = a i, e l) (he' : ∀ (i : ι), -1 < ∑ l : ι with a' l = a' i, e' l) (z₀ z₀' : UpperHalfPlane) {A B A' B' : ℂ} (hf : Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U) (hf' : Set.BijOn (fun (z : ℂ) => A' * schwarzChristoffelPrimitive a' e' z₀' z + B') UpperHalfPlane.upperHalfPlaneSet U) (hv : ∀ (i : ι), A' * schwarzChristoffelVertex a' e' z₀' i + B' = A * schwarzChristoffelVertex a e z₀ i + B) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hi : a' i = a i) (hj : a' j = a j) (hk : a' k = a k) : a' = a ∧ e' = e ∧ A' = A ∧ B' = A * schwarzChristoffelPrimitive a e z₀ ↑z₀' + B

Uniqueness of the Schwarz--Christoffel parameters. Let A * F + B and A' * F' + B' be affine images of normalized Schwarz--Christoffel primitives, for (a, e, z₀) and (a', e', z₀'), whose total exponents at each prevertex are greater than -1. Suppose both map the upper half-plane bijectively onto the same bounded domain whose frontier is a Jordan curve, and send each prevertex to the same vertex. If the prevertices a i are distinct and a' agrees with a at three of them, then a' = a, e' = e, A' = A and B' = A * F z₀' + B, which is B when z₀' = z₀.