Reducing smooth outer approximation to convex polytopes

Every compact convex subset of a finite-dimensional real normed space can be sandwiched between itself and any prescribed neighborhood by the convex hull of finitely many points, with the original set contained in the interior of that hull. Applying this theorem in the complex plane reduces the remaining smooth outer-approximation problem to full-dimensional convex polytopes.

The two half-scale thickenings in the proof compose to the originally requested scale. Consequently the same finite-convex-hull hypothesis reaches the exact Crouzeix--Palencia operator bound.

def HasSmoothJordanOuterApproximationForPolytopes : Prop

Smooth Jordan outer approximation holds for every full-dimensional convex polytope in the complex plane, where a polytope is presented as the convex hull of a finite set of points.

Equations

• HasSmoothJordanOuterApproximationForPolytopes = ∀ (u : Finset ℂ), (interior ((convexHull ℝ) ↑u)).Nonempty → HasSmoothJordanOuterApproximation ((convexHull ℝ) ↑u)

theorem hasSmoothJordanOuterApproximation_of_polytope_case {K : Set ℂ} (hKcompact : IsCompact K) (hKnonempty : K.Nonempty) (hKconvex : Convex ℝ K) (hpoly : HasSmoothJordanOuterApproximationForPolytopes) : HasSmoothJordanOuterApproximation K

The full smooth outer-approximation theorem reduces to the full-dimensional convex-polytope case.

theorem crouzeix_palencia_of_smoothJordanOuterApproximation_polytope_case {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (hpoly : HasSmoothJordanOuterApproximationForPolytopes) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

It is enough to solve smooth outer approximation for full-dimensional finite convex hulls in order to obtain the exact Crouzeix--Palencia bound.