Straight boundary arcs of the Schwarz--Christoffel map

The Schwarz--Christoffel map is the primitive on the upper half-plane of the product ∏ i, (z - a i) ^ (e i) of principal powers with real prevertices a i. This file proves a boundary step toward identifying its image as a polygon: on a real interval containing no prevertex, the map extends continuously and its boundary values run along a straight line, in the direction exp (i π ∑_{a i > x} e i). Only prevertices with nonzero exponent have to be avoided, since a factor with zero exponent is the constant 1.

The obstacle is that the principal power is cut along the negative reals, so the integrand itself is discontinuous across the part of the real axis to the left of a prevertex. It is only the branch that is wrong: replacing the factor (z - a i) ^ (e i) by (a i - z) ^ (e i) for every prevertex lying to the right of a reference point c produces schwarzChristoffelContinuedIntegrand, which differs from the integrand on the upper half-plane by the unimodular constant exp (i · schwarzChristoffelEdgeAngle a e c) and, when c is taken to be the left endpoint of a prevertex-free interval, is holomorphic on the whole vertical strip that interval cuts out. On the interval itself it is real and positive, since every factor is then a positive real raised to a real power.

Integrating the continued integrand over the disc whose diameter is the interval — a disc which lies in the strip, so Morera's theorem for a disc supplies a primitive there — gives a holomorphic function agreeing with the Schwarz--Christoffel primitive up to an additive constant on the upper half of the disc. Its restriction to the interval is therefore the continuous boundary extension, and the fundamental theorem of calculus writes an increment of it as a real multiple of the direction constant. That is the straight boundary arc.

The turning of the direction at a prevertex is schwarzChristoffelEdgeAngle_sub: passing a prevertex a i rotates the edge direction by -π · e i, which for the classical choice e i = α i / π - 1 is the exterior angle π - α i of a polygon with interior angle α i.

Main definitions

• TauCeti.schwarzChristoffelDensity -- the nonnegative real density obtained by taking the norm of the Schwarz--Christoffel integrand on the boundary; it is positive away from prevertices carrying nonzero exponent.
• TauCeti.schwarzChristoffelContinuedIntegrand -- the Schwarz--Christoffel integrand with the branch of every factor to the right of a reference point reflected, so that, as long as no prevertex equals that point, it continues holomorphically across the real axis near it.
• TauCeti.schwarzChristoffelEdgeAngle -- the argument π ∑_{a i > c} e i of the resulting edge direction.

Main results

• TauCeti.schwarzChristoffelEdgeAngle_sub_eq_pi_mul_exponent_sum_of_adjacent -- across adjacent reference points p < q, the edge angle at p minus the edge angle at q is π times the total exponent carried by q; moving from left to right therefore changes the edge angle by -π times that total.
• TauCeti.schwarzChristoffelIntegrand_eq_exp_mul_continued -- on the upper half-plane the integrand is the continued integrand times the unimodular edge-direction constant.
• TauCeti.schwarzChristoffelContinuedIntegrand_ofReal -- on a prevertex-free real interval the continued integrand is the positive real ∏ i, |x - a i| ^ e i.
• TauCeti.tendsto_schwarzChristoffelIntegrand_nhdsWithin -- the boundary value of the integrand at a point of such an interval, whose argument is the edge angle.
• TauCeti.exists_tendsto_schwarzChristoffelPrimitive_sub_eq -- the Schwarz--Christoffel map extends continuously to a prevertex-free real interval, and an increment of the extension is a real multiple of the edge direction.
• TauCeti.exists_hasDerivAt_schwarzChristoffelPrimitive_continuation -- on a disc around a regular edge interval, the primitive has a holomorphic continuation with explicit derivative.
• TauCeti.exists_tendsto_schwarzChristoffelPrimitive_injOn_collinear -- consequently the interval is carried injectively onto a collinear set: the boundary arc runs along a straight line.

References

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

noncomputable def TauCeti.schwarzChristoffelDensity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (x : ℝ) : ℝ

The real Schwarz--Christoffel density on the boundary.

Equations

• TauCeti.schwarzChristoffelDensity a e x = ∏ k : ι, |x - a k| ^ e k

