Four-Power Coordinate Tensor Symmetrization Bound

Let $n,k,d\in\mathbb N$ with $3d\le k$, and let $A$ be a tensor in Coord n k, equivalently a real Hilbert–Schmidt tensor with $k$ index positions over $\operatorname{Fin}(n)$. Assume:

1. $A$ is invariant under permutations fixing every position outside the first $d$ slots.
2. $A$ is invariant under permutations fixing every position outside slots $d$ through $3d-1$.

Then

The estimate leaves all positions after the first $3d$ untouched and allows $n=0$; the type itself does not require $d>0$.

Original Lean declaration header

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

theorem norm_le_four_pow_mul_norm_symmetrize {n k d : ℕ} (hk : 3 * d ≤ k) (A : Coord n k)
    (h₁ : ∀ σ ∈ fixingOutside (slots k 0 d), slotRep n k σ A = A)
    (h₂ : ∀ σ ∈ fixingOutside (slots k d (3 * d)), slotRep n k σ A = A) :
    ‖A‖ ≤ (4 : ℝ) ^ d * ‖symmetrize n k (2 * d) A‖

Module navigation

Module: Analysis/Tensor/Coordinate.

Definition modules: Analysis/Tensor/Symmetrization.

Supporting theorems: card_slots, norm_le_four_pow_mul_norm_blockAverage.

Previous: card_slots · Next: sum_sq_blocks_le.

Source excerpt, lines 88–91 · Frozen source 408915f.

Literature

This formalizes Lemma 2.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 9.