(T : F →L[ℂ] F) {x : F} (hx1 : ‖x‖ = 1) : rayleighVal T x ≤ ‖T‖
ProvedBookProof.RitzMinMax.rayleighVal_le_norm_of_unittimepiece
Lean 4 theorem BookProof.RitzMinMax.rayleighVal_le_norm_of_unit (module BookProof.RitzMinMax), source chapter BookProof/ChapterRitzMinMax.lean.
Preamble
-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.rayleighVal_le_norm_of_unit
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.rayleighVal_le_norm_of_unit (T : F →L[ℂ] F) {x : F} (hx1 : ‖x‖ = 1) :
rayleighVal T x ≤ ‖T‖ := by sorrySource