Positive Quadratic Floor for Positive-Definite Matrices

Proved

FunctionalInequalities.Analysis.exists_quadraticFloor_of_posDef_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $\iota$ be a finite index type and let $S$ be a positive-definite real matrix indexed by $\iota$ . Then there exists $a>0$ such that QuadraticFloor S a holds; equivalently, every vector $v$ satisfies

a\|v\|^2\le\langle v,Sv\rangle.

The conclusion also covers the empty index type, where the theorem supplies the explicit floor $a=1$ . This is a finite-dimensional matrix positivity lemma.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_quadraticFloor_of_posDef {S : Matrix ι ι ℝ} (hS : S.PosDef) :
    ∃ a : ℝ, 0 < a ∧ QuadraticFloor S a

Module navigation

Module: Analysis/Matrix/Positivity.

Previous: posSemidef_weightedGram · Next: root_difference_bound.

Source excerpt, lines 133–134 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity

variable {ι κ : Type*} [Fintype ι] [Fintype κ]
variable [DecidableEq ι]

Formal statement


theorem FunctionalInequalities.Analysis.exists_quadraticFloor_of_posDef_readable {S : Matrix ι ι ℝ} (hS : S.PosDef) :
    ∃ a : ℝ, 0 < a ∧ QuadraticFloor S a := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Positivity.lean#L131-L145 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Positivity`, declaration `FunctionalInequalities.Analysis.exists_quadraticFloor_of_posDef`; the repository is private at upload time).

View graph