Third Cumulant Contraction Bound

This is the local-moment form of Lemma 4.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $\mu$ be a probability measure on a finite-dimensional real inner-product space $E$. Assume:

1. $r>0$ and $e^{r\|x\|}$ is integrable with respect to $\mu$.
2. $\mu$ is centered: $\int\langle v,x\rangle\,d\mu(x)=0$ for every $v\in E$.
3. $\mu$ is isotropic: $\int\langle v,x\rangle\langle w,x\rangle\,d\mu(x)=\langle v,w\rangle$.
4. $\mu$ satisfies LetwinQuadraticBound.

Then for every $u\in E$, with $e_j$ the standard orthonormal basis,

This is the Hilbert–Schmidt contraction estimate for the third cumulant under the stated local exponential-moment assumptions.

Original Lean declaration header

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

theorem sum_sq_cumulant_three_le_of_letwin_of_integrable_exp (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (hc : ∀ v : E, ∫ x, ⟪v, x⟫ ∂μ = 0)
    (hiso : ∀ v w : E, ∫ x, ⟪v, x⟫ * ⟪w, x⟫ ∂μ = ⟪v, w⟫) (hL : LetwinQuadraticBound μ) (u : E) :
    ∑ j, ∑ k, cumulant μ 3 ![u, stdOrthonormalBasis ℝ E j, stdOrthonormalBasis ℝ E k] ^ 2 ≤
      8 * ‖u‖ ^ 2

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: cumulant_three_eq_integral_of_integrable_exp, memLp_of_polynomial_bound_of_integrable_exp.

Previous: memLp_of_polynomial_bound_of_integrable_exp · Next: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp_basis.

Source excerpt, lines 232–236 · Frozen source 408915f.