Grouping Supported Permutation Sums by Block Images

Proved

FunctionalInequalities.Analysis.Tensor.sum_fixingOutside_eq_smul_sum_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a block-sum identity used in partial symmetrization.

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$ satisfy $A\subseteq Q\subseteq A\cup B$ . For $v\in V$ and a function $T$ on finite subsets, assume that for every permutation $\sigma$ fixing outside $A\cup B$ ,

\rho(\sigma)v=T(\sigma(A)).

Then

\sum_{\sigma\text{ fixing outside }Q}\rho(\sigma)v =\frac{\#\{\sigma\text{ fixing outside }Q\}}{\binom{|Q|}{|A|}} \sum_{\substack{F\subseteq Q\\|F|=|A|}}T(F).

The identity converts a permutation sum into a sum over subsets, with the common fiber size accounted for by the scalar factor.

Original Lean declaration header

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

theorem sum_fixingOutside_eq_smul_sum (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) {A B Q : Finset Ω}
    (hAQ : A ⊆ Q) (hQ : Q ⊆ A ∪ B) (v : V) (T : Finset Ω → V)
    (hT : ∀ σ ∈ fixingOutside (A ∪ B), ρ σ v = T (A.image σ)) :
    ∑ σ ∈ fixingOutside Q, ρ σ v =
      (((fixingOutside Q).card : ℝ) / (Q.card.choose A.card : ℝ)) •
        ∑ F ∈ Q.powersetCard A.card, T F

Module navigation

Module: Analysis/Tensor/Symmetrization.

Supporting theorems: card_fiber_eq, image_mem_powersetCard_of_mem_fixingOutside.

Previous: card_fiber_eq · Next: sum_powersetCard_image_eq.

Source excerpt, lines 809–814 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

variable {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_fixingOutside_eq_smul_sum_readable (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) {A B Q : Finset Ω}
    (hAQ : A ⊆ Q) (hQ : Q ⊆ A ∪ B) (v : V) (T : Finset Ω → V)
    (hT : ∀ σ ∈ fixingOutside (A ∪ B), ρ σ v = T (A.image σ)) :
    ∑ σ ∈ fixingOutside Q, ρ σ v =
      (((fixingOutside Q).card : ℝ) / (Q.card.choose A.card : ℝ)) •
        ∑ F ∈ Q.powersetCard A.card, T F := by sorry

Source

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

View graph