Tensor Slot Bound From a Matrix Family Bound

Proved

FunctionalInequalities.Analysis.CoordinateTensor.slot_bound_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary lemma lifts a vector inequality to one tensor slot.

Let $H_i$ be a family of real $n\times n$ matrices satisfying, for every vector $v\in\mathbb R^n$ ,

\sum_i\|H_i v\|^2\le 8\|v\|^2.

Then for every order- $r$ coordinate tensor $T$ and every slot $s$ ,

\sum_i\|H_i^{(s)}T\|^2\le 8\|T\|^2.

This technical lifting result is used to control the slotwise terms in the drift estimate.

Original Lean declaration header

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

private lemma slot_bound (H : Fin n → Matrix (Fin n) (Fin n) ℝ)
    (h8 : ∀ v : Fin n → ℝ, ∑ i, ∑ a, (∑ b, H i a b * v b) ^ 2 ≤ 8 * ∑ a, v a ^ 2)
    (T : (Fin r → Fin n) → ℝ) (s : Fin r) :
    ∑ i, ∑ J, (∑ k, H i (J s) k * T (Function.update J s k)) ^ 2 ≤
      8 * ∑ J, T J ^ 2

Module navigation

Module: Analysis/Tensor/SlotAction.

Next: drift_expression_ge.

Source excerpt, lines 45–49 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_SlotAction

variable {n r : ℕ}

Formal statement

 lemma FunctionalInequalities.Analysis.CoordinateTensor.slot_bound_readable (H : Fin n → Matrix (Fin n) (Fin n) ℝ)
    (h8 : ∀ v : Fin n → ℝ, ∑ i, ∑ a, (∑ b, H i a b * v b) ^ 2 ≤ 8 * ∑ a, v a ^ 2)
    (T : (Fin r → Fin n) → ℝ) (s : Fin r) :
    ∑ i, ∑ J, (∑ k, H i (J s) k * T (Function.update J s k)) ^ 2 ≤
      8 * ∑ J, T J ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/SlotAction.lean#L45-L134 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.SlotAction`, declaration `_private.FunctionalInequalities.Analysis.Tensor.SlotAction.0.FunctionalInequalities.Analysis.CoordinateTensor.slot_bound`; the repository is private at upload time).

View graph