The Schwarz--Christoffel integrand

The derivative in the Schwarz--Christoffel formula is, up to a nonzero constant, a finite product

∏ i, (z - a i) ^ e i,

where the prevertices a i lie on the real axis and e i is the normalized turning exponent at the corresponding polygon vertex. For an interior angle α i, measured in radians, the usual choice is e i = α i / π - 1.

This file defines that product using the principal complex power and establishes its analytic properties on the upper half-plane. Each difference z - a i lies in Complex.slitPlane there, so the chosen branch is holomorphic. The integrand is nowhere zero, its norm is the product of the expected real powers, and its logarithmic derivative is the sum of the simple fractions e i / (z - a i).

These facts are the analytic input for constructing the Schwarz--Christoffel map as a primitive of the integrand. Nonvanishing will make that primitive locally conformal, while the real-power norm formula provides estimates away from the prevertices. Since complex powers are totalized at zero, values of this definition at prevertices do not describe its boundary singularities; those must instead be stated using punctured limits.

Main definitions

• TauCeti.schwarzChristoffelIntegrand -- the finite product of the principal power factors.

Main results

• TauCeti.differentiableOn_schwarzChristoffelIntegrand -- the integrand is holomorphic on the upper half-plane.
• TauCeti.schwarzChristoffelIntegrand_ne_zero -- it has no zero there.
• TauCeti.norm_schwarzChristoffelIntegrand -- its norm is the product of real powers of the distances to the prevertices.
• TauCeti.logDeriv_schwarzChristoffelIntegrand -- its logarithmic derivative is the expected sum of simple fractions.

References

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

noncomputable def TauCeti.schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z : ℂ) : ℂ

The Schwarz--Christoffel integrand associated to real prevertices a i and real exponents e i.

For a polygon with interior angle α i at the vertex corresponding to a i, the classical choice is e i = α i / π - 1. The definition itself does not impose the polygonal angle conditions: its analytic properties hold for every finite family of real exponents. At a prevertex, Mathlib's totalized zero-base power determines the value, which should not be interpreted as analytic boundary data.

Equations

• TauCeti.schwarzChristoffelIntegrand a e z = ∏ i : ι, (z - ↑(a i)) ^ ↑(e i)

theorem TauCeti.schwarzChristoffelIntegrand_def {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z : ℂ) : schwarzChristoffelIntegrand a e z = ∏ i : ι, (z - ↑(a i)) ^ ↑(e i)

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

@[simp]

theorem TauCeti.schwarzChristoffelIntegrand_zero {ι : Type u_1} [Fintype ι] (a : ι → ℝ) : schwarzChristoffelIntegrand a 0 = 1

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

theorem TauCeti.differentiableOn_schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) : DifferentiableOn ℂ (schwarzChristoffelIntegrand a e) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel integrand is holomorphic on the open upper half-plane.

theorem TauCeti.schwarzChristoffelIntegrand_ne_zero {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelIntegrand a e z ≠ 0

The Schwarz--Christoffel integrand is nowhere zero in the upper half-plane. Consequently, any primitive of it is locally conformal there.

theorem TauCeti.schwarzChristoffelIntegrand_add {ι : Type u_1} [Fintype ι] (a e d : ι → ℝ) {z : ℂ} (hz : ∀ (i : ι), z ≠ ↑(a i)) : schwarzChristoffelIntegrand a (e + d) z = schwarzChristoffelIntegrand a e z * schwarzChristoffelIntegrand a d z

Adding two exponent families multiplies their Schwarz--Christoffel integrands at any point off the prevertices. The hypothesis is essential because the principal complex power is additive in its exponent only away from a zero base.

theorem TauCeti.norm_schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z : ℂ) : ‖schwarzChristoffelIntegrand a e z‖ = ∏ i : ι, dist z ↑(a i) ^ e i

The norm of a Schwarz--Christoffel integrand is the product of the corresponding real powers of the distances to its prevertices. Both sides are totalized in the same way at a prevertex, so no hypothesis on z is needed; the common value there is not analytic boundary data, which has to be described by a punctured limit instead.

theorem TauCeti.logDeriv_schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : logDeriv (schwarzChristoffelIntegrand a e) z = ∑ i : ι, ↑(e i) / (z - ↑(a i))

The logarithmic derivative of the Schwarz--Christoffel integrand is the sum of its simple fractions. Its possible poles are the real prevertices and hence lie on the boundary of the domain of holomorphy.

theorem TauCeti.hasDerivAt_schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : HasDerivAt (schwarzChristoffelIntegrand a e) (schwarzChristoffelIntegrand a e z * ∑ i : ι, ↑(e i) / (z - ↑(a i))) z

The derivative of the Schwarz--Christoffel integrand, written as the integrand times its logarithmic derivative.

theorem TauCeti.deriv_schwarzChristoffelIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : deriv (schwarzChristoffelIntegrand a e) z = schwarzChristoffelIntegrand a e z * ∑ i : ι, ↑(e i) / (z - ↑(a i))

The derivative of the Schwarz--Christoffel integrand in the upper half-plane.