Permutation action on tensor fields

Definition

KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Permutation

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a tensor field u : Field ν k and a permutation $σ$ of Fin k, permField σ u is the field with component at $I$ equal to $u(I\circ σ)$ . The declared simp results state that this action has the displayed component formula and that the identity permutation acts trivially; the module also contains the combinatorial symmetrization bound for adjacent transpositions.

Original module imports

import FunctionalInequalities.KLS.BKL.PoissonIterate.Basic

Original declaration excerpt

Shown in the original module context.

@[simp] theorem permField_apply (σ : Equiv.Perm (Fin k)) (u : Field ν k)
    (I : Fin k → Fin (Module.finrank ℝ V)) : permField σ u I = u (I ∘ σ) := rfl

Module navigation

Direct project imports: KLS/BKL/PoissonIterate/Basic.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.PoissonIterate.Permutation · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Basic

noncomputable section
open MeasureTheory Finset
open FunctionalInequalities.Analysis.Tensor
open scoped Classical
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace PoissonIterate
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V]
  {ν : ProbabilityMeasure V} {k : ℕ}
@[simp] theorem permField_apply (σ : Equiv.Perm (Fin k)) (u : Field ν k)
    (I : Fin k → Fin (Module.finrank ℝ V)) : permField σ u I = u (I ∘ σ) := rfl
/-- The identity permutation acts trivially. -/
@[simp] theorem permField_one (u : Field ν k) : permField 1 u = u := rfl
end PoissonIterate
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Permutation.lean#L59-L63 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Permutation`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Permutation`; the repository is private at upload time).

View graph