Numerical radius of normal operators

For a star-normal operator, the spectral radius equals the operator norm. Since the spectrum lies in the closed numerical-range disk, the numerical radius therefore equals the operator norm.

theorem numericalRadius_eq_norm_of_isStarNormal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] : numericalRadius A = ‖A‖

The numerical radius of a normal operator equals its operator norm.

theorem numericalRadius_eq_norm_of_isSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) : numericalRadius A = ‖A‖

A selfadjoint operator has numerical radius equal to its norm.

theorem numericalRadius_eq_one_of_mem_unitary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : numericalRadius U = 1

A unitary operator on a nontrivial Hilbert space has numerical radius one.