Prove2Me

Cumulant Invariance Under Linear Isometries

Proved
FunctionalInequalities.Analysis.BakryEmery.cumulant_map_linearIsometryEquiv_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the invariance of cumulants under a linear isometric equivalence.

Let EE and FF be complete finite-dimensional real inner-product spaces with Borel structures. Let φ:E→F\varphi:E\to F be a linear isometry equivalence, let ν\nu be any measure on EE, let k∈Nk\in\mathbb N, and let u:Fin(k)→Eu:\mathrm{Fin}(k)\to E. Then

κkφ#ν(φu1,…,φuk)=κkν(u1,…,uk).\kappa_k^{\varphi_\#\nu} \bigl(\varphi u_1,\ldots,\varphi u_k\bigr) = \kappa_k^\nu(u_1,\ldots,u_k).

The pushforward is ν.map φ. No finiteness, nonzero, or exponential-moment assumption appears in the theorem type. This provides a reusable coordinate-invariance property for cumulant tensors.

Original Lean declaration header

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

theorem cumulant_map_linearIsometryEquiv [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
    (φ : E ≃ₗᵢ[ℝ] F) (ν : Measure E) (k : ℕ) (u : Fin k → E) :
    cumulant (ν.map φ) k (fun i => φ (u i)) = cumulant ν k u

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Previous: contDiffOn_logLaplace_ball · Next: cumulant_map_affine.

Source excerpt, lines 813–817 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Basic

open MeasureTheory
universe u
variable {E F : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.cumulant_map_linearIsometryEquiv_readable [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
    (φ : E ≃ₗᵢ[ℝ] F) (ν : Measure E) (k : ℕ) (u : Fin k → E) :
    cumulant (ν.map φ) k (fun i => φ (u i)) = cumulant ν k u := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Basic.lean#L811-L855 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.cumulant_map_linearIsometryEquiv`; the repository is private at upload time).

View graph