A Schwarz--Christoffel strip with two logarithmic ends

Two distinct real prevertices, each of exponent -1, give a conformal map onto a strip. For a 0 < a 1, the logarithm of (z - a 1) / (z - a 0) is an affine image of the normalized Schwarz--Christoffel primitive. It maps the upper half-plane bijectively onto the strip 0 < im w < π.

Both finite prevertices represent ends at infinity; the parameter at infinity represents a regular boundary point. Thus this is a polygon with two ends, rather than the one-ended Jordan-curve situation. The image theorem imposes no boundary simplicity or boundary-avoidance assumption.

References

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

@[simp]

theorem TauCeti.const_mul_schwarzChristoffelPrimitive_two_neg_one_add_eq_log (a : Fin 2 → ℝ) (ha : a 0 ≠ a 1) (z₀ : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : (↑(a 1) - ↑(a 0)) * schwarzChristoffelPrimitive a (fun (x : Fin 2) => -1) z₀ z + Complex.log ((↑z₀ - ↑(a 1)) / (↑z₀ - ↑(a 0))) = Complex.log ((z - ↑(a 1)) / (z - ↑(a 0)))

The explicit Schwarz--Christoffel formula for a strip. Two distinct prevertices of exponent -1 give the principal logarithm of their fractional-linear ratio, after scaling by their separation and translating by the value at the base point.

theorem TauCeti.bijOn_const_mul_schwarzChristoffelPrimitive_two_neg_one_add (a : Fin 2 → ℝ) (ha : a 0 < a 1) (z₀ : UpperHalfPlane) : Set.BijOn (fun (z : ℂ) => (↑(a 1) - ↑(a 0)) * schwarzChristoffelPrimitive a (fun (x : Fin 2) => -1) z₀ z + Complex.log ((↑z₀ - ↑(a 1)) / (↑z₀ - ↑(a 0)))) UpperHalfPlane.upperHalfPlaneSet {w : ℂ | w.im ∈ Set.Ioo 0 Real.pi}

The Schwarz--Christoffel map onto a strip with two logarithmic ends. The affine image of the normalized primitive for two ordered prevertices, both of exponent -1, is a bijection onto the entire strip of height π.

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_strip (a : Fin 2 → ℝ) (ha : Function.Injective a) (z₀ : UpperHalfPlane) {l h : ℝ} (hlh : l < h) : ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a (fun (x : Fin 2) => -1) z₀ z + B) UpperHalfPlane.upperHalfPlaneSet {w : ℂ | w.im ∈ Set.Ioo l h}

Every horizontal strip has a two-ended Schwarz--Christoffel representation. For any two distinct real prevertices and any base point, an affine image of their normalized primitive with exponents -1 maps the upper half-plane bijectively onto any prescribed nonempty horizontal strip. The multiplicative constant is nonzero.