{lo hi : ℕ → ℝ} {lam : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) (hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) : Tendsto (fun m => runHi hi m - runLo lo m) atTop (𝓝 0)
ProvedBookProof.RitzCertificate.runBand_widths_tendsto_zerotimepiece
Lean 4 theorem BookProof.RitzCertificate.runBand_widths_tendsto_zero (module BookProof.RitzCertificate), source chapter BookProof/ChapterRitzCertificate.lean.
Preamble
-- Generated from ChapterRitzCertificate.lean — theorem BookProof.RitzCertificate.runBand_widths_tendsto_zero
import Mathlib
import Definitions.Def_ChapterRitzCertificate
open BookProof.RitzCertificate
noncomputable section
open Filter Topology
open BookProof.FockOneParticleGap BookProof.FockSecondQuantization
open BookProof.ChapterSirkRitzSpectrum BookProof.BandEnclosure
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]Formal statement
theorem BookProof.RitzCertificate.runBand_widths_tendsto_zero {lo hi : ℕ → ℝ} {lam : ℝ}
(hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m))
(hwidth : Tendsto (fun m => hi m - lo m) atTop (𝓝 0)) :
Tendsto (fun m => runHi hi m - runLo lo m) atTop (𝓝 0) := by sorrySource