Permutation averages on selected tensor positions

Definition

KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a finite index type $\Omega$ , fixingOutside s is the finite set of permutations that fix every point outside a finite subset $s$ . Given a monoid representation ρ of permutations by linear isometric equivalences of an inner-product space, blockAverage ρ s v is the normalized average of ρ σ v over those permutations, using the real inverse of the cardinality. This bundle contains definitions only and asserts no norm estimate.

Original module imports

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Operator.LinearIsometry
import Mathlib.Data.Nat.Choose.Central
import Mathlib.Data.Nat.Choose.Vandermonde
import Mathlib.GroupTheory.Perm.Basic
import Mathlib.Data.Fintype.Perm

Original declaration excerpt

Shown in the original module context.

def fixingOutside (s : Finset Ω) : Finset (Equiv.Perm Ω) :=
  univ.filter fun σ => ∀ x, x ∉ s → σ x = x

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Tensor.Symmetrization · Frozen source 408915f.

Definition code

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Operator.LinearIsometry
import Mathlib.Data.Nat.Choose.Central
import Mathlib.Data.Nat.Choose.Vandermonde
import Mathlib.GroupTheory.Perm.Basic
import Mathlib.Data.Fintype.Perm

noncomputable section
open Finset
namespace FunctionalInequalities
namespace Analysis
namespace Tensor
variable {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
/-- The permutations of `Ω` fixing every point outside `s`. -/
def fixingOutside (s : Finset Ω) : Finset (Equiv.Perm Ω) :=
  univ.filter fun σ => ∀ x, x ∉ s → σ x = x
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
/-- The average of `ρ σ v` over the permutations fixing every point outside `s` (the operator
`S_q` of the source when `s` is the set of the first `q` positions). -/
def blockAverage (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) (s : Finset Ω) (v : V) : V :=
  ((fixingOutside s).card : ℝ)⁻¹ • ∑ σ ∈ fixingOutside s, ρ σ v
end Tensor
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/Symmetrization.lean#L33-L42 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.Symmetrization`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization`; the repository is private at upload time).

View graph