Grouped Cumulant Expansion for Inverse Covariance

This formalizes the grouped expansion in Equations (72)–(74) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited for the spatial step of Lemma 4.3.

Let $\mu$ be a compactly supported probability measure on a finite-dimensional real inner-product space $E$. Assume the covariance operator $A=\operatorname{Cov}(\mu)$ is invertible. For $m\ge3$, directions $h:\operatorname{Fin}(m)\to E$, and a fixed index $i_0\in\operatorname{Fin}(m)$, define $v(z)=\nabla\Lambda_\mu(z)-\nabla\Lambda_\mu(0)$. Then

The singleton and complementary-singleton allocations contribute $2m\,\kappa_m(h)$, while the remaining allocations are paired by complementation. This is a deterministic fixed-measure identity, not a stochastic evolution statement.

Original Lean declaration header

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

theorem iteratedFDeriv_inner_centeredGradient_zero_grouped_of_compact
    (mu : ProbabilityMeasure E)
    (hc : IsCompact (mu : Measure E).support)
    (hA : IsUnit (Covariance.operator (mu : Measure E)))
    {m : ℕ} (hm : 3 ≤ m) (h : Fin m → E) (i0 : Fin m) :
    iteratedFDeriv ℝ m (fun z : E =>
        ⟪gradient (logLaplace (mu : Measure E)) z - gradient (logLaplace (mu : Measure E)) 0,
          Ring.inverse (Covariance.operator (mu : Measure E))
            (gradient (logLaplace (mu : Measure E)) z -
              gradient (logLaplace (mu : Measure E)) 0)⟫) 0 h =
      (2 * (m : ℝ)) * cumulant (mu : Measure E) m h +
        2 * ∑ q ∈ Finset.univ.filter (fun q : Fin m → Bool =>
          q i0 = true ∧
          2 ≤ (selected h q).length ∧
          2 ≤ (selected h (fun i => !(q i))).length),
          ⟪cumulantVector (mu : Measure E) (selected h q),
            Ring.inverse (Covariance.operator (mu : Measure E))
              (cumulantVector (mu : Measure E)
                (selected h (fun i => !(q i))))⟫

Module navigation

Module: Analysis/BakryEmery/Cumulant/Leibniz.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, Probability/Covariance/Basic, Analysis/BakryEmery/Cumulant/Local, Analysis/IteratedDerivative/Bilinear.

Supporting theorems: inner_cumulantVector_single_ringInverse_cumulantVector, iteratedFDeriv_inner_centeredGradient_zero_of_compact, selected_mask_partition, sum_filter_eq_two_mul_sum_filter_of_compl_invariant.

Previous: iteratedFDeriv_inner_centeredGradient_zero_of_compact.

Source excerpt, lines 153–171 · Frozen source 408915f.