BKL Subset-Sum Identity

Proved

FunctionalInequalities.Analysis.Tensor.sum_norm_sq_sum_subset_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the equality in (25) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Lemma 2.2, p. 9.

Let $V$ be a real inner-product space, let $U$ be a finite set with $|U|=3d$ , and let $x_F\in V$ be assigned to every $d$ -element subset $F\subseteq U$ . Then

\sum_{\substack{E\subseteq U\\|E|=2d}} \left\|\sum_{\substack{F\subseteq E\\|F|=d}}x_F\right\|^2 = \sum_{s=0}^{d}\binom ds \sum_{\substack{S\subseteq U\\|S|=s}} \left\|\sum_{\substack{F\subseteq U,\ |F|=d\\S\subseteq F}}x_F\right\|^2.

This is the central combinatorial norm identity used in the partial symmetrization estimate.

Original Lean declaration header

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

theorem sum_norm_sq_sum_subset_eq (U : Finset α) {d : ℕ} (hU : U.card = 3 * d)
    (x : Finset α → V) :
    ∑ E ∈ U.powersetCard (2 * d), ‖∑ F ∈ E.powersetCard d, x F‖ ^ 2 =
      ∑ s ∈ range (d + 1), (d.choose s : ℝ) *
        ∑ S ∈ U.powersetCard s, ‖∑ F ∈ (U.powersetCard d).filter (S ⊆ ·), x F‖ ^ 2

Module navigation

Module: Analysis/Tensor/Symmetrization.

Supporting theorems: card_filter_union_subset, sum_choose_mul_card_filter_subset, sum_norm_sq_sum_filter.

Previous: sum_norm_sq_sum_filter · Next: sum_norm_sq_le_sum_norm_sq_sum_subset.

Source excerpt, lines 276–280 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

open Finset
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable {α : Type*} [DecidableEq α]

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_norm_sq_sum_subset_eq_readable (U : Finset α) {d : ℕ} (hU : U.card = 3 * d)
    (x : Finset α → V) :
    ∑ E ∈ U.powersetCard (2 * d), ‖∑ F ∈ E.powersetCard d, x F‖ ^ 2 =
      ∑ s ∈ range (d + 1), (d.choose s : ℝ) *
        ∑ S ∈ U.powersetCard s, ‖∑ F ∈ (U.powersetCard d).filter (S ⊆ ·), x F‖ ^ 2 := by sorry

Source

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

View graph