(T : F →L[ℂ] F) (c : ℝ) (hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) : minmaxGap (shiftOp T c) = minmaxGap T
OpenBookProof.RitzPerturbation.minmaxGap_shiftOptimepiece
Lean 4 theorem BookProof.RitzPerturbation.minmaxGap_shiftOp (module BookProof.RitzPerturbation), source chapter BookProof/ChapterRitzPerturbation.lean.
Preamble
-- Generated from ChapterSirkRitzPerturbation.lean — theorem BookProof.RitzPerturbation.minmaxGap_shiftOp
import Mathlib
import Definitions.Def_ChapterSirkRitzPerturbation
open BookProof.RitzPerturbation
noncomputable section
open BookProof.RitzMinMax BookProof.ChapterSirkRitzSpectrum BookProof.HermiteGalerkin
open Filter Topology
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]Formal statement
theorem BookProof.RitzPerturbation.minmaxGap_shiftOp (T : F →L[ℂ] F) (c : ℝ)
(hne0 : (minmaxSet T 0).Nonempty) (hne1 : (minmaxSet T 1).Nonempty) :
minmaxGap (shiftOp T c) = minmaxGap T := by sorrySource