Matrix-entry coordinates and quadratic floors

Definition

KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

FunctionalInequalities.Analysis.matrixEntries views a real matrix as an element of the Euclidean space indexed by pairs of indices, using the Frobenius-coordinate representation. QuadraticFloor A a means that $a\sum_i v_i^2\le v\,\mathbin{\text{⬝ᵥ}}\,(A\,\mathbin{\text{*ᵥ}}\,v)$ for every coordinate vector v. The private outer definition forms the matrix with entries $v_i v_j$ .

Original module imports

import Mathlib.Analysis.Matrix.Order
import Mathlib.Analysis.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.Kronecker
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.CStarAlgebra.Matrix
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Original declaration excerpt

Shown in the original module context.

def matrixEntries (A : Matrix ι ι ℝ) : EuclideanSpace ℝ (ι × ι) :=
  WithLp.toLp 2 (fun ij => A ij.1 ij.2)

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Matrix.Positivity · Frozen source 408915f.

Definition code

import Mathlib.Analysis.Matrix.Order
import Mathlib.Analysis.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.Kronecker
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.CStarAlgebra.Matrix
import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

noncomputable section
open scoped MatrixOrder Kronecker
namespace FunctionalInequalities
namespace Analysis
variable {ι κ : Type*} [Fintype ι] [Fintype κ]
section Frobenius
open Matrix Finset
open scoped RealInnerProductSpace
/-- Euclidean view of the matrix entries; its norm is the Frobenius norm. -/
def matrixEntries (A : Matrix ι ι ℝ) : EuclideanSpace ℝ (ι × ι) :=
  WithLp.toLp 2 (fun ij => A ij.1 ij.2)
end Frobenius
section Floor
open Matrix Finset
open scoped RealInnerProductSpace Matrix.Norms.L2Operator
/-- A quadratic lower floor `a ‖v‖² ≤ ⟪v, A v⟫` in coordinates. -/
def QuadraticFloor (A : Matrix ι ι ℝ) (a : ℝ) : Prop :=
  ∀ v : ι → ℝ, a * (∑ i, (v i) ^ 2) ≤ v ⬝ᵥ (A *ᵥ v)
variable [DecidableEq ι]
 def outer (v : ι → ℝ) : Matrix ι ι ℝ := fun i j => v i * v j
end Floor
end Analysis
end FunctionalInequalities

Source

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

View graph