Distance From Partial Symmetrization

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_sub_symField_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes BKL Lemma 3.3, Equation (44), p. 12.

Let $u$ be a field with $k$ indices and let $q\le k$ . Let $S_q u$ be the average over permutations of the first $q$ positions, and let $\tau_\ell$ swap positions $\ell$ and $\ell+1$ . Then

\|u-S_qu\|^2 \le q^4\sum_{\substack{\ell<k\\\ell+1<q}} \|u-\tau_\ell u\|^2.

The squared norm is the field quantity normSq, and the sum is over the finite set of admissible adjacent positions.

This is the combinatorial symmetrization estimate used in the approximate symmetry of Poisson iterates.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.PoissonIterate. Shown in its original module context. Proof omitted.

theorem normSq_sub_symField_le {q : ℕ} (hq : q ≤ k) (u : Field ν k) :
    normSq (u - symField q u) ≤
      (q : ℝ) ^ 4 * ∑ ℓ ∈ univ.filter (fun ℓ : Fin k => ℓ.val + 1 < q),
        normSq (u - permField (Equiv.swap ℓ (finRotate k ℓ)) u)

Module navigation

Module: KLS/BKL/PoissonIterate/Permutation.

Definition modules: KLS/BKL/PoissonIterate/Basic.

Supporting theorems: sqrt_normSq_sub_permField_le_of_adjacent.

Previous: sqrt_normSq_sub_permField_le_of_adjacent.

Source excerpt, lines 314–317 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Permutation

open MeasureTheory Finset
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {ν : MeasureTheory.ProbabilityMeasure V} {k : ℕ}

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_sub_symField_le_readable {q : ℕ} (hq : q ≤ k) (u : Field ν k) :
    normSq (u - symField q u) ≤
      (q : ℝ) ^ 4 * ∑ ℓ ∈ univ.filter (fun ℓ : Fin k => ℓ.val + 1 < q),
        normSq (u - permField (Equiv.swap ℓ (finRotate k ℓ)) u) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Permutation.lean#L311-L338 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Permutation`, declaration `FunctionalInequalities.KLS.LogConcave.PoissonIterate.normSq_sub_symField_le`; the repository is private at upload time).

View graph