Bauer–Fike theorem

TheoremResolvent norm bound for a normal operator#✓fully proved

The resolvent norm bound for a normal operator: if z lies outside the spectrum of a normal A, then ‖(z • 1 - A)⁻¹‖ ≤ 1 / dist z (spectrum ℂ A).

theorem norm_ringInverse_sub_smul_one_le {A : H →L[ℂ] H} [IsStarNormal A] {z : ℂ}
    (hz : z ∉ spectrum ℂ A) :
    ‖Ring.inverse (algebraMap ℂ (H →L[ℂ] H) z - A)‖
      ≤ (Metric.infDist z (spectrum ℂ A))⁻¹

Used by 1

Used byBauer–Fike theorem

TheoremBauer–Fike theorem#✓fully proved

The Bauer–Fike theorem: every point of the spectrum of A + E lies within ‖E‖ of the spectrum of a normal operator A.

theorem infDist_le_norm_of_mem_spectrum_add {A E : H →L[ℂ] H} [IsStarNormal A]
    {μ : ℂ} (hμ : μ ∈ spectrum ℂ (A + E)) :
    Metric.infDist μ (spectrum ℂ A) ≤ ‖E‖

Uses 1 · Used by 2

Proof usesResolvent norm bound for a normal operator

Used byAttained form of the Bauer–Fike theorem · Hausdorff distance between spectra of self-adjoint perturbations

TheoremAttained form of the Bauer–Fike theorem#✓fully proved

The attained form of Bauer–Fike: some eigenvalue-like point of the spectrum of A is within ‖E‖ of μ.

theorem exists_mem_spectrum_norm_sub_le {A E : H →L[ℂ] H} [IsStarNormal A]
    {μ : ℂ} (hμ : μ ∈ spectrum ℂ (A + E)) :
    ∃ v ∈ spectrum ℂ A, ‖μ - v‖ ≤ ‖E‖

Uses 1

Proof usesBauer–Fike theorem

TheoremHausdorff distance between spectra of self-adjoint perturbations#✓fully proved

For self-adjoint A and A + E, the Hausdorff distance of the two spectra is at most ‖E‖.

theorem hausdorffDist_spectrum_le_of_isSelfAdjoint {A E : H →L[ℂ] H}
    (hA : IsSelfAdjoint A) (hAE : IsSelfAdjoint (A + E)) :
    Metric.hausdorffDist (spectrum ℂ A) (spectrum ℂ (A + E)) ≤ ‖E‖

Uses 1

Proof usesBauer–Fike theorem

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.