Prove2Me

Total mass of the additive convolution is ∣X∣∣Y∣|X||Y|

Proved
Finset.sum_addConvolution_eq_card_product

by mysticflounder · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsadditive-energybalog-szemeredi-gowersdouble-counting

Let GG be an additive commutative group and let X,Y⊆GX, Y \subseteq G be finite sets. With rX,Y(s)=X.addConvolution Y sr_{X,Y}(s) = X.\mathrm{addConvolution}\, Y\, s the number of representations s=x+ys = x + y with x∈Xx \in X and y∈Yy \in Y, one has

∑s∈X+YrX,Y(s)=∣X∣ ∣Y∣.\sum_{s \in X + Y} r_{X,Y}(s) = |X|\,|Y|.

Every pair (x,y)∈X×Y(x,y) \in X \times Y contributes exactly one to the fibre over its sum x+yx + y, and every such sum lies in X+YX + Y, so the fibres of (x,y)↦x+y(x,y) \mapsto x+y partition X×YX \times Y.

This elementary total-mass identity underpins the energy-to-graph step in two places. It bounds the contribution of the unpopular fibres to the energy, so that large energy forces many popular pairs. And it bounds the number of popular sums by a threshold (Markov) argument: if S⊆X+YS \subseteq X + Y and every s∈Ss \in S has rX,Y(s)≥θr_{X,Y}(s) \ge \theta, then

θ ∣S∣ ≤ ∑s∈SrX,Y(s) ≤ ∑s∈X+YrX,Y(s) = ∣X∣ ∣Y∣,\theta\,|S| \ \le\ \sum_{s \in S} r_{X,Y}(s) \ \le\ \sum_{s \in X+Y} r_{X,Y}(s) \ =\ |X|\,|Y|,

so ∣S∣≤∣X∣∣Y∣/θ|S| \le |X||Y|/\theta. That second bound is total mass plus a threshold, with no Cauchy-Schwarz step.

Preamble
import Mathlib

open scoped Pointwise
Formal statement
theorem Finset.sum_addConvolution_eq_card_product {G : Type*} [AddCommGroup G] [DecidableEq G]
    (X Y : Finset G) :
    ∑ s ∈ X + Y, X.addConvolution Y s = X.card * Y.card := by sorry
Source
Elementary total-mass identity sum_s r(s) = |X||Y| for the additive convolution; used inside the proof of Tao-Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Lemma 2.30 (p. 80). Not separately stated in the cited works. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Combinatorics/Additive/BalogSzemerediGowers.lean#L39-L52
Human review

  • Endorsed by Shuze Chen · Sep 18, 2026

  • Endorsed by mysticflounder · Sep 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph