Squared Norm Expansion for Filtered Finite Sums

Proved

FunctionalInequalities.Analysis.Tensor.sum_norm_sq_sum_filter_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite-dimensional inner-product expansion.

Let $V$ be a real inner-product space, let $\mathcal E$ and $P$ be finite sets, let $r(F,E)$ be a decidable relation between $F\in P$ and $E\in\mathcal E$ , and let $x_F\in V$ . Then

\sum_{E\in\mathcal E}\left\|\sum_{\substack{F\in P\\r(F,E)}}x_F\right\|^2 = \sum_{F,F'\in P} \#\{E\in\mathcal E:r(F,E)\land r(F',E) \}\,\langle x_F,x_{F'}\rangle.

This identity is a reusable way to expand sums of squared norms while retaining the multiplicity of common filters.

Original Lean declaration header

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

theorem sum_norm_sq_sum_filter {β ι : Type*} (𝓔 : Finset β) (P : Finset ι) (r : ι → β → Prop)
    [∀ F E, Decidable (r F E)] (x : ι → V) :
    ∑ E ∈ 𝓔, ‖∑ F ∈ P.filter (fun F => r F E), x F‖ ^ 2 =
      ∑ F ∈ P, ∑ F' ∈ P, ((𝓔.filter fun E => r F E ∧ r F' E).card : ℝ) * inner ℝ (x F) (x F')

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: sum_choose_mul_card_filter_subset · Next: sum_norm_sq_sum_subset_eq.

Source excerpt, lines 222–225 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Symmetrization

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

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_norm_sq_sum_filter_readable {β ι : Type*} (𝓔 : Finset β) (P : Finset ι) (r : ι → β → Prop)
    [∀ F E, Decidable (r F E)] (x : ι → V) :
    ∑ E ∈ 𝓔, ‖∑ F ∈ P.filter (fun F => r F E), x F‖ ^ 2 =
      ∑ F ∈ P, ∑ F' ∈ P, ((𝓔.filter fun E => r F E ∧ r F' E).card : ℝ) * inner ℝ (x F) (x F') := by sorry

Source

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

View graph