theorem TauCeti.schwarzChristoffelDensity_def {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (x : ℝ) : schwarzChristoffelDensity a e x = ∏ k : ι, |x - a k| ^ e k

The Schwarz--Christoffel density is its defining product.

theorem TauCeti.schwarzChristoffelDensity_nonneg {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (x : ℝ) : 0 ≤ schwarzChristoffelDensity a e x

The Schwarz--Christoffel boundary density is nonnegative.

theorem TauCeti.schwarzChristoffelDensity_neg {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (x : ℝ) : schwarzChristoffelDensity (fun (i : ι) => -a i) e x = schwarzChristoffelDensity a e (-x)

Reflecting the prevertices and the boundary parameter preserves the Schwarz--Christoffel density.

theorem TauCeti.schwarzChristoffelDensity_pos {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {x : ℝ} (hx : ∀ (k : ι), e k ≠ 0 → x ≠ a k) : 0 < schwarzChristoffelDensity a e x

The Schwarz--Christoffel boundary density is positive away from every prevertex carrying a nonzero exponent.

theorem TauCeti.continuousOn_schwarzChristoffelDensity {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q : ℝ} (ha : ∀ (k : ι), e k ≠ 0 → a k ∉ Set.Ioo p q) : ContinuousOn (schwarzChristoffelDensity a e) (Set.Ioo p q)

The Schwarz--Christoffel boundary density is continuous on an interval containing no prevertex with nonzero exponent.

@[simp]

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

Zero turning exponents give constant boundary density one.

theorem TauCeti.schwarzChristoffelDensity_eq_norm_integrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (x : ℝ) : schwarzChristoffelDensity a e x = ‖schwarzChristoffelIntegrand a e ↑x‖

The boundary density is the norm of the Schwarz--Christoffel integrand at a real point.

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

The Schwarz--Christoffel integrand continued across a reference point c.

Each factor (z - a i) ^ (e i) of schwarzChristoffelIntegrand whose prevertex a i lies to the right of c is replaced by (a i - z) ^ (e i), moving its branch cut from the real half-line to the left of a i to the one to the right. Provided no prevertex equals c, all the cuts then avoid a neighbourhood of c in the real axis, so the product continues holomorphically across it (differentiableAt_schwarzChristoffelContinuedIntegrand), while on the upper half-plane it still agrees with the integrand up to the unimodular constant of schwarzChristoffelIntegrand_eq_exp_mul_continued.

Equations

• TauCeti.schwarzChristoffelContinuedIntegrand a e c z = ∏ i : ι, (if a i ≤ c then z - ↑(a i) else ↑(a i) - z) ^ ↑(e i)

theorem TauCeti.schwarzChristoffelContinuedIntegrand_def {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (c : ℝ) (z : ℂ) : schwarzChristoffelContinuedIntegrand a e c z = ∏ i : ι, (if a i ≤ c then z - ↑(a i) else ↑(a i) - z) ^ ↑(e i)

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

noncomputable def TauCeti.schwarzChristoffelEdgeAngle {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (c : ℝ) : ℝ

The Schwarz--Christoffel edge angle at a reference point c: the argument π ∑_{a i > c} e i of the direction in which the map runs along the image of the boundary interval containing c.

Equations

• TauCeti.schwarzChristoffelEdgeAngle a e c = Real.pi * ∑ i : ι, if c < a i then e i else 0

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_sum_filter {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (c : ℝ) : schwarzChristoffelEdgeAngle a e c = Real.pi * ∑ i : ι with c < a i, e i

The Schwarz--Christoffel edge angle as a sum over the prevertices to the right of the reference point.

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_zero_of_forall_le {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c : ℝ} (hc : ∀ (i : ι), a i ≤ c) : schwarzChristoffelEdgeAngle a e c = 0

The Schwarz--Christoffel edge angle is zero to the right of every prevertex.

theorem TauCeti.schwarzChristoffelEdgeAngle_eq_pi_mul_sum_of_forall_lt {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c : ℝ} (hc : ∀ (i : ι), c < a i) : schwarzChristoffelEdgeAngle a e c = Real.pi * ∑ i : ι, e i

To the left of every prevertex, the Schwarz--Christoffel edge angle is π times the total exponent.

theorem TauCeti.schwarzChristoffelEdgeAngle_sub {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c d : ℝ} (hcd : c ≤ d) : schwarzChristoffelEdgeAngle a e c - schwarzChristoffelEdgeAngle a e d = Real.pi * ∑ i : ι with a i ∈ Set.Ioc c d, e i

The edge angle drops, as the reference point moves to the right past a set of prevertices, by π times the total of their exponents. For the classical choice e i = α i / π - 1 attached to a polygon with interior angle α i, passing a single prevertex therefore turns the edge direction by -π * e i = π - α i, the exterior angle at that vertex.

theorem TauCeti.schwarzChristoffelEdgeAngle_sub_eq_pi_mul_exponent_sum_of_adjacent {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q : ℝ} (hpq : p < q) (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : schwarzChristoffelEdgeAngle a e p - schwarzChristoffelEdgeAngle a e q = Real.pi * ∑ i : ι with a i = q, e i

Across two adjacent real reference points p < q -- that is, with no prevertex of nonzero exponent strictly between them -- the Schwarz--Christoffel edge angle at p minus the edge angle at q is exactly π times the total exponent carried by q; equivalently, moving from left to right changes the edge angle by -π times that total. For the classical choice e i = α i / π - 1, every index i with a i = q contributes the exterior angle π - α i to that left-to-right change, which is therefore the sum of those contributions and equals a single exterior angle exactly when one index sits at q.

theorem TauCeti.schwarzChristoffelIntegrand_eq_exp_mul_continued {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (c : ℝ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : schwarzChristoffelIntegrand a e z = Complex.exp (↑(schwarzChristoffelEdgeAngle a e c) * Complex.I) * schwarzChristoffelContinuedIntegrand a e c z

On the upper half-plane the Schwarz--Christoffel integrand is its continuation across any real reference point, times the unimodular constant with argument the edge angle there.

theorem TauCeti.differentiableAt_schwarzChristoffelContinuedIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c : ℝ} {z : ℂ} (hz : ∀ (i : ι), e i ≠ 0 → (if a i ≤ c then z - ↑(a i) else ↑(a i) - z) ∈ Complex.slitPlane) : DifferentiableAt ℂ (schwarzChristoffelContinuedIntegrand a e c) z

The continued Schwarz--Christoffel integrand is holomorphic at any point where each reflected principal-power factor with nonzero exponent lies in Complex.slitPlane. A factor with zero exponent is the constant 1, so it is unrestricted.

theorem TauCeti.differentiableOn_schwarzChristoffelContinuedIntegrand {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : DifferentiableOn ℂ (schwarzChristoffelContinuedIntegrand a e p) {z : ℂ | z.re ∈ Set.Ioo p q}

The Schwarz--Christoffel integrand continued across the left endpoint of an interval free of prevertices with nonzero exponent is holomorphic on the whole vertical strip over that interval.

theorem TauCeti.schwarzChristoffelContinuedIntegrand_ofReal {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {c x : ℝ} (hlo : ∀ (i : ι), e i ≠ 0 → a i ≤ c → a i < x) (hhi : ∀ (i : ι), e i ≠ 0 → c < a i → x < a i) : schwarzChristoffelContinuedIntegrand a e c ↑x = ↑(schwarzChristoffelDensity a e x)

At a real point separated in the expected direction from every prevertex with nonzero exponent, the continued Schwarz--Christoffel integrand takes the positive real value ∏ i, |x - a i| ^ e i: every such factor is a positive real raised to a real power, and a factor with zero exponent is 1 on both sides.

theorem TauCeti.tendsto_schwarzChristoffelIntegrand_nhdsWithin {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q) : Filter.Tendsto (schwarzChristoffelIntegrand a e) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds (Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I) * ↑(schwarzChristoffelDensity a e x)))

The boundary value of the Schwarz--Christoffel integrand at a point of a real interval free of prevertices with nonzero exponent: approaching from the upper half-plane, the integrand tends to the positive real ∏ i, |x - a i| ^ e i rotated by the edge angle. In particular its argument is constant along the interval.

theorem TauCeti.exists_hasDerivAt_schwarzChristoffelPrimitive_continuation {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : ∃ (G : ℂ → ℂ), (∀ z ∈ Metric.ball (↑((p + q) / 2)) ((q - p) / 2), HasDerivAt G (Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I) * schwarzChristoffelContinuedIntegrand a e p z) z) ∧ Set.EqOn G (schwarzChristoffelPrimitive a e z₀) (Metric.ball (↑((p + q) / 2)) ((q - p) / 2) ∩ UpperHalfPlane.upperHalfPlaneSet)

On a disc with prevertex-free real diameter, the Schwarz--Christoffel primitive has a holomorphic continuation whose derivative is the continued integrand times the edge direction. This is the analytic continuation underlying both the boundary increment formula and local injectivity at a regular edge point.

theorem TauCeti.exists_tendsto_schwarzChristoffelPrimitive_sub_eq {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : ∃ (L : ℝ → ℂ), (∀ x ∈ Set.Ioo p q, Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds (L x))) ∧ ContinuousOn L (Set.Ioo p q) ∧ ∀ x ∈ Set.Ioo p q, ∀ y ∈ Set.Ioo p q, L x - L y = ↑(∫ (t : ℝ) in y..x, schwarzChristoffelDensity a e t) * Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I)

The Schwarz--Christoffel map has straight image edges. Let every prevertex a i with nonzero exponent avoid the real interval Ioo p q; a prevertex with zero exponent contributes the constant factor 1 and is harmless. Then the Schwarz--Christoffel primitive extends continuously from the upper half-plane to that interval, and any increment of the extension along it is a real multiple of the unimodular direction with argument schwarzChristoffelEdgeAngle a e p. The image of the interval is therefore contained in a line with that direction; see exists_tendsto_schwarzChristoffelPrimitive_injOn_collinear.

theorem TauCeti.exists_tendsto_schwarzChristoffelPrimitive_injOn_collinear {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {p q : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) : ∃ (L : ℝ → ℂ), (∀ x ∈ Set.Ioo p q, Filter.Tendsto (schwarzChristoffelPrimitive a e z₀) (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds (L x))) ∧ ContinuousOn L (Set.Ioo p q) ∧ Set.InjOn L (Set.Ioo p q) ∧ Collinear ℝ (L '' Set.Ioo p q)

The Schwarz--Christoffel map carries a boundary interval free of prevertices with nonzero exponent injectively into a line. The boundary values of the map along such an interval are collinear, and distinct points of the interval have distinct boundary values, so the interval is carried injectively onto a subset of a line — a candidate edge for a later polygon identification.