Reducing smooth outer approximation to the full-dimensional case

For a nonempty compact convex planar set, it is enough to construct smooth Jordan outer approximations when the set has nonempty interior. Before invoking that case, replace the target by its closed half-scale thickening. This thickening is still compact and convex, has nonempty interior, and a second half-scale thickening fits inside the requested original scale.

theorem hasSmoothJordanOuterApproximation_of_nonemptyInterior_case {K : Set ℂ} (hKcompact : IsCompact K) (hKnonempty : K.Nonempty) (hKconvex : Convex ℝ K) (hfull : ∀ (L : Set ℂ), IsCompact L → Convex ℝ L → (interior L).Nonempty → HasSmoothJordanOuterApproximation L) : HasSmoothJordanOuterApproximation K

Smooth outer approximation for compact convex sets with nonempty interior implies the same statement for every nonempty compact convex set.

theorem crouzeix_palencia_of_smoothJordanOuterApproximation_nonemptyInterior_case {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (hfull : ∀ (K : Set ℂ), IsCompact K → Convex ℝ K → (interior K).Nonempty → HasSmoothJordanOuterApproximation K) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

To obtain the exact Crouzeix--Palencia bound, the remaining planar geometry theorem may be restricted to compact convex sets with nonempty interior.