[Nontrivial F] (T : F →L[ℂ] F) (hT : IsSelfAdjoint T) : minmaxLevel T 0 = sInf (spectrum ℝ T)
OpenBookProof.RitzMinMax.minmaxLevel_zero_eq_sInf_spectrumtimepiece
Lean 4 theorem BookProof.RitzMinMax.minmaxLevel_zero_eq_sInf_spectrum (module BookProof.RitzMinMax), source chapter BookProof/ChapterRitzMinMax.lean.
Preamble
-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.minmaxLevel_zero_eq_sInf_spectrum
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_sInf_spectrum [Nontrivial F] (T : F →L[ℂ] F)
(hT : IsSelfAdjoint T) : minmaxLevel T 0 = sInf (spectrum ℝ T) := by sorrySource