Nonemptiness of the numerical range

The numerical range is nonempty exactly when the underlying inner-product space is nontrivial. Thus the only empty numerical ranges are those on a subsingleton space.

theorem numericalRange_nonempty_iff_nontrivial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : (numericalRange A).Nonempty ↔ Nontrivial E

The numerical range is nonempty exactly when the underlying space is nontrivial.

theorem nonempty_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : (numericalRange A).Nonempty

On a nontrivial space, every bounded operator has nonempty numerical range.

theorem numericalRange_eq_empty_iff_subsingleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : numericalRange A = ∅ ↔ Subsingleton E

The numerical range is empty exactly on a subsingleton space.

theorem closure_numericalRange_nonempty_iff_nontrivial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : (closure (numericalRange A)).Nonempty ↔ Nontrivial E

Closing the numerical range does not change its nonemptiness characterization.

theorem closure_numericalRange_eq_empty_iff_subsingleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : closure (numericalRange A) = ∅ ↔ Subsingleton E

The closed numerical range is empty exactly on a subsingleton space.