{A : F →L[ℂ] F} {b delta : ℝ} {x : ℕ → F} (hdelta : 0 < delta) (hle : ∀ m, rayleigh A (x m) ≤ b - delta) (hres : Tendsto (fun m => resid A (x m)) atTop (𝓝 0)) : Tendsto (fun m =>...
ProvedBookProof.RitzCertificate.temple_width_tendsto_zerotimepiece
Lean 4 theorem BookProof.RitzCertificate.temple_width_tendsto_zero (module BookProof.RitzCertificate), source chapter BookProof/ChapterRitzCertificate.lean.
Preamble
-- Generated from ChapterRitzCertificate.lean — theorem BookProof.RitzCertificate.temple_width_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.temple_width_tendsto_zero {A : F →L[ℂ] F} {b delta : ℝ} {x : ℕ → F}
(hdelta : 0 < delta) (hle : ∀ m, rayleigh A (x m) ≤ b - delta)
(hres : Tendsto (fun m => resid A (x m)) atTop (𝓝 0)) :
Tendsto (fun m => rayleigh A (x m) -
(rayleigh A (x m) - resid A (x m) ^ 2 / (b - rayleigh A (x m)))) atTop (𝓝 0) := by sorrySource