Sharp numerical-range bounds for normal operators

For a normal operator, continuous functional calculus improves the general 1 + sqrt 2 Crouzeix--Palencia constant to 1. This file packages that fact as a polynomial spectral-set theorem, rewrites the norm bound directly on the numerical range, and obtains the classical identity w(A) = ‖A‖.

theorem isPolynomialSpectralSet_closure_numericalRange_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] : IsPolynomialSpectralSet A (closure (numericalRange A))

The closed numerical range is a polynomial spectral set with sharp constant 1 for every normal operator.

theorem norm_aeval_le_polynomialSupNorm_numericalRange_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ polynomialSupNorm p (numericalRange A)

The sharp normal-operator polynomial bound, with the supremum taken directly over the numerical range.

theorem norm_aeval_mul_aeval_le_iSup_numericalRange_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (p q : Polynomial ℂ) : ‖(Polynomial.aeval A) p * (Polynomial.aeval A) q‖ ≤ ⨆ z ∈ numericalRange A, ‖Polynomial.eval z p * Polynomial.eval z q‖

Products in the polynomial functional calculus of a normal operator satisfy the sharp constant-one bound.

theorem norm_aeval_pow_le_iSup_numericalRange_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (p : Polynomial ℂ) (n : ℕ) : ‖(Polynomial.aeval A) p ^ n‖ ≤ ⨆ z ∈ numericalRange A, ‖Polynomial.eval z p ^ n‖

Powers in the polynomial functional calculus of a normal operator satisfy the sharp constant-one bound.

theorem norm_pow_le_numericalRadius_pow_of_isStarNormal {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (n : ℕ) : ‖A ^ n‖ ≤ numericalRadius A ^ n

Powers of a normal operator are bounded sharply by powers of its numerical radius.

theorem norm_pow_le_one_of_isStarNormal_of_numericalRadius_le_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (hA : numericalRadius A ≤ 1) (n : ℕ) : ‖A ^ n‖ ≤ 1

A normal operator in the numerical-radius unit ball is power-bounded by one.