Uniqueness of Schwarz--Christoffel prevertices

A bounded polygonal Jordan domain is the image of the upper half-plane under an affine image A * F + B of a normalized Schwarz--Christoffel primitive F, with the prevertex a i going to the vertex v i; this is TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_frontier. This file shows that two such representations have prevertex families with the same cross-ratios. If they share three prevertices, they share all of them, and the two maps coincide on the upper half-plane.

The argument is the boundary correspondence of two conformal maps onto a Jordan domain (TauCeti.crossRatio_eq_of_tendsto_of_bijOn_upperHalfPlaneSet and TauCeti.eqOn_upperHalfPlaneSet_of_tendsto_of_bijOn). The Schwarz--Christoffel map tends to the vertex v i at the prevertex a i.

Main results

• TauCeti.exists_prevertex_cayley_automorphism -- the boundary correspondence of two representations is one disc automorphism in Cayley coordinates, simultaneously at every prevertex.
• TauCeti.crossRatio_eq_of_bijOn_schwarzChristoffelPrimitive -- two Schwarz--Christoffel representations of a Jordan domain with the same vertices have prevertices with the same cross-ratios.
• TauCeti.eq_and_eqOn_of_bijOn_schwarzChristoffelPrimitive -- if two such representations share three prevertices, then they share all prevertices and the two maps coincide.

References

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

theorem TauCeti.exists_prevertex_cayley_automorphism {ι : Type u_1} [Fintype ι] {U : Set ℂ} (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {a e a' e' : ι → ℝ} (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) : ∃ (u : Circle) (c : Complex.UnitDisc), ∀ (i : ι), (↑(a' i) - Complex.I) / (↑(a' i) + Complex.I) = ↑u * (((↑(a i) - Complex.I) / (↑(a i) + Complex.I) - ↑c) / (1 - (starRingEnd ℂ) ↑c * ((↑(a i) - Complex.I) / (↑(a i) + Complex.I))))

Prevertex correspondence in Cayley coordinates. For two Schwarz--Christoffel representations of the same bounded Jordan domain with matching vertices, one standard disc automorphism carries the Cayley coordinate of every prevertex of the first representation to the corresponding coordinate of the second.

theorem TauCeti.crossRatio_eq_of_bijOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] {U : Set ℂ} (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {a e a' e' : ι → ℝ} (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 l : ι) : (a' i - a' k) * (a' j - a' l) / ((a' i - a' l) * (a' j - a' k)) = (a i - a k) * (a j - a l) / ((a i - a l) * (a j - a k))

Schwarz--Christoffel prevertices have equal cross-ratios. Let A * F + B and A' * F' + B' be affine images of normalized Schwarz--Christoffel primitives whose total exponents at each prevertex exceed -1. Suppose both map the upper half-plane bijectively onto the same bounded domain whose frontier is a Jordan curve. Suppose also that they send each prevertex to the same vertex. Then the prevertex families a and a' have the same cross-ratios.

theorem TauCeti.eq_and_eqOn_of_bijOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] {U : Set ℂ} (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {a e a' e' : ι → ℝ} (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 : a i ≠ a j) (hik : a i ≠ a k) (hjk : a j ≠ a k) (hi : a' i = a i) (hj : a' j = a j) (hk : a' k = a k) : a' = a ∧ Set.EqOn (fun (z : ℂ) => A' * schwarzChristoffelPrimitive a' e' z₀' z + B') (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet

Three prevertices determine a Schwarz--Christoffel representation. Let A * F + B and A' * F' + B' be affine images of normalized Schwarz--Christoffel primitives 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. Suppose also that they send each prevertex to the same vertex. If a and a' agree at three distinct prevertices, then a' = a and the two maps coincide on the upper half-plane.