`BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound` {A : F →L[ℂ] F} (hA : IsSelfAdjoint A) {c q : ℝ} (hq : 0 < q) (hbound : ∀ x : F, q * ‖x‖ ^ 2 ≤ ‖(A - (c :

Proved

BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSpectralGapStability.

BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound {A : F →L[ℂ] F} (hA : IsSelfAdjoint A) {c q : ℝ} (hq : 0 < q) (hbound : ∀ x : F, q * ‖x‖ ^ 2 ≤ ‖(A - (c : ℂ) • (1 : F →L[ℂ] F)) x‖ ^ 2) : ∀ lam ∈ Set.Ioo (c - Real.sqrt q) (c + Real.sqrt q), (lam : ℂ) ∉ spectrum ℂ A

Formalization note: Lean 4 identifier BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound.

Preamble

-- Generated from ChapterSpectralGapStability.lean — theorem BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound
import Mathlib
import Definitions.Def_ChapterSpectralGapStability
open BookProof.SpectralGapStability


noncomputable section


open scoped InnerProductSpace
open Filter Topology

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

Formal statement

theorem BookProof.SpectralGapStability.spectrum_disjoint_of_shifted_square_bound {A : F →L[ℂ] F} (hA : IsSelfAdjoint A)
    {c q : ℝ} (hq : 0 < q)
    (hbound : ∀ x : F, q * ‖x‖ ^ 2 ≤ ‖(A - (c : ℂ) • (1 : F →L[ℂ] F)) x‖ ^ 2) :
    ∀ lam ∈ Set.Ioo (c - Real.sqrt q) (c + Real.sqrt q),
      (lam : ℂ) ∉ spectrum ℂ A := by sorry

View graph