Polynomials in a normal element — the sup-norm bound

For a normal element a of a C*-algebra and a compact set K ⊇ σ(a), ‖p(a)‖ ≤ sup_{z ∈ K} ‖p(z)‖ for every polynomial p: p(a) is normal, so its norm is its spectral radius, and σ(p(a)) = p(σ(a)) ⊆ p(K) by the spectral mapping theorem.

Main declarations

• norm_aeval_le_polynomialSupNorm_of_isStarNormal_aeval — the same bound under the weaker hypothesis that the single element p(a) is normal.
• norm_aeval_le_polynomialSupNorm_of_isStarNormal — the bound above, in any C*-algebra.

Consumers: unitaries with K the closed unit disk (Crouzeix/VonNeumann.lean), and normal operators on a Hilbert space with K = closure W(A) (Crouzeix/Palencia.lean).

theorem norm_aeval_le_polynomialSupNorm_of_isStarNormal_aeval {A : Type u_1} [CStarAlgebra A] (a : A) {K : Set ℂ} (hK : IsCompact K) (hσ : spectrum ℂ a ⊆ K) (p : Polynomial ℂ) [IsStarNormal ((Polynomial.aeval a) p)] : ‖(Polynomial.aeval a) p‖ ≤ polynomialSupNorm p K

If the single element p(a) is normal and K is compact with K ⊇ σ(a), then ‖p(a)‖ ≤ polynomialSupNorm p K. Normality of a itself is not needed.

theorem norm_aeval_le_polynomialSupNorm_of_isStarNormal {A : Type u_1} [CStarAlgebra A] (a : A) [IsStarNormal a] {K : Set ℂ} (hK : IsCompact K) (hσ : spectrum ℂ a ⊆ K) (p : Polynomial ℂ) : ‖(Polynomial.aeval a) p‖ ≤ polynomialSupNorm p K

For a normal element a of a C*-algebra and a compact K ⊇ σ(a), ‖p(a)‖ ≤ polynomialSupNorm p K: p(a) is normal, so ‖p(a)‖ is its spectral radius, and σ(p(a)) = p(σ(a)) by the spectral mapping theorem.