Assembly from the scalar Plemelj companion

The published fourth-power route to the Crouzeix--Palencia estimate consumes a continuous scalar companion which is contractive on each compact stage, uniformly approximable there by polynomials, and whose auxiliary contour is the conjugate-polynomial auxiliary operator. This file supplies the bridge from the canonical Plemelj construction to that interface.

The remaining analytic inputs stay explicit: convergence of the regularized transform, the sharp lower-degree boundary-phase inequality, uniform polynomial approximation of the resulting closed extension, and reproduction of the original auxiliary contour.

Main declarations

• exists_continuous_scalarCompanion_approximation_of_boundaryPhaseTransform packages the canonical closed extension for one smooth domain;
• crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_approximation feeds those packages through the smooth-thickening fourth-power capstone.

theorem exists_continuous_scalarCompanion_approximation_of_boundaryPhaseTransform {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hbounded : Bornology.IsBounded Omega.carrier) (hkernel : ∀ z ∈ Omega.carrier, crouzeixScalarCauchyKernel Omega z = 1) (hreg : ∀ xi ∈ frontier Omega.carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized Omega p xi) (nhdsWithin xi Omega.carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized Omega p xi xi))) (hphase : ∀ xi ∈ frontier Omega.carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform Omega xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier Omega.carrier)) (r : ℕ → Polynomial ℂ) (happrox : ∀ (j : ℕ), ∀ z ∈ closure Omega.carrier, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension Omega p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : crouzeixAuxiliaryOperator A Omega (crouzeixPolynomialScalarCompanionClosedExtension Omega p) = crouzeixPolynomialAuxiliaryOperator A Omega p) : ∃ (g : ℂ → ℂ) (q : ℕ → Polynomial ℂ), ContinuousOn g (Omega.boundaryParam '' Set.Icc 0 (2 * Real.pi)) ∧ (∀ z ∈ closure Omega.carrier, ‖g z‖ ≤ polynomialSupNorm p (closure Omega.carrier)) ∧ (∀ (j : ℕ), ∀ z ∈ closure Omega.carrier, ‖Polynomial.eval z (q j) - g z‖ ≤ 1 / (↑j + 1)) ∧ crouzeixAuxiliaryOperator A Omega g = crouzeixPolynomialAuxiliaryOperator A Omega p

Regularized Plemelj convergence and the sharp boundary-phase inequality turn the canonical closed scalar companion into the exact continuous and contractive datum used by the polynomial-approximation route. Approximation and reproduction of its auxiliary contour remain explicit analytic inputs.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_approximation {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) (hreg : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi) (nhdsWithin xi (Omega n).carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi xi))) (hphase : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, ‖star (Polynomial.eval xi p) + crouzeixPolynomialBoundaryPhaseTransform (Omega n) xi (p /ₘ (Polynomial.X - Polynomial.C xi))‖ ≤ polynomialSupNorm p (frontier (Omega n).carrier)) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (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 : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

On the explicit smooth thickening exhaustion, the boundary-phase contraction, regularized convergence, polynomial approximation, and contour reproduction together imply the exact Crouzeix--Palencia spectral-set bound.

This is the direct capstone connector for the scalar-companion route. The geometric Cauchy and support hypotheses provide the symmetrized estimate and the finite stagewise calculus bound; the canonical scalar companions provide the cancellation-preserving fourth-power input.