{A : F →L[ℂ] F} (hA : IsSelfAdjoint A) {l b : ℝ} {x : F} (hsep : SpectralSeparation A l b) (hx : ‖x‖ = 1) (hlt : rayleigh A x < b) : rayleigh A x - resid A x ^ 2 / (b

Initializing...

{A : F →L[ℂ] F} (hA : IsSelfAdjoint A) {l b : ℝ} {x : F} (hsep : SpectralSeparation A l b) (hx : ‖x‖ = 1) (hlt : rayleigh A x < b) : rayleigh A x - resid A x ^ 2 / (b - rayleigh A x) ≤ l · Prove2Me