noncomputable def BSG.sumsetImage {G : Type u_1} [DecidableEq G] [AddCommGroup G] (X : Finset (G × G)) : Finset G

The sumset image of a finite set $X \subseteq G \times G$ under addition: $\{a + b : (a,b) \in X\}$.

theorem BSG.sum_fiber_le {G : Type u_1} [DecidableEq G] [AddCommGroup G] [Fintype G] (X : Finset (G × G)) (S : Finset G) : ∑ s ∈ S, {t ∈ sumsetImage X ×ˢ sumsetImage X ×ˢ sumsetImage X | t.1 - t.2.1 + t.2.2 = s}.card ≤ (sumsetImage X).card ^ 3

Auxiliary counting bound: for any $S$, the total number of triples $(t_0, t_1, t_2) \in (\text{sumsetImage}\,X)^3$ with $t_0 - t_1 + t_2 \in S$, summed over $s \in S$, is at most $|\text{sumsetImage}\,X|^3$.

theorem BSG.card_sq_mul_card_sq_le_card_add_mul_addEnergy {α : Type u_1} [DecidableEq α] [Add α] (A B : Finset α) : A.card ^ 2 * B.card ^ 2 ≤ (A + B).card * A.addEnergy B

BSG (Balog–Szemerédi–Gowers) proposition / energy lower bound: for finite sets $A, B$ in an additive structure, $|A|^2 |B|^2 \leq |A + B| \cdot E(A, B)$, where $E(A,B)$ denotes the additive energy.