Compact supersets of the closed numerical range

The Crouzeix--Palencia estimate, and its normal-operator constant-one improvement, persist on every compact set containing the closed numerical range.

theorem isKPolynomialSpectralSet_of_closure_numericalRange_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hK : IsCompact K) (hsub : closure (numericalRange A) ⊆ K) : IsKPolynomialSpectralSet A (1 + √2) K

Every compact superset of the closed numerical range is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem isPolynomialSpectralSet_of_isStarNormal_of_closure_numericalRange_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] {K : Set ℂ} (hK : IsCompact K) (hsub : closure (numericalRange A) ⊆ K) : IsPolynomialSpectralSet A K

For a normal operator, every compact superset of the closed numerical range is a constant-one polynomial spectral set.

theorem isKPolynomialSpectralSet_closedBall_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : IsKPolynomialSpectralSet A (1 + √2) (Metric.closedBall 0 (numericalRadius A))

The closed disk centered at zero with radius w(A) is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem isPolynomialSpectralSet_closedBall_numericalRadius_of_isStarNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] : IsPolynomialSpectralSet A (Metric.closedBall 0 (numericalRadius A))

For a normal operator, the numerical-radius disk is a constant-one polynomial spectral set.

theorem isKPolynomialSpectralSet_closedBall_of_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : numericalRadius A ≤ R) : IsKPolynomialSpectralSet A (1 + √2) (Metric.closedBall 0 R)

Every centered closed disk whose radius dominates w(A) is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem isPolynomialSpectralSet_closedBall_of_isStarNormal_of_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] {R : ℝ} (hR : numericalRadius A ≤ R) : IsPolynomialSpectralSet A (Metric.closedBall 0 R)

For a normal operator, every centered closed disk whose radius dominates w(A) is a constant-one polynomial spectral set.

theorem isKPolynomialSpectralSet_closedBall_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : IsKPolynomialSpectralSet A (1 + √2) (Metric.closedBall c (numericalRadius (A - c • 1)))

The disk centered at c with radius w(A-cI) is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem isPolynomialSpectralSet_closedBall_centered_numericalRadius_of_isStarNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (c : ℂ) : IsPolynomialSpectralSet A (Metric.closedBall c (numericalRadius (A - c • 1)))

For a normal operator, the disk centered at c with radius w(A-cI) is a constant-one polynomial spectral set.

theorem isKPolynomialSpectralSet_closedBall_of_centered_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : numericalRadius (A - c • 1) ≤ R) : IsKPolynomialSpectralSet A (1 + √2) (Metric.closedBall c R)

Every disk whose radius dominates w(A-cI) is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem isPolynomialSpectralSet_closedBall_of_isStarNormal_of_centered_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (c : ℂ) {R : ℝ} (hR : numericalRadius (A - c • 1) ≤ R) : IsPolynomialSpectralSet A (Metric.closedBall c R)

For a normal operator, every disk whose radius dominates w(A-cI) is a constant-one polynomial spectral set.

theorem norm_aeval_le_one_add_sqrt_two_mul_polynomialNorm_closedBall_of_centered_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : numericalRadius (A - c • 1) ≤ R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ (1 + √2) * polynomialSupNorm p (Metric.closedBall c R)

Direct polynomial form of the Crouzeix--Palencia bound on any disk whose radius dominates w(A-cI).

theorem norm_aeval_le_polynomialSupNorm_closedBall_of_isStarNormal_of_centered_numericalRadius_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (c : ℂ) {R : ℝ} (hR : numericalRadius (A - c • 1) ≤ R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ polynomialSupNorm p (Metric.closedBall c R)

Direct constant-one polynomial bound for a normal operator on any disk whose radius dominates w(A-cI).

theorem exists_minimal_centered_numericalRadius_isKPolynomialSpectralSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) : ∃ (c : ℂ), (∀ (d : ℂ), numericalRadius (A - c • 1) ≤ numericalRadius (A - d • 1)) ∧ IsKPolynomialSpectralSet A (1 + √2) (Metric.closedBall c (numericalRadius (A - c • 1)))

A nontrivial Hilbert space admits a globally minimal centered numerical-radius disk, and that disk is a polynomial spectral set with the Crouzeix--Palencia constant.

theorem exists_minimal_centered_numericalRadius_isPolynomialSpectralSet_of_isStarNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) [IsStarNormal A] : ∃ (c : ℂ), (∀ (d : ℂ), numericalRadius (A - c • 1) ≤ numericalRadius (A - d • 1)) ∧ IsPolynomialSpectralSet A (Metric.closedBall c (numericalRadius (A - c • 1)))

For a normal operator, a globally minimal centered numerical-radius disk is a constant-one polynomial spectral set.