Small triple-representation set bounds the sumset via multiplicity
ProvedFinset.restricted_sumset_via_multiplicityLet be an additive commutative group and let be finite sets, and let . Suppose every sum with and admits at least representations
Then
The proof is double counting: the fibres of the map , , over distinct sums are pairwise disjoint and each has size at least , while they all sit inside , which has elements.
Note that is the Cartesian cube of , and the image of the map above is the triple-representation set . Neither is a dilate of : no scaling is applied to , and the three coordinates range independently.
In the Balog-Szemeredi-Gowers project this is the final counting step: the Tao-Vu injection supplies a uniform multiplicity of such triple representations for every sum in , and this lemma converts that into the honest sumset bound .
import Mathlib open scoped Pointwise
theorem Finset.restricted_sumset_via_multiplicity {G : Type*} [AddCommGroup G] [DecidableEq G]
(A B S : Finset G) (M : ℕ) :
(∀ a ∈ A, ∀ b ∈ B,
M ≤ ((S ×ˢ S ×ˢ S).filter
(fun p : G × G × G ↦ p.1 - p.2.1 + p.2.2 = a + b)).card) →
M * (A + B).card ≤ S.card ^ 3 := by sorry
Confirmed by the mission captain (proposal self-audit).