theorem ProjectionTheory.bsg_projection_variant {G : Type u_1} [CommRing G] [DecidableEq G] : ∃ (c₁ : ℕ) (c₂ : ℕ) (C₁ : ℝ) (C₂ : ℝ), C₁ > 0 ∧ C₂ > 0 ∧ ∀ (A B : Finset G) (X : Finset (G × G)) (t : G) (N : ℕ), ∀ K ≥ 1, A.card ≤ N → B.card ≤ N → X ⊆ A ×ˢ B → ↑X.card ≥ K⁻¹ * ↑N ^ 2 → ↑(Finset.image (fun (p : G × G) => p.1 + t * p.2) X).card ≤ K * ↑N → ∃ (A' : Finset G) (B' : Finset G), A' ⊆ A ∧ B' ⊆ B ∧ ↑{p ∈ X | p ∈ A' ×ˢ B'}.card ≥ C₁ * K ^ (-↑c₁) * ↑N ^ 2 ∧ ↑(Finset.image (fun (p : G × G) => p.1 + t * p.2) (A' ×ˢ B')).card ≤ C₂ * K ^ ↑c₂ * ↑N

Balog–Szemerédi–Gowers (projection variant). For a commutative ring G and any parameter t ∈ G, define the projection πₜ(a, b) = a + t·b. If X ⊆ A × B with |A|, |B| ≤ N, |X| ≥ K⁻¹ N² and |πₜ(X)| ≤ K N, then there exist refined subsets A' ⊆ A, B' ⊆ B such that |X ∩ (A' × B')| ≳ K^{-O(1)} N² and |πₜ(A' × B')| ≲ K^{O(1)} N. This is the form of BSG used in the proof of the Bourgain–Katz–Tao sum-product theorem.