Cumulant gradient vector

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Local

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a measure $\mu$ on a finite-dimensional real inner-product space $E$ and a list hs of vectors, cumulantVector μ hs is the Riesz-represented vector corresponding to the continuous linear functional obtained by fixing the first hs.length slots of the cumulant of order hs.length + 1. Thus its defining property is that pairing it with a vector $w$ yields the corresponding cumulant with $w$ in the final slot. This is a local gradient-jet construction; no additional identity is asserted by the definition.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.Cumulant.Basic
import FunctionalInequalities.Analysis.BakryEmery.Tilt.LocalDerivatives
import FunctionalInequalities.Analysis.Tensor.BasisChange
import FunctionalInequalities.Probability.Covariance.Basic
import FunctionalInequalities.Probability.Covariance.Positivity
import Mathlib.Probability.Moments.IntegrableExpMul
import Mathlib.MeasureTheory.Measure.Support
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.Calculus.Gradient.Basic
import FunctionalInequalities.Analysis.IteratedDerivative.GradientJet
import FunctionalInequalities.Analysis.IteratedDerivative.Symmetry
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Original declaration excerpt

Shown in the original module context.

noncomputable def cumulantVector (μ : Measure E) (hs : List E) : E :=
  (InnerProductSpace.toDual ℝ E).symm
    ((cumulant μ (hs.length + 1)).curryRight (fun i => hs.get i))

Module navigation

Direct project imports: Analysis/BakryEmery/Cumulant/Basic, Analysis/BakryEmery/Tilt/LocalDerivatives, Analysis/Tensor/BasisChange, Probability/Covariance/Basic, Probability/Covariance/Positivity, Analysis/IteratedDerivative/GradientJet, Analysis/IteratedDerivative/Symmetry.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.BakryEmery.Cumulant.Local · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_LocalDerivatives
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_BasisChange
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Positivity
import Mathlib.Probability.Moments.IntegrableExpMul
import Mathlib.MeasureTheory.Measure.Support
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.Calculus.Gradient.Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_GradientJet
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Symmetry
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure

open MeasureTheory Filter Topology
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Analysis
namespace BakryEmery
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
section GradientJets
/-- The Riesz vector of the last slot of the scalar cumulant of order `hs.length + 1`, the first slots being the
list `hs` (inherited order): `⟪cumulantVector μ hs, w⟫ = κ_{|hs|+1}(hs, w)`. -/
noncomputable def cumulantVector (μ : Measure E) (hs : List E) : E :=
  (InnerProductSpace.toDual ℝ E).symm
    ((cumulant μ (hs.length + 1)).curryRight (fun i => hs.get i))
end GradientJets
end BakryEmery
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Local.lean#L517-L521 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Local`, definition bundle `KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Local`; the repository is private at upload time).

View graph