The Schwarz--Christoffel formula on the unit disc

The disc form of the Schwarz--Christoffel formula writes a conformal map of the open unit disc onto a polygon as

f ζ = A * ∫₀^ζ ∏ i, (1 - ξ / w i) ^ e i dξ + B,

with prevertices w i on the unit circle and turning exponents e i, the interior angle at the corresponding vertex being (e i + 1) * π. This file defines the integrand and its primitive normalized at the centre of the disc, and relates them to the upper-half-plane form of TauCeti.schwarzChristoffelPrimitive through the inverse Cayley transform ζ ↦ i (1 + ζ) / (1 - ζ).

On the open disc each factor 1 - ζ / w i has positive real part, so the principal powers are holomorphic and nowhere zero, and the logarithmic derivative of the integrand is ∑ i, e i / (ζ - w i). Composing a half-plane Schwarz--Christoffel map with the inverse Cayley transform turns the pre-Schwarzian ∑ i, e i / (z - a i) into ∑ i, e i / (ζ - w i) + (∑ i, e i + 2) / (1 - ζ), where w i is the Cayley image (a i - i) / (a i + i) of the prevertex a i. The spurious pole at 1, the image of ∞, disappears when the turning exponents sum to -2, which is the closing condition of a bounded polygon. Under that condition the two forms of the formula differ by an affine map, so every half-plane Schwarz--Christoffel representation of a domain yields a disc representation, with the prevertex limits carried along. Without the closing condition, the pole is retained as an additional prevertex at 1, with exponent -∑ i, e i - 2. This gives the disc form for unbounded polygons as well, including divergence at their vertex at infinity.

Main definitions

• TauCeti.schwarzChristoffelDiscIntegrand -- the product ∏ i, (1 - ζ / w i) ^ e i.
• TauCeti.schwarzChristoffelDiscPrimitive -- its primitive on the disc vanishing at 0.

Main results

• TauCeti.hasDerivAt_schwarzChristoffelDiscPrimitive -- the primitive has the integrand as its derivative throughout the open unit disc.
• TauCeti.logDeriv_deriv_schwarzChristoffelDiscPrimitive -- the Schwarz--Christoffel differential equation on the disc.
• TauCeti.eqOn_schwarzChristoffelDiscPrimitive -- the derivative and normalization characterize the primitive on the disc.
• TauCeti.eqOn_schwarzChristoffelPrimitive_comp_I_mul_one_add_div_one_sub_with_infty -- unrestricted Cayley transport with the additional prevertex at infinity.
• TauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_with_infty_of_bijOn -- unrestricted transport of a bijection, its finite boundary limits, and divergence at infinity.

References

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

noncomputable def TauCeti.schwarzChristoffelDiscIntegrand {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) (ζ : ℂ) : ℂ

The disc Schwarz--Christoffel integrand with prevertices w i on the unit circle and turning exponents e i, namely ∏ i, (1 - ζ / w i) ^ e i with principal powers. For a polygon with interior angle α i at the vertex corresponding to w i, the classical choice is e i = α i / π - 1; the definition itself imposes no condition on the exponents.

Equations

• TauCeti.schwarzChristoffelDiscIntegrand w e ζ = ∏ i : ι, (1 - ζ / ↑(w i)) ^ ↑(e i)

theorem TauCeti.schwarzChristoffelDiscIntegrand_def {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) (ζ : ℂ) : schwarzChristoffelDiscIntegrand w e ζ = ∏ i : ι, (1 - ζ / ↑(w i)) ^ ↑(e i)

The disc Schwarz--Christoffel integrand is the product of its principal-power factors.

@[simp]

theorem TauCeti.schwarzChristoffelDiscIntegrand_zero {ι : Type u_1} [Fintype ι] (w : ι → Circle) : schwarzChristoffelDiscIntegrand w 0 = 1

With every turning exponent zero, the disc Schwarz--Christoffel integrand is constant one.

