Binomial Partial Symmetrization Bound

Let $\Omega$ be finite, let $V$ be a real inner-product space, and let $\rho$ be a permutation representation by linear isometries. Let $A,B,Q\subseteq\Omega$ and $d\in\mathbb N$ satisfy:

1. $|A|=d$ and $|B|=2d$.
2. $A$ and $B$ are disjoint.
3. $A\subseteq Q\subseteq A\cup B$.
4. $|Q|=2d$.
5. $v\in V$ is invariant under permutations fixing outside $A$ and under permutations fixing outside $B$.

Then

This is the stronger binomial-factor version of the partial symmetrization estimate.

Original Lean declaration header

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

theorem norm_le_choose_mul_norm_blockAverage (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V))
    {A B Q : Finset Ω} {d : ℕ} (hA : A.card = d) (hB : B.card = 2 * d) (hAB : Disjoint A B)
    (hAQ : A ⊆ Q) (hQ : Q ⊆ A ∪ B) (hQc : Q.card = 2 * d) (v : V)
    (hvA : ∀ σ ∈ fixingOutside A, ρ σ v = v) (hvB : ∀ σ ∈ fixingOutside B, ρ σ v = v) :
    ‖v‖ ≤ ((2 * d).choose d : ℝ) * ‖blockAverage ρ Q v‖

Module navigation

Module: Analysis/Tensor/Symmetrization.

Supporting theorems: apply_eq_of_image_eq, exists_mem_fixingOutside_image_eq, sum_fixingOutside_eq_smul_sum, sum_norm_sq_le_sum_norm_sq_sum_subset, sum_powersetCard_image_eq.

Previous: sum_powersetCard_image_eq · Next: norm_le_four_pow_mul_norm_blockAverage.

Source excerpt, lines 945–949 · Frozen source 408915f.

Literature

This formalizes Lemma 2.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 9, in orthogonal-representation form.