Multilinear Contraction in the Middle Slot

This is a finite-dimensional multilinear algebra lemma used to contract a middle tensor slot.

Let $T:(\mathbb{R}^n)^3\to\mathbb{R}$ be a continuous trilinear map, let $x,z,w\in\mathbb{R}^n$, let $v:\operatorname{Fin}(n)\to\mathbb{R}$, and let $b:\operatorname{Fin}(n)\to\mathbb{R}^n$. If

then

This auxiliary lemma records linearity in the middle argument and is used to rewrite finite sums of third-order cumulant terms.

Original Lean declaration header

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

private lemma cumulant_middle_sum
    (T : ContinuousMultilinearMap ℝ (fun _ : Fin 3 => EuclideanSpace ℝ (Fin n)) ℝ)
    (x z : EuclideanSpace ℝ (Fin n)) (v : Fin n → ℝ)
    (b : Fin n → EuclideanSpace ℝ (Fin n))
    (w : EuclideanSpace ℝ (Fin n))
    (hw : w = ∑ j, v j • b j) :
    ∑ j, T ![x, b j, z] * v j = T ![x, w, z]

Module navigation

Module: KLS/BKL/Localization/NoiseBound.

Next: cumulantEnergy_succ_eq.

Source excerpt, lines 24–30 · Frozen source 408915f.