@[simp]

theorem TauCeti.schwarzChristoffelDiscIntegrand_apply_zero {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) : schwarzChristoffelDiscIntegrand w e 0 = 1

The disc Schwarz--Christoffel integrand takes the value one at the centre of the disc.

@[simp]

theorem TauCeti.schwarzChristoffelDiscIntegrand_option_zero {ι : Type u_1} [Fintype ι] (v : Circle) (w : ι → Circle) (e : ι → ℝ) : schwarzChristoffelDiscIntegrand (Option.elim' v w) (Option.elim' 0 e) = schwarzChristoffelDiscIntegrand w e

Adding a prevertex with exponent zero does not change the disc integrand.

theorem TauCeti.differentiableOn_schwarzChristoffelDiscIntegrand {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) : DifferentiableOn ℂ (schwarzChristoffelDiscIntegrand w e) (Metric.ball 0 1)

The disc Schwarz--Christoffel integrand is holomorphic on the open unit disc.

theorem TauCeti.schwarzChristoffelDiscIntegrand_ne_zero {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : schwarzChristoffelDiscIntegrand w e ζ ≠ 0

The disc Schwarz--Christoffel integrand has no zero in the open unit disc.

theorem TauCeti.logDeriv_schwarzChristoffelDiscIntegrand {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : logDeriv (schwarzChristoffelDiscIntegrand w e) ζ = ∑ i : ι, ↑(e i) / (ζ - ↑(w i))

The logarithmic derivative of the disc Schwarz--Christoffel integrand is the sum of the simple fractions e i / (ζ - w i), whose poles lie on the unit circle.

noncomputable def TauCeti.schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) (ζ : ℂ) : ℂ

The normalized disc Schwarz--Christoffel primitive: the integral of schwarzChristoffelDiscIntegrand w e from the centre 0 of the disc to ζ, along a horizontal segment followed by a vertical one. The definition is total on ℂ, but its analytic interpretation is asserted on the open unit disc.

Equations

• TauCeti.schwarzChristoffelDiscPrimitive w e ζ = Complex.wedgeIntegral 0 ζ (TauCeti.schwarzChristoffelDiscIntegrand w e)

theorem TauCeti.schwarzChristoffelDiscPrimitive_def {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) (ζ : ℂ) : schwarzChristoffelDiscPrimitive w e ζ = Complex.wedgeIntegral 0 ζ (schwarzChristoffelDiscIntegrand w e)

The normalized disc primitive as a wedge integral from the disc centre.

@[simp]

theorem TauCeti.schwarzChristoffelDiscPrimitive_apply_zero {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) : schwarzChristoffelDiscPrimitive w e 0 = 0

The normalized disc Schwarz--Christoffel primitive vanishes at the centre of the disc.

@[simp]

theorem TauCeti.schwarzChristoffelDiscPrimitive_option_zero {ι : Type u_1} [Fintype ι] (v : Circle) (w : ι → Circle) (e : ι → ℝ) : schwarzChristoffelDiscPrimitive (Option.elim' v w) (Option.elim' 0 e) = schwarzChristoffelDiscPrimitive w e

Adding a prevertex with exponent zero does not change the disc primitive.

theorem TauCeti.hasDerivAt_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : HasDerivAt (schwarzChristoffelDiscPrimitive w e) (schwarzChristoffelDiscIntegrand w e ζ) ζ

The derivative of the normalized disc Schwarz--Christoffel primitive is its integrand throughout the open unit disc.

@[simp]

theorem TauCeti.deriv_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : deriv (schwarzChristoffelDiscPrimitive w e) ζ = schwarzChristoffelDiscIntegrand w e ζ

The derivative of the normalized disc Schwarz--Christoffel primitive on the open unit disc.

theorem TauCeti.differentiableOn_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) : DifferentiableOn ℂ (schwarzChristoffelDiscPrimitive w e) (Metric.ball 0 1)

