Equivariance of Subset Sums

Proved

FunctionalInequalities.Analysis.Tensor.sum_powersetCard_image_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an equivariance identity for subset sums.

Let $\Omega$ be a type, let $V$ be a real inner-product space, let $\rho$ be a permutation representation by linear isometries, let $g$ be a permutation, and let $T$ assign a vector $T(F)$ to each finite subset $F$ . Assume

\rho(g)T(F)=T(g(F))

for every finite subset $F$ . Then for every finite subset $Q$ and natural number $k$ ,

\sum_{\substack{F\subseteq g(Q)\\|F|=k}}T(F) =\rho(g)\left(\sum_{\substack{F\subseteq Q\\|F|=k}}T(F)\right).

The result permits subset sums over different blocks to be compared by applying a representing permutation.

Original Lean declaration header

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

theorem sum_powersetCard_image_eq (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) (g : Equiv.Perm Ω)
    (T : Finset Ω → V) (hT : ∀ F, ρ g (T F) = T (F.image g)) (Q : Finset Ω) (k : ℕ) :
    ∑ F ∈ (Q.image g).powersetCard k, T F = ρ g (∑ F ∈ Q.powersetCard k, T F)

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: sum_fixingOutside_eq_smul_sum · Next: norm_le_choose_mul_norm_blockAverage.

Source excerpt, lines 910–912 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

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

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_powersetCard_image_eq_readable (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) (g : Equiv.Perm Ω)
    (T : Finset Ω → V) (hT : ∀ F, ρ g (T F) = T (F.image g)) (Q : Finset Ω) (k : ℕ) :
    ∑ F ∈ (Q.image g).powersetCard k, T F = ρ g (∑ F ∈ Q.powersetCard k, T F) := by sorry

Source

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

View graph