(T : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) (k : ℕ) : Tendsto (fun m : ℕ => minmaxLevelIn T (galerkinSpan b m) k) atTop (nhds (minmaxLevel T k))

Initializing...

(T : F →L[ℂ] F) (b : HilbertBasis ℕ ℂ F) (k : ℕ) : Tendsto (fun m : ℕ => minmaxLevelIn T (galerkinSpan b m) k) atTop (nhds (minmaxLevel T k)) · Prove2Me