Fixed-direction differential operator for cumulant calculations

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantGenerator

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For normed real vector spaces $U$ and $V$ , fixedOp b s f p is the scalar expression $D f(p)[b]+\frac12\sum_k D(Df)(p)[s_k][s_k]$ , where $b\in U$ , $s:\operatorname{Fin}d\to U$ , and $f:U\to\mathbb R$ . The bundle contains this technical auxiliary definition; no cumulant-generator theorem is declared here.

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.LogLaplaceGenerator
import FunctionalInequalities.KLS.BKL.Localization.Coefficients
import FunctionalInequalities.KLS.BKL.CumulantEnergy.Basic
import FunctionalInequalities.Probability.Posterior.LogPartition
import FunctionalInequalities.KLS.BKL.Posterior.Covariance

Original declaration excerpt

Shown in the original module context.

private def fixedOp {d : ℕ} (b : U) (s : Fin d → U)
    (f : U → ℝ) (p : U) : ℝ :=
  fderiv ℝ f p b + (1 / 2 : ℝ) * ∑ k, fderiv ℝ (fderiv ℝ f) p (s k) (s k)

Module navigation

Direct project imports: KLS/BKL/Localization/LogLaplaceGenerator, KLS/BKL/Localization/Coefficients, KLS/BKL/CumulantEnergy/Basic, Probability/Posterior/LogPartition, KLS/BKL/Posterior/Covariance.

Theorems in source order:

generator_cumulant_posterior

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_LogLaplaceGenerator
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Coefficients
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_LogPartition
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance

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
section Calculus
variable {U V : Type*}
  [NormedAddCommGroup U] [NormedSpace ℝ U]
  [NormedAddCommGroup V] [NormedSpace ℝ V]
 def fixedOp {d : ℕ} (b : U) (s : Fin d → U)
    (f : U → ℝ) (p : U) : ℝ :=
  fderiv ℝ f p b + (1 / 2 : ℝ) * ∑ k, fderiv ℝ (fderiv ℝ f) p (s k) (s k)
end Calculus
variable {n : ℕ} (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
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/CumulantGenerator.lean#L150-L152 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.CumulantGenerator`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantGenerator`; the repository is private at upload time).

View graph