Coordinate tensors and matrix slot actions

Definition

KLSModular_FunctionalInequalities_Analysis_Tensor_SlotAction

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

An order- $r$ coordinate tensor is represented as a function $(\mathrm{Fin}\,r\to\mathrm{Fin}\,n)\to\mathbb{R}$ . inner T S is its Euclidean coordinate inner product $\sum_J T_JS_J$ ; actOn H s T applies a matrix $H$ to the $s$ -th tensor input, and actSum H T sums this action over all slots. These definitions use Function.update to preserve every tensor index except the selected one.

Original module imports

import Mathlib

Original declaration excerpt

Shown in the original module context.

def inner (T S : (Fin r → Fin n) → ℝ) : ℝ := ∑ J, T J * S J

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Tensor.SlotAction · Frozen source 408915f.

Definition code

import Mathlib

noncomputable section
open Matrix
namespace FunctionalInequalities
namespace Analysis
namespace CoordinateTensor
variable {n r : ℕ}
/-- The Euclidean inner product of two order-`r` coordinate tensors on `ℝⁿ`. -/
def inner (T S : (Fin r → Fin n) → ℝ) : ℝ := ∑ J, T J * S J
/-- `H^{(s)}`: the matrix `H` acting on the `s`-th input of an order-`r` tensor (BKL arXiv:2610.05474v1, p. 23). -/
def actOn (H : Matrix (Fin n) (Fin n) ℝ) (s : Fin r) (T : (Fin r → Fin n) → ℝ) : (Fin r → Fin n) → ℝ :=
  fun J => ∑ k, H (J s) k * T (Function.update J s k)
/-- `Σ_H = Σ_s H^{(s)}`. -/
def actSum (H : Matrix (Fin n) (Fin n) ℝ) (T : (Fin r → Fin n) → ℝ) : (Fin r → Fin n) → ℝ :=
  fun J => ∑ s, actOn H s T J
end CoordinateTensor
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/SlotAction.lean#L19-L28 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.SlotAction`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Tensor_SlotAction`; the repository is private at upload time).

View graph