Registry · Lemma IV.L9 tau-effective formalized

IV.L9 — Finite-stage spectral problem

At each stage n >= n_0, Q_n is a symmetric non-negative bilinear form on R^{|P_n(U)|} with finite spectrum 0 = mu_0^(n) <= mu_1^(n) <= ... <= mu_{d_n}^(n), establishing the finite-dimensional spectral problem from which the gap is extracted.

Book IV Part 5 Ch. 40

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookIV.Strong.GapMetaTheorem

Symbol: Tau.BookIV.Strong.FinitestageSpectralProblem