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

Initializing...

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