Smooth Jordan domains from rounded finite support functions

The rounded log-sum-exp support curve and its open halfspace envelope provide all fields of SmoothJordanDomain. This file packages that construction and uses arbitrarily tight scale choices to discharge the remaining planar outer approximation problem, culminating in the exact polynomial Crouzeix--Palencia theorem.

noncomputable def polytopeRoundedSupportDomainOfRange {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (hrange : Set.range (polytopeRoundedSupportCurve u delta rho) = frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))) : SmoothJordanDomain

Package a rounded support envelope as a smooth Jordan domain once its support curve has been identified with the envelope frontier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem polytopeRoundedSupportDomainOfRange_carrier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) (hrange : Set.range (polytopeRoundedSupportCurve u delta rho) = frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))) : (polytopeRoundedSupportDomainOfRange hu hdelta hrho hrange).carrier = smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)

theorem Finset.nonempty_of_interior_convexHull_nonempty {u : Finset ℂ} (hinterior : (interior ((convexHull ℝ) ↑u)).Nonempty) : u.Nonempty

A finite point set whose convex hull has nonempty interior is nonempty.

theorem hasSmoothJordanOuterApproximationForPolytopes_of_supportCurve_range (hrange : ∀ {u : Finset ℂ}, u.Nonempty → ∀ {delta rho : ℝ}, 0 < delta → 0 < rho → Set.range (polytopeRoundedSupportCurve u delta rho) = frontier (smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho))) : HasSmoothJordanOuterApproximationForPolytopes

The full-dimensional finite-polytope approximation problem follows from frontier surjectivity of every positive rounded support curve.

noncomputable def polytopeRoundedSupportDomain {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : SmoothJordanDomain

The smooth Jordan domain canonically associated with a nonempty rounded finite support function.

Equations

• polytopeRoundedSupportDomain hu hdelta hrho = polytopeRoundedSupportDomainOfRange hu hdelta hrho ⋯

@[simp]

theorem polytopeRoundedSupportDomain_carrier {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : (polytopeRoundedSupportDomain hu hdelta hrho).carrier = smoothSupportOpenEnvelope (polytopeRoundedSupport u delta rho)

@[simp]

theorem polytopeRoundedSupportDomain_boundaryParam {u : Finset ℂ} (hu : u.Nonempty) {delta rho : ℝ} (hdelta : 0 < delta) (hrho : 0 < rho) : (polytopeRoundedSupportDomain hu hdelta hrho).boundaryParam = polytopeRoundedSupportCurve u delta rho

theorem hasSmoothJordanOuterApproximationForPolytopes : HasSmoothJordanOuterApproximationForPolytopes

Every full-dimensional finite convex hull has arbitrarily tight smooth Jordan outer approximations.

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

The exact Crouzeix--Palencia theorem: the closed numerical range is a 1 + sqrt 2 polynomial spectral set for every bounded operator on a complex Hilbert space.