L4.2 assembly from the boundary double-layer probability measure

The scalar-companion boundary value is contractive once its explicit double-layer density is an oriented probability density. This file feeds that concrete geometric interface into the strongest radial assembly: phase contractivity is automatic, approximation is needed only for positive-degree polynomials vanishing at zero, and auxiliary-contour reproduction only after frontier-sup normalization.

Main declaration

• crouzeixPalencia_of_thickening_cauchy_support_doubleLayerDensity_radialZero -- the radial Crouzeix--Palencia capstone with the opaque phase hypothesis replaced by integrability, unit mass, and oriented frontier support of the explicit scalar double-layer density.
• crouzeixPalencia_of_thickening_cauchy_support_doubleLayerMass_radialZero -- the strongest form, where the existing numerical-range support fixes the boundary orientation and unit density mass is the only remaining phase geometry.
• crouzeixPalencia_of_thickening_cauchy_support_doubleLayer_radialZero -- oriented convexity also forces unit mass, leaving no separate boundary probability-measure premise.
• crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_radialZero -- a single resolvent-mass identity also supplies the all-polynomial Cauchy representation used by the strongest capstone.
• crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_basepointWinding_radialZero -- winding normalization at one carrier point per stage propagates across the whole strictly convex carrier.
• crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_automaticWinding_radialZero -- oriented numerical-range support also supplies that basepoint normalization, so no separate winding premise remains.

theorem crouzeixPalencia_of_thickening_cauchy_support_doubleLayerDensity_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hrho : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity (Omega n) xi) MeasureTheory.volume 0 (2 * Real.pi)) (hmass : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity (Omega n) xi t = 1) (hboundarySupport : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (xi - (Omega n).boundaryParam t)).re ≤ 0) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The strongest radial scalar-companion capstone with sharp phase contractivity supplied by the explicit boundary double-layer probability measure.

theorem crouzeixPalencia_of_thickening_cauchy_support_doubleLayerProbability_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hmass : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity (Omega n) xi t = 1) (hboundarySupport : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (xi - (Omega n).boundaryParam t)).re ≤ 0) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Unit density mass and oriented frontier support already make the boundary double layer a probability measure: integrability follows because a nonintegrable Bochner integral is zero. Thus no separate density integrability witness is needed in this strongest capstone.

theorem oriented_carrier_point_of_convexThickening_numericalRange_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (n : ℕ) : ∃ w ∈ (Omega n).carrier, ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0

The numerical-range support inequality supplies a point of the open carrier whose canonical-normal sign holds for every real parameter. The carrier cannot be nonempty unless the underlying numerical range is nonempty; periodicity then extends the fundamental-interval hypothesis.

theorem boundary_support_of_convexThickening_numericalRange_support {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (n : ℕ) (xi : ℂ) : xi ∈ frontier (Omega n).carrier → ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (xi - (Omega n).boundaryParam t)).re ≤ 0

The existing numerical-range support inequality fixes the orientation of every smooth convex thickening and therefore propagates to all of its frontier points. Nonemptiness of the smooth carrier forces the numerical range to be nonempty through the exact thickening identity, providing the interior point that selects the normal orientation.

theorem crouzeixPalencia_of_thickening_cauchy_support_doubleLayerMass_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hmass : ∀ (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity (Omega n) xi t = 1) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

In the strongest radial capstone, the numerical-range support hypothesis already determines the oriented frontier support needed for density nonnegativity. Thus unit mass is the only remaining explicit geometric premise for the boundary double-layer probability measure.

theorem crouzeixPalencia_of_thickening_cauchy_support_doubleLayer_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

In the strongest convex-thickening capstone, numerical-range support fixes the boundary orientation and the resulting oriented convex geometry forces the double-layer density to have unit mass. Thus phase contractivity requires neither an abstract phase witness nor any separate density integrability, positivity, support, or mass premise.

theorem crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hmass : ∀ (n : ℕ), contourIntegral (resolvent A) (Omega n).boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The all-polynomial Cauchy representation in the strongest boundary double-layer capstone can be reduced to a single resolvent-mass identity at each smooth stage. The exact polynomial resolvent splitting and vanishing of its closed-contour remainder supply every polynomial case internally.

theorem crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_basepointWinding_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hmass : ∀ (n : ℕ), contourIntegral (resolvent A) (Omega n).boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hwind : ∀ (n : ℕ), ∃ c ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) c = 1) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Strict convexity makes the scalar winding kernel constant throughout each carrier. Hence the strongest resolvent-mass boundary-double-layer capstone needs winding normalization only at one carrier basepoint per stage, rather than at every point.

theorem crouzeixPalencia_of_thickening_resolventMass_support_doubleLayer_automaticWinding_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hmass : ∀ (n : ℕ), contourIntegral (resolvent A) (Omega n).boundaryParam = (2 * ↑Real.pi * Complex.I) • 1) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Oriented numerical-range support supplies a consistently oriented point of every smooth carrier, and oriented convex geometry forces the scalar Cauchy kernel there to have winding one. Thus the resolvent-mass boundary-double-layer capstone needs no separate winding hypothesis.

theorem crouzeixPalencia_of_thickening_support_doubleLayer_automaticMass_automaticWinding_radialZero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), 0 < p.natDegree → Polynomial.eval 0 p = 0 → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The numerical-range support condition now supplies both analytic normalizations that were formerly hypotheses: oriented convex winding gives the scalar Cauchy kernel, while affine resolvent homotopy gives the operator resolvent mass. Only polynomial approximation and auxiliary reproduction remain explicit beyond the exact smooth carrier realization.