Mixed Cumulant Entries of the Regular Suspension Joint Law

This auxiliary lemma states the mixed-cumulant entry identity corresponding to BKL equation (112).

Let $n,N\in\mathbb N$ with $N>0$ and $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)). Let $h_V:$ RegularPotential $V\ a\ b'$: $a,b'>0$, $V$ is smooth with derivatives of polynomial growth, and $a\operatorname{Id}\le D^2V\le b'\operatorname{Id}$. Put $\mu=h_V.\text{law}$, the normalized $e^{-V}$ law. Assume:

1. $\beta>0$, $f:E\to\mathbb R$ is $C^2$, and $\|D(Df)(x)\|\le M$ for every $x$.
2. $(\beta/\sqrt N)M\le a$.

Set $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma) and $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$ on $H=$ JointSpace $N\ n$. Let $e_0,e_{(i,j)}$ be its scalar and copy-coordinate unit vectors, and $(b_j)$ the standard basis of $E$. For every natural $d\ge1$, $I:\operatorname{Fin}d\to\operatorname{Fin}N$, and $J:\operatorname{Fin}d\to\operatorname{Fin}n$,

Here $\kappa_{d+1}^{\lambda}$ is cumulant and $T_d^\mu f$ is taylorTensor. The identity retains repeated spatial slots and supplies the entry data for cumulant norm estimates. Neither isotropy of $\mu$ nor centering or unit variance of $f$ is assumed.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.Suspension. Shown in its original module context. Proof omitted.

private theorem source_mixed_cumulant_entries {n N : ℕ} (hN : 0 < N)
    (V : EuclideanSpace ℝ (Fin n) → ℝ) {a b' : ℝ} (hV : KLS.RegularPotential V a b')
    {f : EuclideanSpace ℝ (Fin n) → ℝ} {M β : ℝ} (hβ : 0 < β)
    (hf : ContDiff ℝ 2 f) (hfM : ∀ x, ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ M)
    (h110 : β / Real.sqrt N * M ≤ a)
    {d : ℕ} (hd : 1 ≤ d) (I : Fin d → Fin N) (J : Fin d → Fin n) :
    cumulant (jointLaw (hV.law : Measure _) f β (sigma β) N) (d + 1)
      (Fin.cons (EuclideanSpace.single none 1)
        (fun k => EuclideanSpace.single (some (I k, J k)) 1)) =
      if ∀ k k', I k = I k' then
        (d.factorial : ℝ) / (sigma β * Real.sqrt N) *
          taylorTensor (hV.law : Measure _) f d
            (fun k => EuclideanSpace.basisFun (Fin n) ℝ (J k)) else 0

Module navigation

Module: KLS/BKL/Suspension/Derivatives.

Definition modules: KLS/BKL/Suspension/Law, Analysis/BakryEmery/Tilt/Basic, KLS/LogConcave/Regular/Basic, Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: contDiffOn_logLaplace_ball, exists_integrable_exp_norm, fderiv_logLaplace_jointLaw_none, jointLaw_eq_tilted, logConcave_jointLaw_of_eq_tilted.

Previous: fderiv_logLaplace_jointLaw_none.

Source excerpt, lines 713–725 · Frozen source 408915f.