Coordinate Tensor Norm Bound

This theorem bounds the coordinate-array norm of a multilinear map in an orthonormal basis.

Let $E$ be a real inner-product space, let $n,k\in\mathbb N$, let $b$ be an orthonormal basis indexed by $\operatorname{Fin}(n)$, and let $\Phi:E^k\to\mathbb R$ be a continuous $k$-linear map. Then its coordinate tensor satisfies

Here coordTensor is the coefficient array obtained by evaluating $\Phi$ on basis vectors, while $\|\Phi\|$ is the continuous multilinear operator norm. The estimate is a dimension-dependent bridge from operator norms to coordinate Hilbert-space norms.

Original Lean declaration header

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

theorem norm_coordTensor_le {n k : ℕ} (b : OrthonormalBasis (Fin n) ℝ E)
    (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin k => E) ℝ) :
    ‖coordTensor b Φ‖ ≤ Real.sqrt n ^ k * ‖Φ‖

Module navigation

Module: Analysis/Tensor/Coefficients.

Definition modules: Analysis/Tensor/Coordinate.

Previous: apply_eq_sum_coordTensor.

Source excerpt, lines 181–183 · Frozen source 408915f.