Set-theoretic characterization of numerical radius

The inequality w(A) ≤ r is equivalent to containment of the numerical range, or its closure, in the closed disk of radius r about zero.

theorem numericalRadius_le_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 ≤ r) : numericalRadius A ≤ r ↔ ∀ z ∈ numericalRange A, ‖z‖ ≤ r

A nonnegative real bounds the numerical radius exactly when it bounds the modulus of every point in the numerical range.

theorem numericalRadius_le_iff_numericalRange_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 ≤ r) : numericalRadius A ≤ r ↔ numericalRange A ⊆ Metric.closedBall 0 r

Closed-disk form of numericalRadius_le_iff.

theorem numericalRadius_le_iff_closure_numericalRange_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 ≤ r) : numericalRadius A ≤ r ↔ closure (numericalRange A) ⊆ Metric.closedBall 0 r

The same disk characterization holds for the closed numerical range.