Attainment of numerical radius in finite dimension

In a nontrivial finite-dimensional Hilbert space the numerical range is a nonempty compact set, so its norm achieves the numerical radius.

theorem exists_mem_numericalRange_norm_eq_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : ∃ z ∈ numericalRange A, ‖z‖ = numericalRadius A

In finite dimension, some point of the numerical range has modulus equal to the numerical radius.

theorem exists_norm_eq_one_norm_inner_apply_eq_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : ∃ (x : E), ‖x‖ = 1 ∧ ‖inner ℂ x (A x)‖ = numericalRadius A

In finite dimension, a unit vector attains the numerical radius.