The boundary double-layer probability density

For a boundary point xi and a smooth parametrization gamma, the scalar double-layer density is

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

The Crouzeix--Palencia boundary companion is integration of the conjugate polynomial datum against this density. The key cancellation is exact: the second half of the double-layer kernel is the conjugate of the contour of a polynomial divided difference, hence integrates to zero on the closed curve.

Consequently, integrability, nonnegativity, and unit mass of this explicit density imply the sharp boundary-phase contraction. This file isolates those two geometric facts rather than assuming the contraction itself.

Main declarations

• crouzeixBoundaryDoubleLayerDensity -- the explicit real density;
• contourIntegral_polynomial_eval_eq_zero -- polynomial contours vanish on every smooth closed boundary;
• crouzeixPolynomialScalarCompanionBoundaryValue_eq_integral_boundaryDoubleLayerDensity -- the exact probability-integral representation;
• crouzeixBoundaryPhaseContractive_of_boundaryDoubleLayerDensity -- sharp phase contractivity from nonnegativity and unit mass;
• crouzeixBoundaryPhaseContractive_of_boundaryDoubleLayerDensity_mass_support -- the sharp invariant from unit mass and oriented support alone.

noncomputable def crouzeixBoundaryDoubleLayerDensity (Omega : SmoothJordanDomain) (xi : ℂ) (t : ℝ) : ℝ

The real scalar double-layer density based at xi. At the (measure-zero) parameter values where the boundary trace equals xi, Mathlib's inverse at zero makes this definition zero.

Equations

• crouzeixBoundaryDoubleLayerDensity Omega xi t = (deriv Omega.boundaryParam t * (Omega.boundaryParam t - xi)⁻¹).im / Real.pi

theorem intervalIntegrable_crouzeixBoundaryDoubleLayerDensity_of_integral_eq_one (Omega : SmoothJordanDomain) (xi : ℂ) (hmass : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) : IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)

Unit interval-integral mass forces integrability. This uses the Bochner integral convention that a nonintegrable function has integral zero, so the nonzero mass hypothesis already contains the required integrability datum.

theorem crouzeixBoundaryDoubleLayerDensity_nonneg_of_support (Omega : SmoothJordanDomain) (xi : ℂ) (t : ℝ) (hsupport : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (xi - Omega.boundaryParam t)).re ≤ 0) : 0 ≤ crouzeixBoundaryDoubleLayerDensity Omega xi t

An oriented supporting-normal inequality at the boundary trace makes the scalar double-layer density nonnegative. This records the exact orientation data absent from the bare SmoothJordanDomain structure.

theorem ofReal_crouzeixBoundaryDoubleLayerDensity (Omega : SmoothJordanDomain) (xi : ℂ) (t : ℝ) : ↑(crouzeixBoundaryDoubleLayerDensity Omega xi t) = (2 * ↑Real.pi * Complex.I)⁻¹ * (deriv Omega.boundaryParam t * (Omega.boundaryParam t - xi)⁻¹ - star (deriv Omega.boundaryParam t * (Omega.boundaryParam t - xi)⁻¹))

The real density is the difference of the two conjugate Cauchy kernels with the standard 1 / (2 pi i) normalization.

theorem contourIntegral_polynomial_eval_eq_zero (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : contourIntegral (fun (z : ℂ) => Polynomial.eval z p) Omega.boundaryParam = 0

The contour integral of a complex polynomial vanishes on every smooth closed boundary.

theorem crouzeixPolynomialScalarCompanionBoundaryValue_eq_integral_boundaryDoubleLayerDensity (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ frontier Omega.carrier) (hrho : IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)) (hmass : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) : crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi = ∫ (t : ℝ) in 0..2 * Real.pi, ↑(crouzeixBoundaryDoubleLayerDensity Omega xi t) * star (Polynomial.eval (Omega.boundaryParam t) p)

The Plemelj boundary value is the conjugate polynomial boundary datum integrated against the scalar double-layer density, provided that density is integrable and has unit mass. The analytic half of the kernel cancels as a closed polynomial contour.

theorem norm_crouzeixPolynomialScalarCompanionBoundaryValue_le_of_boundaryDoubleLayerDensity (Omega : SmoothJordanDomain) (p : Polynomial ℂ) {xi : ℂ} (hxi : xi ∈ frontier Omega.carrier) (hrho : IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)) (hmass : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) (hpos : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), 0 ≤ crouzeixBoundaryDoubleLayerDensity Omega xi t) : ‖crouzeixPolynomialScalarCompanionBoundaryValue Omega p xi‖ ≤ polynomialSupNorm p (frontier Omega.carrier)

Integration of conjugate polynomial boundary data against a nonnegative unit-mass double-layer density is contractive for the frontier sup norm.

theorem crouzeixBoundaryPhaseContractive_of_boundaryDoubleLayerDensity (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hrho : ∀ xi ∈ frontier Omega.carrier, IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)) (hmass : ∀ xi ∈ frontier Omega.carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) (hpos : ∀ xi ∈ frontier Omega.carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), 0 ≤ crouzeixBoundaryDoubleLayerDensity Omega xi t) : CrouzeixBoundaryPhaseContractive Omega p

Nonnegativity and unit mass of the explicit boundary double-layer density imply the sharp boundary-phase invariant.

theorem crouzeixBoundaryPhaseContractive_of_boundaryDoubleLayerDensity_support (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hrho : ∀ xi ∈ frontier Omega.carrier, IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)) (hmass : ∀ xi ∈ frontier Omega.carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) (hsupport : ∀ xi ∈ frontier Omega.carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (xi - Omega.boundaryParam t)).re ≤ 0) : CrouzeixBoundaryPhaseContractive Omega p

The sharp boundary-phase invariant follows directly from integrability, unit mass, and the oriented supporting-normal inequality on the frontier. The pointwise density sign is discharged algebraically.

theorem crouzeixBoundaryPhaseContractive_of_boundaryDoubleLayerDensity_mass_support (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hmass : ∀ xi ∈ frontier Omega.carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) (hsupport : ∀ xi ∈ frontier Omega.carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (xi - Omega.boundaryParam t)).re ≤ 0) : CrouzeixBoundaryPhaseContractive Omega p

Unit mass and oriented frontier support alone imply the sharp boundary-phase invariant. A separate integrability assumption is redundant: mass one rules out the nonintegrable zero-integral convention.