The Schwarz--Christoffel primitive

The Schwarz--Christoffel map is obtained by integrating the product of complex powers attached to its real prevertices. This file constructs the globally defined primitive on the upper half-plane, normalized to vanish at an arbitrary base point there.

For prevertices a, turning exponents e, and a base point z₀, schwarzChristoffelPrimitive a e z₀ z is the integral of schwarzChristoffelIntegrand a e along the horizontal-then-vertical polygonal path from z₀ to z. Holomorphy of the integrand and convexity of the upper half-plane make these wedge integrals additive. The primitive has the prescribed derivative everywhere in the upper half-plane and is conformal there because that derivative never vanishes. Its normalization characterizes it uniquely among all primitives of the same integrand.

These properties provide the analytic map used in the Schwarz--Christoffel formula. Identifying its boundary values, its straight image edges, and its image as the intended polygon requires separate boundary analysis.

Main definitions

• TauCeti.schwarzChristoffelPrimitive -- the primitive normalized to vanish at a chosen point of the upper half-plane.

Main results

• TauCeti.hasDerivAt_schwarzChristoffelPrimitive -- its derivative is the Schwarz--Christoffel integrand.
• TauCeti.schwarzChristoffelPrimitive_change_base -- changing the normalization point subtracts the value at the new base point.
• TauCeti.conformalAt_schwarzChristoffelPrimitive -- it is conformal throughout the upper half-plane.
• TauCeti.logDeriv_deriv_schwarzChristoffelPrimitive -- its pre-Schwarzian derivative is the sum of the simple fractions e i / (z - a i).
• TauCeti.eqOn_schwarzChristoffelPrimitive -- the derivative and normalization uniquely characterize it on the upper half-plane.
• TauCeti.norm_schwarzChristoffelPrimitive_sub_le_integral -- along an affine segment of the upper half-plane it moves by at most the integral of any integrable bound on its speed.

References

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

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

The normalized Schwarz--Christoffel primitive associated to real prevertices a and turning exponents e. It is the integral of schwarzChristoffelIntegrand a e from the chosen upper-half-plane base point z₀ to z, along a horizontal segment followed by a vertical one.

The definition is total on ℂ, but its analytic interpretation is asserted on upperHalfPlaneSet.

Equations

• TauCeti.schwarzChristoffelPrimitive a e z₀ z = (↑z₀).wedgeIntegral z (TauCeti.schwarzChristoffelIntegrand a e)

@[simp]

theorem TauCeti.schwarzChristoffelPrimitive_apply_base {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : schwarzChristoffelPrimitive a e z₀ ↑z₀ = 0

The normalized Schwarz--Christoffel primitive vanishes at its base point.

theorem TauCeti.hasDerivAt_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : HasDerivAt (schwarzChristoffelPrimitive a e z₀) (schwarzChristoffelIntegrand a e z) z

The derivative of the normalized Schwarz--Christoffel primitive is its integrand throughout the upper half-plane.

theorem TauCeti.schwarzChristoffelPrimitive_change_base {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (b c : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelPrimitive a e b z = schwarzChristoffelPrimitive a e c z - schwarzChristoffelPrimitive a e c ↑b

Changing the base point of a normalized Schwarz--Christoffel primitive subtracts its value at the new base point.

theorem TauCeti.deriv_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : deriv (schwarzChristoffelPrimitive a e z₀) z = schwarzChristoffelIntegrand a e z

The derivative of the normalized Schwarz--Christoffel primitive on the upper half-plane.

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

The pre-Schwarzian derivative of the Schwarz--Christoffel map. Throughout the upper half-plane the quotient F'' / F' of the normalized primitive F is the sum of simple fractions ∑ i, e i / (z - a i). This is the Schwarz--Christoffel differential equation, the identity a conformal map of the upper half-plane onto a polygon has to satisfy for a its prevertices and e its turning exponents.

theorem TauCeti.differentiableOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : DifferentiableOn ℂ (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet

The normalized Schwarz--Christoffel primitive is holomorphic on the upper half-plane.

theorem TauCeti.conformalAt_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : ConformalAt (schwarzChristoffelPrimitive a e z₀) z

The normalized Schwarz--Christoffel primitive is conformal at every point of the upper half-plane.

theorem TauCeti.eqOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {g : ℂ → ℂ} (hg : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, HasDerivAt g (schwarzChristoffelIntegrand a e z) z) (hg₀ : g ↑z₀ = 0) : Set.EqOn g (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet

A primitive of the Schwarz--Christoffel integrand that vanishes at the chosen base point agrees with schwarzChristoffelPrimitive throughout the upper half-plane.

theorem TauCeti.norm_schwarzChristoffelPrimitive_sub_le_integral {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {α β : ℝ} (hab : α ≤ β) {c v : ℂ} {B : ℝ → ℝ} (hmem : ∀ s ∈ Set.Icc α β, c + ↑s * v ∈ UpperHalfPlane.upperHalfPlaneSet) (hB : ∀ s ∈ Set.Icc α β, ‖v‖ * ‖schwarzChristoffelIntegrand a e (c + ↑s * v)‖ ≤ B s) (hBi : IntervalIntegrable B MeasureTheory.volume α β) : ‖schwarzChristoffelPrimitive a e z₀ (c + ↑β * v) - schwarzChristoffelPrimitive a e z₀ (c + ↑α * v)‖ ≤ ∫ (s : ℝ) in α..β, B s

Displacement of the normalized Schwarz--Christoffel primitive along an affine segment. If the segment s ↦ c + s * v, s ∈ [α, β], stays in the upper half-plane and the speed ‖v‖ * ‖schwarzChristoffelIntegrand a e (c + s * v)‖ is bounded along it by an integrable function B, then the primitive moves by at most ∫ s in α..β, B s.