Crouzeix--Palencia assembly from smooth Jordan geometry

The unconditional Mergelyan theorem for smooth convex Jordan domains removes the analytic approximation hypotheses from the terminal exhaustion assemblies. What remains is purely geometric: construct a strictly nested smooth Jordan exhaustion, or realize the explicit convex thickenings by such domains.

theorem crouzeix_palencia_of_strictNestedSmoothJordanExhaustion {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : StrictNestedSmoothJordanExhaustion (closure (numericalRange A))) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Every strict smooth-Jordan exhaustion of the closed numerical range gives the exact Crouzeix--Palencia polynomial spectral-set bound.

theorem crouzeix_palencia_of_convexThickening_smoothJordanRealization {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) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Smooth Jordan realizations of the explicit metric thickenings discharge all analytic inputs to the Crouzeix--Palencia assembly.

theorem crouzeix_palencia_of_exists_convexThickening_smoothJordanRealization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hrealize : ∃ (Omega : ℕ → SmoothJordanDomain), ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Existence-only form of the explicit-thickening boundary: once each thickening has a smooth Jordan realization, the sharp bound follows.