Third Cumulant Bound in Any Orthonormal Basis

This formalizes the basis-independent form of Lemma 4.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 18.

Let $\mu$ be a probability measure on a finite-dimensional real inner-product space $E$. Assume $r>0$, $e^{r\|x\|}$ is integrable, $\mu$ is centered and isotropic, and $\mu$ satisfies LetwinQuadraticBound. For any orthonormal basis $b$ indexed by $\operatorname{Fin}(m)$ and any $u\in E$,

The result transports the third-cumulant Hilbert–Schmidt estimate from the standard orthonormal basis to every orthonormal basis.

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_basis (μ : 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 μ) {m : ℕ} (b : OrthonormalBasis (Fin m) ℝ E) (u : E) :
    ∑ j, ∑ k, cumulant μ 3 ![u, b j, b k] ^ 2 ≤ 8 * ‖u‖ ^ 2

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp, sum_coordTensor_sq_eq.

Previous: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp · Next: cumulant_two_eq_centered_moment_of_integrable_exp.

Source excerpt, lines 359–364 · Frozen source 408915f.