Cumulant Vectors from Centered Log-Laplace Derivatives

This is a finite-dimensional identity for the derivatives of 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 probability measure on $E$ whose support is compact. For every integer $r\ge 1$ and every map $h:\operatorname{Fin}(r)\to E$, define $\Lambda=\log\operatorname{Laplace}(\mu)$. Then the $r$-th iterated derivative at $0$ of the map $z\mapsto\nabla\Lambda(z)-\nabla\Lambda(0)$, applied to $h$, equals the cumulant Riesz vector associated with the list of directions represented by $h$.

Here iteratedFDeriv is the iterated Fréchet derivative and cumulantVector is the Riesz vector associated with the corresponding cumulant functional. The result is a technical bridge between derivatives of the log-Laplace transform and cumulant tensors.

Original Lean declaration header

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

theorem iteratedFDeriv_centeredGradient_logLaplace_zero_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (r : ℕ) (hr : 1 ≤ r) (h : Fin r → E) :
    iteratedFDeriv ℝ r (fun z : E =>
      gradient (logLaplace (μ : Measure E)) z - gradient (logLaplace (μ : Measure E)) 0) 0 h =
      cumulantVector (μ : Measure E) (List.ofFn h)

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: inner_iteratedFDeriv_gradient_apply, iteratedFDeriv_sub_const_of_pos.

Previous: cumulant_two_eq_centered_moment_of_integrable_exp · Next: inner_cumulantVector_single_ringInverse_cumulantVector.

Source excerpt, lines 608–612 · Frozen source 408915f.