Prove2Me

Expansion of the Squared Slot-Sum Action

Proved
FunctionalInequalities.Analysis.CoordinateTensor.inner_actSum_actSum_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement expands the inner product of a coordinate tensor with its summed slot action.

Let MM be a symmetric real n×nn\times n matrix and let T:(Fin⁡(r)→Fin⁡(n))→RT:(\operatorname{Fin}(r)\to\operatorname{Fin}(n))\to\mathbb R. Then

⟨ΣMT,ΣMT⟩=∑s⟨M(s)T,M(s)T⟩+∑s∑t∈Fin⁡(r)∖{s}⟨T,M(s)(M(t)T)⟩,\begin{aligned} \langle \Sigma_M T,\Sigma_M T\rangle &=\sum_s\langle M^{(s)}T,M^{(s)}T\rangle\\ &\quad+\sum_s\sum_{t\in\operatorname{Fin}(r)\setminus\{s\}} \langle T,M^{(s)}(M^{(t)}T)\rangle, \end{aligned}

where ΣMT=∑sM(s)T\Sigma_M T=\sum_s M^{(s)}T, implemented by actSum. This is the diagonal/off-diagonal decomposition used in the coordinate-tensor drift algebra.

Original Lean declaration header

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

theorem inner_actSum_actSum (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.IsSymm) (T : (Fin r → Fin n) → ℝ) :
    inner (actSum M T) (actSum M T) =
      ∑ s, inner (actOn M s T) (actOn M s T) +
        ∑ s, ∑ t ∈ Finset.univ.erase s, inner T (actOn M s (actOn M t T))

Module navigation

Module: Analysis/Tensor/SlotAction.

Supporting theorems: inner_actOn_left.

Previous: inner_actOn_left.

Source excerpt, lines 412–415 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_SlotAction

variable {n r : ℕ}
Formal statement

theorem FunctionalInequalities.Analysis.CoordinateTensor.inner_actSum_actSum_readable (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.IsSymm) (T : (Fin r → Fin n) → ℝ) :
    inner (actSum M T) (actSum M T) =
      ∑ s, inner (actOn M s T) (actOn M s T) +
        ∑ s, ∑ t ∈ Finset.univ.erase s, inner T (actOn M s (actOn M t T)) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/SlotAction.lean#L411-L459 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.SlotAction`, declaration `FunctionalInequalities.Analysis.CoordinateTensor.inner_actSum_actSum`; the repository is private at upload time).

View graph