The normalized disc Schwarz--Christoffel primitive is holomorphic on the open unit disc.

theorem TauCeti.conformalAt_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : ConformalAt (schwarzChristoffelDiscPrimitive w e) ζ

The normalized disc Schwarz--Christoffel primitive is conformal at every point of the open unit disc.

theorem TauCeti.logDeriv_deriv_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : logDeriv (deriv (schwarzChristoffelDiscPrimitive w e)) ζ = ∑ i : ι, ↑(e i) / (ζ - ↑(w i))

The Schwarz--Christoffel differential equation on the disc. Throughout the open unit disc the pre-Schwarzian F'' / F' of the normalized disc primitive F is the sum of simple fractions ∑ i, e i / (ζ - w i).

theorem TauCeti.eqOn_schwarzChristoffelDiscPrimitive {ι : Type u_1} [Fintype ι] (w : ι → Circle) (e : ι → ℝ) {g : ℂ → ℂ} (hg : ∀ ζ ∈ Metric.ball 0 1, HasDerivAt g (schwarzChristoffelDiscIntegrand w e ζ) ζ) (hg₀ : g 0 = 0) : Set.EqOn g (schwarzChristoffelDiscPrimitive w e) (Metric.ball 0 1)

A primitive of the disc Schwarz--Christoffel integrand vanishing at the centre agrees with schwarzChristoffelDiscPrimitive throughout the open unit disc.

Comparison with the upper-half-plane form

theorem TauCeti.eqOn_schwarzChristoffelPrimitive_comp_I_mul_one_add_div_one_sub_with_infty {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : Set.EqOn (fun (ζ : ℂ) => schwarzChristoffelPrimitive a e z₀ (Complex.I * (1 + ζ) / (1 - ζ))) (fun (ζ : ℂ) => 2 * Complex.I * schwarzChristoffelIntegrand a e Complex.I * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-∑ i : ι, e i - 2) e) ζ + schwarzChristoffelPrimitive a e z₀ Complex.I) (Metric.ball 0 1)

Cayley transport with a prevertex at infinity. For arbitrary real exponents, the half-plane primitive in disc coordinates equals the disc primitive with the finite Cayley prevertices and an additional prevertex 1 of exponent -∑ i, e i - 2, up to explicit affine constants. For an unbounded polygon with sector opening β * π at infinity, that exponent is -β - 1. No closing or angle restriction is required for this analytic identity.

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_with_infty_of_bijOn {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {U : Set ℂ} {A B : ℂ} (hAB : Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U) : ∃ (A' : ℂ), A' ≠ 0 ∧ ∃ (B' : ℂ), Set.BijOn (fun (ζ : ℂ) => A' * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-∑ i : ι, e i - 2) e) ζ + B') (Metric.ball 0 1) U ∧ (∀ (x : ℝ) (v : ℂ), Filter.Tendsto (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds v) → Filter.Tendsto (fun (ζ : ℂ) => A' * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-∑ i : ι, e i - 2) e) ζ + B') (nhdsWithin (↑(boundaryCayley x)) (Metric.ball 0 1)) (nhds v)) ∧ (Filter.Tendsto (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (Bornology.cobounded ℂ) → Filter.Tendsto (fun (ζ : ℂ) => A' * schwarzChristoffelDiscPrimitive (Option.elim' 1 fun (i : ι) => boundaryCayley (a i)) (Option.elim' (-∑ i : ι, e i - 2) e) ζ + B') (nhdsWithin 1 (Metric.ball 0 1)) (Bornology.cobounded ℂ))

Disc transport including the point at infinity. A half-plane Schwarz--Christoffel bijection gives a disc Schwarz--Christoffel bijection after adding the prevertex 1 with exponent -∑ i, e i - 2. Finite boundary limits pass to their Cayley prevertices, and divergence at infinity passes to divergence at 1.