[Nontrivial F] (T : F →L[ℂ] F) : minmaxLevel T 0 = rayleighInf T
OpenBookProof.RitzMinMax.minmaxLevel_zero_eq_rayleighInftimepiece
Lean 4 theorem BookProof.RitzMinMax.minmaxLevel_zero_eq_rayleighInf (module BookProof.RitzMinMax), source chapter BookProof/ChapterRitzMinMax.lean.
Preamble
-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.minmaxLevel_zero_eq_rayleighInf
import Mathlib
import Definitions.Def_ChapterSirkRitzMinMax
open BookProof.RitzMinMax
noncomputable section
open BookProof.HermiteGalerkin BookProof.ChapterSirkRitzSpectrum
open Filter Topology
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]Formal statement
theorem BookProof.RitzMinMax.minmaxLevel_zero_eq_rayleighInf [Nontrivial F] (T : F →L[ℂ] F) :
minmaxLevel T 0 = rayleighInf T := by sorrySource