The Schwarz--Christoffel integrand at a prevertex

Near a real prevertex p, all factors of the Schwarz--Christoffel integrand based away from p tend to nonzero limits. The factors based at p combine into the single power (z - p) ^ t, where t is the sum of their exponents. This file identifies the remaining nonzero coefficient and proves the corresponding normalized limit from the upper half-plane.

The coefficient includes the unimodular phase of the boundary edge immediately to the right of p. Its remaining factor is a positive real product of the distances from p to the other prevertices. Consequently the coefficient never vanishes. This is the local analytic input for integrating the leading term and obtaining the power-law corner asymptotic of the Schwarz--Christoffel primitive.

Main definitions

• TauCeti.schwarzChristoffelPrevertexCoefficient -- the nonzero coefficient of the leading power of the integrand at a real point.

Main results

• TauCeti.schwarzChristoffelPrevertexCoefficient_ne_zero -- the coefficient is nonzero.
• TauCeti.norm_schwarzChristoffelPrevertexCoefficient -- its norm is the positive product of distances to the other prevertices.
• TauCeti.tendsto_schwarzChristoffelIntegrand_div_cpow -- after division by the total power at a prevertex, the integrand tends to its leading coefficient.

References

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

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

The leading coefficient of the Schwarz--Christoffel integrand at a real point p.

The exponential records the direction of the boundary edge immediately to the right of p. The positive real product is the contribution at p of every factor based at a different prevertex. If p is not itself a prevertex, this is simply the boundary value of the integrand there.

Equations

• TauCeti.schwarzChristoffelPrevertexCoefficient a e p = Complex.exp (↑(TauCeti.schwarzChristoffelEdgeAngle a e p) * Complex.I) * ↑(∏ i : ι with a i ≠ p, |p - a i| ^ e i)

theorem TauCeti.schwarzChristoffelPrevertexCoefficient_def {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (p : ℝ) : schwarzChristoffelPrevertexCoefficient a e p = Complex.exp (↑(schwarzChristoffelEdgeAngle a e p) * Complex.I) * ↑(∏ i : ι with a i ≠ p, |p - a i| ^ e i)

The leading coefficient is its boundary direction times the positive product of distances to the other prevertices.

@[simp]

theorem TauCeti.norm_schwarzChristoffelPrevertexCoefficient {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (p : ℝ) : ‖schwarzChristoffelPrevertexCoefficient a e p‖ = ∏ i : ι with a i ≠ p, |p - a i| ^ e i

The norm of the leading coefficient is the positive real product of the powered distances from p to the other prevertices.

@[simp]

theorem TauCeti.schwarzChristoffelPrevertexCoefficient_ne_zero {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (p : ℝ) : schwarzChristoffelPrevertexCoefficient a e p ≠ 0

The leading coefficient of the Schwarz--Christoffel integrand at a real point is nonzero.

theorem TauCeti.tendsto_schwarzChristoffelIntegrand_div_cpow {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (p : ℝ) : Filter.Tendsto (fun (z : ℂ) => schwarzChristoffelIntegrand a e z / (z - ↑p) ^ ↑(∑ i : ι with a i = p, e i)) (nhdsWithin (↑p) UpperHalfPlane.upperHalfPlaneSet) (nhds (schwarzChristoffelPrevertexCoefficient a e p))

Leading asymptotic of the Schwarz--Christoffel integrand at a prevertex. Dividing the integrand by (z - p) raised to the total exponent carried by p leaves a function tending to the nonzero prevertex coefficient as z approaches p from the upper half-plane. Coincident prevertices are handled by summing all of their exponents.