Boundedness of the numerical range (L1.2)

The numerical range of a continuous linear operator A on a complex inner product space is contained in the closed disk of radius ‖A‖: for a unit vector x, Cauchy–Schwarz gives ‖⟪x, A x⟫_ℂ‖ ≤ ‖x‖ * ‖A x‖ ≤ ‖x‖ ^ 2 * ‖A‖ = ‖A‖.

Main declarations

• norm_le_of_mem_numericalRange — ‖z‖ ≤ ‖A‖ for every z ∈ numericalRange A.
• numericalRange_subset_closedBall and isBounded_numericalRange — the corresponding set-level forms.
• numericalRadius — the supremum of ‖z‖ over the numerical range, with its elementary nonnegativity and operator-norm bound.

No completeness assumption on E is needed. (Recreated in run-003; the original file was not recovered after the accidental deletion.)

theorem norm_le_of_mem_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {z : ℂ} (hz : z ∈ numericalRange A) : ‖z‖ ≤ ‖A‖

The numerical range lies in the closed disk of radius ‖A‖: for a unit vector x, Cauchy–Schwarz gives ‖⟪x, A x⟫_ℂ‖ ≤ ‖x‖ * ‖A x‖ ≤ ‖A‖.

theorem numericalRange_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : numericalRange A ⊆ Metric.closedBall 0 ‖A‖

The numerical range is contained in the closed disk centered at zero with radius the operator norm.

theorem isBounded_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Bornology.IsBounded (numericalRange A)

The numerical range of every bounded operator is a bounded set.

noncomputable def numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : ℝ

The numerical radius is the supremum of the moduli of points in the numerical range. This definition also gives zero on an empty numerical range, as happens on a subsingleton space.

Equations

• numericalRadius A = ⨆ z ∈ numericalRange A, ‖z‖

theorem numericalRadius_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : 0 ≤ numericalRadius A

The numerical radius is nonnegative.

theorem norm_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {z : ℂ} (hz : z ∈ numericalRange A) : ‖z‖ ≤ numericalRadius A

Every point in the numerical range has modulus at most the numerical radius.

theorem numericalRadius_le_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : numericalRadius A ≤ ‖A‖

The numerical radius is bounded above by the operator norm.