Smooth Jordan exhaustions from rounded support envelopes

The finite-polytope construction gives more than the terminal operator inequality: combined with the polytope reduction, it supplies arbitrarily tight smooth Jordan outer approximations of every nonempty compact convex planar set. This file exposes that geometric consequence and packages the resulting strict nested exhaustion, including the canonical specialization to the closed numerical range of an operator.

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

Every nonempty compact convex planar set admits arbitrarily tight smooth Jordan outer approximations.

noncomputable def StrictNestedSmoothJordanExhaustion.ofCompactConvex (K : Set ℂ) (hKcompact : IsCompact K) (hKnonempty : K.Nonempty) (hKconvex : Convex ℝ K) : StrictNestedSmoothJordanExhaustion K

The rounded-support construction canonically produces a strict nested smooth Jordan exhaustion of every nonempty compact convex planar set.

Equations

• StrictNestedSmoothJordanExhaustion.ofCompactConvex K hKcompact hKnonempty hKconvex = StrictNestedSmoothJordanExhaustion.ofOuterApproximation K hKcompact hKconvex ⋯

theorem isCompact_closure_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : IsCompact (closure (numericalRange A))

The closure of the numerical range of a bounded operator is compact.

theorem nonempty_closure_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : (closure (numericalRange A)).Nonempty

On a nontrivial Hilbert space the numerical range, and hence its closure, is nonempty.

theorem hasSmoothJordanOuterApproximation_closure_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : HasSmoothJordanOuterApproximation (closure (numericalRange A))

The closed numerical range has arbitrarily tight smooth Jordan outer approximations.

noncomputable def StrictNestedSmoothJordanExhaustion.numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : StrictNestedSmoothJordanExhaustion (closure (_root_.numericalRange A))

The canonical strict nested smooth Jordan exhaustion of the closed numerical range.

Equations

• StrictNestedSmoothJordanExhaustion.numericalRange A = StrictNestedSmoothJordanExhaustion.ofCompactConvex (closure (numericalRange A)) ⋯ ⋯ ⋯