Affine covariance of the Schwarz--Christoffel map

A positive affine change x ↦ c * x + d of the real prevertices extends to an automorphism of the upper half-plane. This file computes its effect on the Schwarz--Christoffel integrand and on the normalized primitive. If S = ∑ i, e i, then the integrand acquires the factor c ^ S, while the primitive acquires c ^ (S + 1) because the change of variable contributes one further factor of c.

This covariance removes the translation and positive-scaling redundancy from the prevertex parameters.

Main results

• TauCeti.schwarzChristoffelIntegrand_affine_prevertices -- covariance of the integrand.
• TauCeti.schwarzChristoffelPrimitive_affine_prevertices -- covariance of the normalized primitive.
• TauCeti.schwarzChristoffelPrimitive_affine_prevertices_of_exponent_sum_eq_neg_two -- under the closing condition, the affine change scales the primitive by the inverse scale factor.
• TauCeti.schwarzChristoffelVertex_affine_prevertices -- covariance of the boundary values.
• TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_affine_prevertices -- a positive affine change of all prevertices preserves an affine image of the primitive and its boundary values.

References

• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.

theorem TauCeti.schwarzChristoffelIntegrand_affine_prevertices {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c : ℝ} (hc : 0 < c) (d : ℝ) (z : ℂ) : schwarzChristoffelIntegrand (fun (i : ι) => c * a i + d) e (↑c * z + ↑d) = ↑c ^ ↑(∑ i : ι, e i) * schwarzChristoffelIntegrand a e z

The Schwarz--Christoffel integrand is covariant under a positive affine change of all its prevertices. The exponent of the scale factor is the total turning exponent.

theorem TauCeti.schwarzChristoffelPrimitive_affine_prevertices {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {c : ℝ} (hc : 0 < c) (d : ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelPrimitive (fun (i : ι) => c * a i + d) e (d +ᵥ ⟨c, hc⟩ • z₀) (↑c * z + ↑d) = ↑c ^ ↑(∑ i : ι, e i + 1) * schwarzChristoffelPrimitive a e z₀ z

The normalized Schwarz--Christoffel primitive is covariant under a simultaneous positive affine change of its prevertices, base point, and argument. Its scale exponent is one more than the total turning exponent.

theorem TauCeti.schwarzChristoffelPrimitive_affine_prevertices_of_exponent_sum_eq_neg_two {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {c : ℝ} (hc : 0 < c) (d : ℝ) (hsum : ∑ i : ι, e i = -2) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelPrimitive (fun (i : ι) => c * a i + d) e (d +ᵥ ⟨c, hc⟩ • z₀) (↑c * z + ↑d) = (↑c)⁻¹ * schwarzChristoffelPrimitive a e z₀ z

Under the polygonal closing condition ∑ i, e i = -2, a positive affine change x ↦ c * x + d of the prevertices, base point, and argument multiplies the normalized Schwarz--Christoffel primitive by c⁻¹.

theorem TauCeti.schwarzChristoffelVertex_affine_prevertices {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {c : ℝ} (hc : 0 < c) (d : ℝ) (j : ι) (hj : -1 < ∑ i : ι with a i = a j, e i) : schwarzChristoffelVertex (fun (i : ι) => c * a i + d) e z₀ j = ↑c ^ ↑(∑ i : ι, e i + 1) * schwarzChristoffelVertex a e z₀ j - schwarzChristoffelPrimitive (fun (i : ι) => c * a i + d) e (d +ᵥ ⟨c, hc⟩ • z₀) ↑z₀

A positive affine change of the prevertices scales their Schwarz--Christoffel boundary values by the same factor as the primitive. Keeping the original base point introduces the displayed translation, independent of the chosen prevertex.

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_affine_prevertices {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {c : ℝ} (hc : 0 < c) (d : ℝ) {A B : ℂ} {U : Set ℂ} (hbij : Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U) : ∃ (A' : ℂ), A' ≠ 0 ∧ ∃ (B' : ℂ), Set.BijOn (fun (z : ℂ) => A' * schwarzChristoffelPrimitive (fun (i : ι) => c * a i + d) e z₀ z + B') UpperHalfPlane.upperHalfPlaneSet U ∧ ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i → A' * schwarzChristoffelVertex (fun (i : ι) => c * a i + d) e z₀ j + B' = A * schwarzChristoffelVertex a e z₀ j + B

A positive affine change of all real prevertices preserves the domain represented by an affine image of the Schwarz--Christoffel primitive. The normalization point of the primitive is kept fixed; its change under reparametrization is absorbed into the additive constant. At every integrable prevertex, the adjusted affine images of the old and new boundary values agree.