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

Auxiliary counting lemma used in the proof of Balog–Szemerédi–Gowers. For a finite set X ⊂ G × G and any S ⊂ G, the sum over s ∈ S of the number of triples (t₀, t₁, t₂) ∈ (X.image (+))^3 with t₀ - t₁ + t₂ = s is bounded by |X.image (+)|^3 — the total number of triples available.