Coordinate trace and Hilbert–Schmidt square norm

Definition

KLSModular_FunctionalInequalities_Analysis_Operator_HilbertSchmidt

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

stdTrace M is the trace of a continuous operator $M$ on $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)$ computed in the standard basis: $\sum_i\langle e_i,Me_i\rangle$ . hsNormSq M is the squared Hilbert–Schmidt norm $\sum_i\sum_j\langle e_i,Me_j\rangle^2$ . Both are real-valued finite sums and require no positivity or symmetry assumption on $M$ .

Original module imports

import Mathlib
import Mathlib.Analysis.InnerProductSpace.Trace

Original declaration excerpt

Shown in the original module context.

def stdTrace (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ i, ⟪EuclideanSpace.basisFun (Fin n) ℝ i, M (EuclideanSpace.basisFun (Fin n) ℝ i)⟫

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Operator.HilbertSchmidt · Frozen source 408915f.

Definition code

import Mathlib
import Mathlib.Analysis.InnerProductSpace.Trace

noncomputable section
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Analysis
variable {n : ℕ}
/-- The coordinate trace `tr M = Σ_i ⟪e_i, M e_i⟫` of an operator on `ℝⁿ`. -/
def stdTrace (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ i, ⟪EuclideanSpace.basisFun (Fin n) ℝ i, M (EuclideanSpace.basisFun (Fin n) ℝ i)⟫
/-- The squared Hilbert–Schmidt norm `‖M‖²_HS = Σ_{i,j} ⟪e_i, M e_j⟫²`. -/
def hsNormSq (M : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) : ℝ :=
  ∑ i, ∑ j, ⟪EuclideanSpace.basisFun (Fin n) ℝ i, M (EuclideanSpace.basisFun (Fin n) ℝ j)⟫ ^ 2
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Operator/HilbertSchmidt.lean#L54-L60 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Operator.HilbertSchmidt`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Operator_HilbertSchmidt`; the repository is private at upload time).

View graph