Prove2Me

Orthonormal Basis Expansion of a Multilinear Form

Proved
FunctionalInequalities.Analysis.Tensor.apply_eq_sum_coordTensor_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the coordinate expansion of a real continuous multilinear form.

Let EE be a real inner-product space, let bb be an orthonormal basis indexed by Fin⁡(n)\operatorname{Fin}(n), let Φ:Ek→R\Phi:E^k\to\mathbb R be a continuous kk-linear map, and let h0,…,hk−1∈Eh_0,\ldots,h_{k-1}\in E. Then

Φ(h0,…,hk−1)=∑i:Fin⁡(k)→Fin⁡(n)coordTensor⁡b(Φ)(i)∏j=0k−1⟨b(ij),hj⟩.\Phi(h_0,\ldots,h_{k-1}) =\sum_{i:\operatorname{Fin}(k)\to\operatorname{Fin}(n)}\operatorname{coordTensor}_b(\Phi)(i)\prod_{j=0}^{k-1}\langle b(i_j),h_j\rangle.

The formula expresses a multilinear form through its coordinate tensor in an orthonormal basis.

Original Lean declaration header

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

theorem apply_eq_sum_coordTensor {n k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) (h : Fin k → E) :
    Φ h = ∑ i : Fin k → Fin n, coordTensor b Φ i * ∏ j, ⟪b (i j), h j⟫

Module navigation

Module: Analysis/Tensor/Coefficients.

Next: norm_coordTensor_le.

Source excerpt, lines 108–110 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Coefficients

open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
Formal statement

theorem FunctionalInequalities.Analysis.Tensor.apply_eq_sum_coordTensor_readable {n k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) (h : Fin k → E) :
    Φ h = ∑ i : Fin k → Fin n, coordTensor b Φ i * ∏ j, ⟪b (i j), h j⟫ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/Coefficients.lean#L107-L125 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.Coefficients`, declaration `FunctionalInequalities.Analysis.Tensor.apply_eq_sum_coordTensor`; the repository is private at upload time).

View graph