Lyapunov function and trace-coordinate maps for localization

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_Lyapunov_Basic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $n\in\mathbb N$ , Vec n is the Euclidean space $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$ , and Op n is its space of continuous linear endomorphisms. The maps entryMap and traceMap evaluate an operator through inner products with coordinate basis vectors, with traceMap summing the diagonal entries. Given a probability measure $\mu$ on Vec n whose support is compact, lyapunov μ hc p is the real-valued function $1+\|p.1\|^2+\|p.2\|_{HS}^2+\operatorname{tr}(\operatorname{cov}(\mu,p)^{-1})^2$ for a localization parameter $p$ .

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.CovarianceGenerator
import FunctionalInequalities.KLS.BKL.Localization.CumulantDerivative
import FunctionalInequalities.KLS.BKL.Localization.NoiseBound
import FunctionalInequalities.Analysis.Operator.HilbertSchmidt
import FunctionalInequalities.Probability.Diffusion.VectorGenerator
import FunctionalInequalities.Probability.Diffusion.InverseCalculus
import FunctionalInequalities.KLS.BKL.Posterior.Covariance
import FunctionalInequalities.KLS.BKL.Posterior.Regularity
import FunctionalInequalities.Probability.Diffusion.Generator

Original declaration excerpt

Shown in the original module context.

private abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)

Module navigation

Direct project imports: KLS/BKL/Localization/CovarianceGenerator, KLS/BKL/Localization/CumulantDerivative, KLS/BKL/Localization/NoiseBound, Analysis/Operator/HilbertSchmidt, Probability/Diffusion/VectorGenerator, Probability/Diffusion/InverseCalculus, KLS/BKL/Posterior/Covariance, KLS/BKL/Posterior/Regularity, Probability/Diffusion/Generator.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Localization.Lyapunov.Basic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CovarianceGenerator
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantDerivative
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_HilbertSchmidt
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_VectorGenerator
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_InverseCalculus
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Regularity
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Generator

noncomputable section
open MeasureTheory
open scoped RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Probability.Diffusion
namespace FunctionalInequalities
namespace KLS
namespace BKL
namespace Localization
 abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)
 abbrev Op (n : ℕ) := FunctionalInequalities.KLS.BKL.Localization.Vec n →L[ℝ] FunctionalInequalities.KLS.BKL.Localization.Vec n
 def entryMap {n : ℕ} (x y : FunctionalInequalities.KLS.BKL.Localization.Vec n) : FunctionalInequalities.KLS.BKL.Localization.Op n →L[ℝ] ℝ :=
  (innerSL ℝ x).comp (ContinuousLinearMap.apply ℝ (FunctionalInequalities.KLS.BKL.Localization.Vec n) y)
 def traceMap {n : ℕ} : FunctionalInequalities.KLS.BKL.Localization.Op n →L[ℝ] ℝ :=
  ∑ i : Fin n,
    FunctionalInequalities.KLS.BKL.Localization.entryMap (EuclideanSpace.basisFun (Fin n) ℝ i)
      (EuclideanSpace.basisFun (Fin n) ℝ i)
variable {n : ℕ} (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
/-- The Lyapunov function `𝒱(c, Q) = 1 + ‖c‖² + ‖Q‖²_HS + (tr A(p)⁻¹)²` of the localization (67) (non-explosion of
the cutoff Eldan processes, uniformly in the cutoff). -/
def lyapunov (p : Param n) : ℝ :=
  1 + ‖p.1‖ ^ 2 + hsNormSq p.2 + stdTrace (Ring.inverse (cov μ hc p)) ^ 2
end Localization
end BKL
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Lyapunov/Basic.lean#L24-L184 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Lyapunov.Basic`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_Lyapunov_Basic`; the repository is private at upload time).

View graph