Numerical range — compactness in finite dimension

W(A) is the image of the unit sphere under the continuous map x ↦ ⟪x, A x⟫_ℂ. When E is finite-dimensional the unit sphere is compact, so W(A) is compact, in particular closed.

Main declarations

• numericalRange_eq_image — numericalRange A = (fun x => ⟪x, A x⟫_ℂ) '' sphere 0 1.
• isCompact_numericalRange, isClosed_numericalRange — for [FiniteDimensional ℂ E].

In infinite dimension W(A) need not be closed (the unilateral shift has W(S) the open unit disk), which is why spectrum_subset_closure_numericalRange carries a closure; see spectrum_subset_numericalRange for the finite-dimensional statement without it.

theorem numericalRange_eq_image {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : numericalRange A = (fun (x : E) => inner ℂ x (A x)) '' Metric.sphere 0 1

The numerical range is the image of the unit sphere under x ↦ ⟪x, A x⟫_ℂ.

theorem isCompact_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (A : E →L[ℂ] E) : IsCompact (numericalRange A)

In finite dimension the numerical range is compact: the continuous image of the unit sphere.

theorem isClosed_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (A : E →L[ℂ] E) : IsClosed (numericalRange A)

In finite dimension the numerical range is closed.