Cumulant Energy in Conjugated Coordinates

This statement expresses cumulant energy as a coordinate energy form, corresponding to the conjugation identities (83) and (85) of the Bizeul–Klartag–Lehec framework.

Let $\nu$ be a measure on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ whose covariance operator $A$ is positive and invertible. Let $P$ be a self-adjoint invertible continuous linear map. For every $r\in\mathbb{N}$ and $u$, one has

Here $e_j$ is the standard basis and energyForm is the coordinate-tensor quadratic form. The identity is a finite-dimensional change-of-coordinates formula for cumulant energies.

Original Lean declaration header

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

theorem cumulantEnergy_eq_energyForm (ν : Measure (EuclideanSpace ℝ (Fin n)))
    (hpos : (Covariance.operator ν).IsPositive) (hunit : IsUnit (Covariance.operator ν))
    (P : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (hP : IsSelfAdjoint P) (hPu : IsUnit P)
    (r : ℕ) (u : EuclideanSpace ℝ (Fin n)) :
    cumulantEnergy ν r u =
      energyForm (P * Covariance.operator ν * P)
        (fun K : Fin r → Fin n => cumulant ν (r + 1) (Fin.cons u fun s => P (EuclideanSpace.basisFun (Fin n) ℝ (K s))))

Module navigation

Module: KLS/BKL/CumulantEnergy/Conjugation.

Definition modules: Analysis/Tensor/EnergyForm, KLS/BKL/CumulantEnergy/Basic, Probability/Covariance/Basic, Analysis/BakryEmery/Cumulant/Basic.

Source excerpt, lines 105–111 · Frozen source 408915f.