Directional Cumulants of the Centered Log-Laplace Gradient

This is a finite-dimensional directional-derivative identity for a centered log-Laplace gradient.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, and let $\mu$ be a compactly supported probability measure on $E$. For every finite list $l$ of vectors in $E$, set $\Lambda=\log\operatorname{Laplace}(\mu)$. The directional derivative indexed by $l$ of $z\mapsto\nabla\Lambda(z)-\nabla\Lambda(0)$ at $0$ is zero when $l$ is empty, and otherwise is the cumulant vector associated with $l$:

This result packages the corresponding iterated-derivative identity in list form for reuse in multilinear expansions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem directional_centeredGradient_logLaplace_zero_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (l : List E) :
    directional l (fun z : E =>
        gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0) 0 =
      if l = [] then 0 else cumulantVector (μ : Measure E) l

Module navigation

Module: Analysis/BakryEmery/Cumulant/Leibniz.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, Analysis/BakryEmery/Cumulant/Local, Analysis/IteratedDerivative/Symmetry.

Supporting theorems: iteratedFDeriv_centeredGradient_logLaplace_zero_of_compact.

Next: iteratedFDeriv_inner_centeredGradient_zero_of_compact.

Source excerpt, lines 30–34 · Frozen source 408915f.