Permutation Displacement From Adjacent Displacements

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.sqrt_normSq_sub_permField_le_of_adjacent_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $u$ be a field with $k$ index positions and let $q\le k$ . Suppose $B\ge0$ and every adjacent transposition of positions $\ell$ and $\ell+1$ with $\ell+1<q$ moves $u$ by at most $B$ in Hilbert–Schmidt norm:

\sqrt{\|u-\tau_\ell u\|^2}\le B.

Then every permutation $\sigma$ that fixes all positions outside the first $q$ positions satisfies

\sqrt{\|u-\sigma u\|^2}\le q^2B.

The result is purely combinatorial and applies to arbitrary fields of $L^2$ classes; it does not use properties of the measure.

Original Lean declaration header

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

theorem sqrt_normSq_sub_permField_le_of_adjacent {q : ℕ} (hq : q ≤ k) (u : Field ν k) {B : ℝ}
    (hB0 : 0 ≤ B)
    (hB : ∀ ℓ : Fin k, ℓ.val + 1 < q →
      √(normSq (u - permField (Equiv.swap ℓ (finRotate k ℓ)) u)) ≤ B)
    {σ : Equiv.Perm (Fin k)} (hσ : σ ∈ fixingOutside (slots k 0 q)) :
    √(normSq (u - permField σ u)) ≤ (q : ℝ) ^ 2 * B

Module navigation

Module: KLS/BKL/PoissonIterate/Permutation.

Definition modules: KLS/BKL/PoissonIterate/Basic, Analysis/Tensor/Coordinate, Analysis/Tensor/Symmetrization.

Next: normSq_sub_symField_le.

Source excerpt, lines 223–228 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Permutation

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

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.sqrt_normSq_sub_permField_le_of_adjacent_readable {q : ℕ} (hq : q ≤ k) (u : Field ν k) {B : ℝ}
    (hB0 : 0 ≤ B)
    (hB : ∀ ℓ : Fin k, ℓ.val + 1 < q →
      √(normSq (u - permField (Equiv.swap ℓ (finRotate k ℓ)) u)) ≤ B)
    {σ : Equiv.Perm (Fin k)} (hσ : σ ∈ fixingOutside (slots k 0 q)) :
    √(normSq (u - permField σ u)) ≤ (q : ℝ) ^ 2 * B := by sorry

Source

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

View graph