`BookProof.SpectralGapStability.gapAt_perturb` {A B : F →L[ℂ] F} {lam d eps : ℝ} (h : GapAt A lam d) (hAB : ‖A - B‖ ≤ eps) : GapAt B lam (d - eps)
ProvedBookProof.SpectralGapStability.gapAt_perturbtheoremstimepiece
Prove the following Lean 4 theorem from ChapterSpectralGapStability.
BookProof.SpectralGapStability.gapAt_perturb {A B : F →L[ℂ] F} {lam d eps : ℝ} (h : GapAt A lam d) (hAB : ‖A - B‖ ≤ eps) : GapAt B lam (d - eps)
Formalization note: Lean 4 identifier BookProof.SpectralGapStability.gapAt_perturb.
Preamble
-- Generated from ChapterSpectralGapStability.lean — theorem BookProof.SpectralGapStability.gapAt_perturb
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.gapAt_perturb {A B : F →L[ℂ] F} {lam d eps : ℝ}
(h : GapAt A lam d) (hAB : ‖A - B‖ ≤ eps) : GapAt B lam (d - eps) := by sorry