Unit First-Order Cumulant Energy

This auxiliary statement identifies the first-order cumulant energy on a unit vector.

Let $\mu$ be a probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ with compact support and assume that $\mu$ is isotropic. For $u$ satisfying $\|u\|=1$, the cumulantEnergy at order $1$ is

The identity is a technical base case for the cutoff-energy argument and is not itself a universal cumulant or KLS bound.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

private theorem cumulantEnergy_one_is_one
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hiso : KLS.Isotropic μ) (u : EuclideanSpace ℝ (Fin n)) (hu : ‖u‖ = 1) :
    cumulantEnergy (μ : Measure (EuclideanSpace ℝ (Fin n))) 1 u = 1

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Base.

Definition modules: KLS/BKL/CumulantEnergy/Basic, KLS/Isotropic.

Supporting theorems: cumulant_two_eq_centered_moment_of_integrable_exp, memLp_of_polynomial_bound_of_integrable_exp.

Next: cutoffEnergyClaim_one.

Source excerpt, lines 42–46 · Frozen source 408915f.