(T : F →L[ℂ] F) (k : ℕ) (hne : (minmaxSet T k).Nonempty) : -‖T‖ ≤ minmaxLevel T k

Proved

BookProof.RitzPerturbation.neg_norm_le_minmaxLevel

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

Lean 4 theorem BookProof.RitzPerturbation.neg_norm_le_minmaxLevel (module BookProof.RitzPerturbation), source chapter BookProof/ChapterRitzPerturbation.lean.

Preamble

-- Generated from ChapterSirkRitzPerturbation.lean — theorem BookProof.RitzPerturbation.neg_norm_le_minmaxLevel
import Mathlib
import Definitions.Def_ChapterSirkRitzPerturbation
open BookProof.RitzPerturbation








noncomputable section


open BookProof.RitzMinMax BookProof.ChapterSirkRitzSpectrum BookProof.HermiteGalerkin
open Filter Topology

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

Formal statement

theorem BookProof.RitzPerturbation.neg_norm_le_minmaxLevel (T : F →L[ℂ] F) (k : ℕ) (hne : (minmaxSet T k).Nonempty) :
    -‖T‖ ≤ minmaxLevel T k := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterRitzPerturbation.lean

View graph