Spectrum of self-adjoint operators

TheoremSpectrum of an accretive operator has nonnegative real part#✓fully proved

Let \(T\) be a bounded linear operator on a Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\). If \(\operatorname{Re}\langle Tu, u\rangle \ge 0\) for every \(u \in H\), then every element \(\mu\) of the spectrum of \(T\) satisfies \(\operatorname{Re}\mu \ge 0\).

theorem spectrum_re_nonneg_of_reApplyInnerSelf_nonneg {T : H →L[𝕜] H}
    (hpos : ∀ u : H, 0 ≤ T.reApplyInnerSelf u) :
    ∀ μ ∈ spectrum 𝕜 T, 0 ≤ RCLike.re μ

Used by 1

Used byPositivity iff spectrum nonnegative

TheoremPositivity iff spectrum nonnegative#✓fully proved

Let \(T\) be a self-adjoint bounded linear operator on a nonzero Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\). Then \(\operatorname{Re}\langle Tu, u\rangle \ge 0\) for every \(u \in H\) if and only if every element \(\mu\) of the spectrum of \(T\) satisfies \(\operatorname{Re}\mu \ge 0\).

theorem positive_iff_spectrum_nonneg [Nontrivial H] (T : H →L[𝕜] H) (hT : IsSelfAdjoint T) :
    (∀ u : H, 0 ≤ T.reApplyInnerSelf u) ↔
    (∀ μ ∈ spectrum 𝕜 T, 0 ≤ RCLike.re μ)

Uses 1

Proof usesSpectrum of an accretive operator has nonnegative real part

TheoremRayleigh quotient of a shifted operator#✓fully proved

Let \(T\) be a bounded linear operator on an inner product space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\), let \(I\) be the identity operator on \(H\), and write \(R_S(x) = \operatorname{Re}\langle Sx, x\rangle / \|x\|^2\) for the Rayleigh quotient of an operator \(S\). Then for every real number \(t\) and every nonzero \(x \in H\), \(R_{tI - T}(x) = t - R_T(x)\).

theorem rayleighQuotient_algebraMap_sub (T : H →L[𝕜] H) (t : ℝ) (x : H) (hx : x ≠ 0) :
    ((algebraMap 𝕜 (H →L[𝕜] H)) (↑t : 𝕜) - T).rayleighQuotient x =
      t - T.rayleighQuotient x

Used by 1

Used bySpectrum bounds over nonzero vectors

TheoremSpectrum bounds over nonzero vectors#✓fully proved

Let \(T\) be a self-adjoint bounded linear operator on a nonzero Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\), with Rayleigh quotient \(R_T(x) = \operatorname{Re}\langle Tx, x\rangle / \|x\|^2\). Then every \(\mu\) in the spectrum of \(T\) satisfies \(\inf_{x \ne 0} R_T(x) \le \operatorname{Re}\mu \le \sup_{x \ne 0} R_T(x)\), where the infimum and supremum range over the nonzero vectors \(x \in H\).

theorem selfAdjoint_spectrum_subset_Icc_nonzero [Nontrivial H]
    (T : H →L[𝕜] H) (hT : IsSelfAdjoint T) {mu : 𝕜} (hmu : mu ∈ spectrum 𝕜 T) :
    ⨅ x : {x : H // x ≠ 0}, T.rayleighQuotient x.1 ≤ RCLike.re mu ∧
    RCLike.re mu ≤ ⨆ x : {x : H // x ≠ 0}, T.rayleighQuotient x.1

Uses 1 · Used by 1

Proof usesRayleigh quotient of a shifted operator

Used bySpectrum bounds over all vectors

TheoremSpectrum bounds over all vectors#✓fully proved

Let \(T\) be a self-adjoint bounded linear operator on a nonzero Hilbert space \(H\) over \(\mathbb{R}\) or \(\mathbb{C}\), with Rayleigh quotient \(R_T(x) = \operatorname{Re}\langle Tx, x\rangle / \|x\|^2\) for \(x \ne 0\) and \(R_T(0) = 0\). Then every \(\mu\) in the spectrum of \(T\) satisfies \(\inf_{x \in H} R_T(x) \le \operatorname{Re}\mu \le \sup_{x \in H} R_T(x)\).

Unlike the bounds over nonzero vectors, these extrema also take into account the value \(0\) of the quotient at \(x = 0\).

theorem selfAdjoint_spectrum_subset_Icc [Nontrivial H]
    (T : H →L[𝕜] H) (hT : IsSelfAdjoint T) {mu : 𝕜} (hmu : mu ∈ spectrum 𝕜 T) :
    ⨅ x : H, T.rayleighQuotient x ≤ RCLike.re mu ∧
    RCLike.re mu ≤ ⨆ x : H, T.rayleighQuotient x

Uses 1

Proof usesSpectrum bounds over nonzero vectors

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.