Coordinate coefficients of multilinear maps

Definition

KLSModular_FunctionalInequalities_Analysis_Tensor_Coefficients

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Given an orthonormal basis $b$ of an $n$ -dimensional real inner-product space $E$ and a continuous real $k$ -linear map $\Phi$ , coordTensor b Φ is the element of Coord n k whose coordinate at $(i_1,\ldots,i_k)$ is $\Phi(b(i_1),\ldots,b(i_k))$ . It packages the coefficient array of the multilinear map in the chosen basis; no additional equality or norm theorem is declared in this bundle.

Original module imports

import FunctionalInequalities.Analysis.Tensor.Coordinate
import FunctionalInequalities.Analysis.Tensor.Multilinear

Original declaration excerpt

Shown in the original module context.

def coordTensor {n k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) : Coord n k :=
  WithLp.toLp 2 fun i => Φ (fun j => b (i j))

Module navigation

Direct project imports: Analysis/Tensor/Coordinate, Analysis/Tensor/Multilinear.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Coordinate
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Multilinear

noncomputable section
open Finset
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Analysis
namespace Tensor
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- The coefficient array `(Φ (b i₁, …, b i_k))_i` of a real `k`-linear map in an orthonormal
basis `b`. -/
def coordTensor {n k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) : Coord n k :=
  WithLp.toLp 2 fun i => Φ (fun j => b (i j))
end Tensor
end Analysis
end FunctionalInequalities

Source

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

View graph