Cumulant, drift, and noise tensors in localization coordinates

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_Energy_Generator

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a compactly supported probability measure $\mu$ on $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}n)$ and localization parameter $p$ , energyTensor, lowerTensor, and noiseTensor are coordinate-indexed tensors built from posterior cumulants and the lower drift, after applying the inverse square root of the covariance to Euclidean basis vectors. The noise tensor has one additional distinguished coordinate $k\in\operatorname{Fin}n$ and uses a cumulant of order $r+2$ . conjugatedNoiseOperator is the covariance-conjugated derivative of the noise operator, and sandwich P is the continuous linear map sending an operator $Q$ to $P\circ Q\circ P$ .

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.CumulantGenerator
import FunctionalInequalities.KLS.BKL.Localization.CovarianceGenerator
import FunctionalInequalities.KLS.BKL.Localization.CumulantDerivative
import FunctionalInequalities.KLS.BKL.CumulantEnergy.Conjugation
import FunctionalInequalities.KLS.BKL.Localization.NoiseBound
import FunctionalInequalities.Probability.Diffusion.VectorGenerator
import FunctionalInequalities.Analysis.Tensor.EnergyForm
import FunctionalInequalities.KLS.BKL.Localization.Standardization
import FunctionalInequalities.KLS.BKL.CumulantEnergy.Basic
import FunctionalInequalities.KLS.BKL.Posterior.Covariance
import FunctionalInequalities.Probability.Diffusion.Generator

Original declaration excerpt

Shown in the original module context.

def energyTensor (p : Param n) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    (Fin r → Fin n) → ℝ :=
  fun K => cumulant
    (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (r + 1)
    (Fin.cons u fun s =>
      inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s)))

Module navigation

Direct project imports: KLS/BKL/Localization/CumulantGenerator, KLS/BKL/Localization/CovarianceGenerator, KLS/BKL/Localization/CumulantDerivative, KLS/BKL/CumulantEnergy/Conjugation, KLS/BKL/Localization/NoiseBound, Probability/Diffusion/VectorGenerator, Analysis/Tensor/EnergyForm, KLS/BKL/Localization/Standardization, KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Posterior/Covariance, Probability/Diffusion/Generator.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Localization.Energy.Generator · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantGenerator
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_CumulantEnergy_Conjugation
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_VectorGenerator
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_EnergyForm
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Standardization
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance
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
  FunctionalInequalities.Analysis.CoordinateTensor
namespace FunctionalInequalities
namespace KLS
namespace BKL
namespace Localization
variable {n : ℕ} (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
def energyTensor (p : Param n) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    (Fin r → Fin n) → ℝ :=
  fun K => cumulant
    (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (r + 1)
    (Fin.cons u fun s =>
      inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s)))
def lowerTensor (p : Param n) (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    (Fin r → Fin n) → ℝ :=
  fun K => lowerDrift
    (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n)))
    (Fin.cons u fun s =>
      inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s))) 0
def noiseTensor (p : Param n) (r : ℕ) (u : EuclideanSpace ℝ (Fin n))
    (k : Fin n) : (Fin r → Fin n) → ℝ :=
  fun K => cumulant
    (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (r + 1 + 1)
    (Fin.cons u
      (Fin.snoc
        (fun s =>
          inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s)))
        (inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ k))))
def conjugatedNoiseOperator (p : Param n) (k : Fin n) :
    EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n) :=
  inverseSqrt (cov μ hc p) *
    fderiv ℝ (cov μ hc) p (noise μ hc p k) *
    inverseSqrt (cov μ hc p)
 def sandwich
    (P : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) →L[ℝ]
      (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :=
  ((ContinuousLinearMap.compL ℝ
    (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin n))
    (EuclideanSpace ℝ (Fin n))).flip P).comp
    (ContinuousLinearMap.compL ℝ
      (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin n))
      (EuclideanSpace ℝ (Fin n)) P)
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/Energy/Generator.lean#L32-L137 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Energy.Generator`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_Energy_Generator`; the repository is private at upload time).

View graph