Subset-Sum Norm Inequality

Proved

FunctionalInequalities.Analysis.Tensor.sum_norm_sq_le_sum_norm_sq_sum_subset_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the inequality form of the BKL subset-sum estimate.

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

\sum_{\substack{F\subseteq U\\|F|=d}}\|x_F\|^2 \le \sum_{\substack{E\subseteq U\\|E|=2d}} \left\|\sum_{\substack{F\subseteq E\\|F|=d}}x_F\right\|^2.

This inequality is the norm estimate extracted from the exact subset-sum identity and is used in the representation-theoretic symmetrization bound.

Original Lean declaration header

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

theorem sum_norm_sq_le_sum_norm_sq_sum_subset (U : Finset α) {d : ℕ} (hU : U.card = 3 * d)
    (x : Finset α → V) :
    ∑ F ∈ U.powersetCard d, ‖x F‖ ^ 2 ≤
      ∑ E ∈ U.powersetCard (2 * d), ‖∑ F ∈ E.powersetCard d, x F‖ ^ 2

Module navigation

Module: Analysis/Tensor/Symmetrization.

Supporting theorems: sum_norm_sq_sum_subset_eq.

Previous: sum_norm_sq_sum_subset_eq · Next: exists_mem_fixingOutside_image_eq.

Source excerpt, lines 401–404 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

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

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_norm_sq_le_sum_norm_sq_sum_subset_readable (U : Finset α) {d : ℕ} (hU : U.card = 3 * d)
    (x : Finset α → V) :
    ∑ F ∈ U.powersetCard d, ‖x F‖ ^ 2 ≤
      ∑ E ∈ U.powersetCard (2 * d), ‖∑ F ∈ E.powersetCard d, x F‖ ^ 2 := by sorry

Source

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

View graph