theorem SpectralTheorem.spectrum_isCompact {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) : IsCompact (spectrum ℂ T)

The spectrum of a bounded operator on a complex Banach space is compact.

theorem SpectralTheorem.spectrum_subset_closedBall_norm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NontrivialTopology H] (T : H →L[ℂ] H) : spectrum ℂ T ⊆ Metric.closedBall 0 ‖T‖

The spectrum of a bounded operator is contained in the closed ball of radius ‖T‖.

theorem SpectralTheorem.spectrum_compact_subset_closedBall {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NontrivialTopology H] (T : H →L[ℂ] H) : IsCompact (spectrum ℂ T) ∧ spectrum ℂ T ⊆ Metric.closedBall 0 ‖T‖

The spectrum of a bounded operator is compact and contained in the closed ball of radius ‖T‖.

theorem SpectralTheorem.norm_polynomial_selfAdjoint_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (q : Polynomial ℝ) {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ t ∈ spectrum ℝ A, ‖Polynomial.eval t q‖ ≤ c) : ‖(Polynomial.aeval A) q‖ ≤ c

Polynomial functional calculus norm bound for self-adjoint operators: the operator norm of q(A) is bounded by any uniform bound on |q(t)| over the spectrum.

theorem SpectralTheorem.norm_polynomial_selfAdjoint_le_Icc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (q : Polynomial ℝ) (m M : ℝ) (hspec : spectrum ℝ A ⊆ Set.Icc m M) {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ t ∈ Set.Icc m M, ‖Polynomial.eval t q‖ ≤ c) : ‖(Polynomial.aeval A) q‖ ≤ c

Variant of norm_polynomial_selfAdjoint_le where the bound is verified on a containing interval [m, M] of the spectrum.