Basis Independence of Coordinate Tensor Square Sums

Proved

FunctionalInequalities.Analysis.Tensor.sum_coordTensor_sq_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the basis-independence identity for the squared coefficient sum of a multilinear form.

Let $E$ be a real inner-product space, let $b$ and $b'$ be orthonormal bases indexed by $\operatorname{Fin}(n)$ and $\operatorname{Fin}(n')$ , respectively, and let $\Phi:E^k\to\mathbb R$ be continuous and $k$ -linear. Then

\sum_{i:\operatorname{Fin}(k)\to\operatorname{Fin}(n)}\operatorname{coordTensor}_b(\Phi)(i)^2 =\sum_{l:\operatorname{Fin}(k)\to\operatorname{Fin}(n')}\operatorname{coordTensor}_{b'}(\Phi)(l)^2.

Thus the squared coordinate-tensor norm is independent of the chosen orthonormal basis, even when the indexing types are presented with different finite cardinalities.

Original Lean declaration header

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

theorem sum_coordTensor_sq_eq {n n' k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (b' : OrthonormalBasis (Fin n') ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) :
    ∑ i : Fin k → Fin n, coordTensor b Φ i ^ 2 = ∑ l : Fin k → Fin n', coordTensor b' Φ l ^ 2

Module navigation

Module: Analysis/Tensor/BasisChange.

Definition modules: Analysis/Tensor/Coefficients.

Supporting theorems: apply_eq_sum_coordTensor.

Source excerpt, lines 70–73 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_BasisChange

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_coordTensor_sq_eq_readable {n n' k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (b' : OrthonormalBasis (Fin n') ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) :
    ∑ i : Fin k → Fin n, coordTensor b Φ i ^ 2 = ∑ l : Fin k → Fin n', coordTensor b' Φ l ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/BasisChange.lean#L68-L98 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.BasisChange`, declaration `FunctionalInequalities.Analysis.Tensor.sum_coordTensor_sq_eq`; the repository is private at upload time).

View graph