Spectral consequences of the numerical radius

The spectrum of a bounded operator lies in the closed numerical-range disk. Equivalently, every spectral value has modulus at most the numerical radius, and the spectral radius is bounded by the numerical radius.

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

The closure of the numerical range remains in the closed disk determined by the numerical radius.

theorem closure_numericalRange_sub_smul_one_subset_closedBall_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) : closure (numericalRange (A - c • 1)) ⊆ Metric.closedBall 0 (numericalRadius (A - c • 1))

The closed numerical range of a centered operator lies in its zero-centered numerical-radius disk.

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

Every point of the closed numerical range has modulus at most the numerical radius.

theorem norm_le_centered_numericalRadius_of_mem_closure_numericalRange_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) {z : ℂ} (hz : z ∈ closure (numericalRange (A - c • 1))) : ‖z‖ ≤ numericalRadius (A - c • 1)

Every point in the closed numerical range of a centered operator has modulus at most its centered numerical radius.

theorem closure_numericalRange_subset_closedBall_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) : closure (numericalRange A) ⊆ Metric.closedBall c (numericalRadius (A - c • 1))

Centering the operator at c gives a closed disk of radius w(A-cI) that contains the closed numerical range of A.

theorem dist_le_centered_numericalRadius_of_mem_closure_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) {z : ℂ} (hz : z ∈ closure (numericalRange A)) : dist z c ≤ numericalRadius (A - c • 1)

Every point of the closed numerical range lies within w(A-cI) of the chosen center c.

theorem spectrum_subset_closedBall_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : spectrum ℂ A ⊆ Metric.closedBall 0 (numericalRadius A)

The spectrum is contained in the closed disk whose radius is the numerical radius.

theorem spectrum_sub_smul_one_subset_closedBall_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : spectrum ℂ (A - c • 1) ⊆ Metric.closedBall 0 (numericalRadius (A - c • 1))

The spectrum of a centered operator lies in its zero-centered numerical-radius disk.

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

Every spectral value has modulus at most the numerical radius.

theorem norm_le_centered_numericalRadius_of_mem_spectrum_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {z : ℂ} (hz : z ∈ spectrum ℂ (A - c • 1)) : ‖z‖ ≤ numericalRadius (A - c • 1)

Every spectral value of a centered operator has modulus at most its centered numerical radius.

theorem spectrum_subset_closedBall_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : spectrum ℂ A ⊆ Metric.closedBall c (numericalRadius (A - c • 1))

The spectrum lies in the disk centered at c with radius w(A-cI).

theorem dist_le_centered_numericalRadius_of_mem_spectrum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {z : ℂ} (hz : z ∈ spectrum ℂ A) : dist z c ≤ numericalRadius (A - c • 1)

Every spectral value lies within w(A-cI) of the chosen center c.

theorem isUnit_smul_one_sub_of_numericalRadius_lt_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {z : ℂ} (hz : numericalRadius A < ‖z‖) : IsUnit (z • 1 - A)

Every scalar whose modulus is larger than the numerical radius belongs to the resolvent set.

theorem isUnit_smul_one_sub_of_centered_numericalRadius_lt_dist {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {z : ℂ} (hz : numericalRadius (A - c • 1) < dist z c) : IsUnit (z • 1 - A)

More generally, a scalar outside the disk centered at c with radius w(A-cI) belongs to the resolvent set of A.

theorem isUnit_one_sub_of_numericalRadius_lt_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : numericalRadius A < 1) : IsUnit (1 - A)

In particular, 1-A is a unit whenever w(A) < 1.

theorem spectralRadius_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : spectralRadius ℂ A ≤ ENNReal.ofReal (numericalRadius A)

The spectral radius is bounded by the numerical radius.

theorem spectralRadius_sub_smul_one_le_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : spectralRadius ℂ (A - c • 1) ≤ ENNReal.ofReal (numericalRadius (A - c • 1))

Centered form of the spectral-radius bound.

theorem spectralRadius_toReal_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : (spectralRadius ℂ A).toReal ≤ numericalRadius A

Real-valued form of spectralRadius_le_numericalRadius.

theorem spectralRadius_sub_smul_one_toReal_le_centered_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : (spectralRadius ℂ (A - c • 1)).toReal ≤ numericalRadius (A - c • 1)

Real-valued centered form of the spectral-radius bound.