Automatic mass of the boundary double-layer density

For an oriented smooth convex Jordan boundary, the double-layer density

rho_xi(t) = Im (gamma'(t) / (gamma(t) - xi)) / pi

has mass one at every frontier point. The proof chooses a parameter s for xi, divides the boundary chord by gamma'(s), and rotates it by -I. Convex support puts this normalized chord in Complex.slitPlane. Its principal argument therefore lifts continuously from 0 to pi during one period, and its derivative is exactly pi * rho_xi. Positivity makes the lift monotone, which supplies derivative integrability; the improper fundamental theorem then gives the mass identity.

Main declarations

• crouzeixBoundaryDoubleLayerDensity_periodic -- the density is periodic;
• canonicalNormal_support_all_of_Ioc -- oriented support on one fundamental interval propagates to every parameter;
• integral_crouzeixBoundaryDoubleLayerDensity_eq_one_of_oriented_carrier_point -- one consistently oriented carrier point forces unit mass at every frontier basepoint;
• crouzeixBoundaryPhaseContractive_of_oriented_carrier_point -- the same geometry gives sharp boundary-phase contractivity for every polynomial.

theorem crouzeixBoundaryDoubleLayerDensity_periodic (Omega : SmoothJordanDomain) (xi : ℂ) : Function.Periodic (crouzeixBoundaryDoubleLayerDensity Omega xi) (2 * Real.pi)

The explicit boundary double-layer density has the same period as the boundary trace.

theorem canonicalNormal_support_all_of_Ioc (Omega : SmoothJordanDomain) (c : ℂ) (hsupport : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (t : ℝ) : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0

An oriented support inequality verified on the standard half-open fundamental interval holds at every real parameter.

theorem integral_crouzeixBoundaryDoubleLayerDensity_eq_one_of_oriented_carrier_point (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (xi : ℂ) (hxi : xi ∈ frontier Omega.carrier) : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1

If one point of the open carrier lies consistently on the inward side of the canonical oriented tangent line, then the boundary double-layer density based at every frontier point has interval-integral mass one.

theorem crouzeixBoundaryPhaseContractive_of_oriented_carrier_point (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (p : Polynomial ℂ) : CrouzeixBoundaryPhaseContractive Omega p

A consistently oriented point of the carrier makes every polynomial boundary phase contractive.