theorem BSGVar.bsg_var {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A B : Finset G) (N : ℕ) (K : ℝ) (hK : K ≥ 1) (hA : A.card = N) (hB : B.card = N) (hE : ↑(A.addEnergy B) ≥ K⁻¹ * ↑N ^ 3) : ∃ C > 0, ∃ (A' : Finset G) (B' : Finset G), A' ⊆ A ∧ B' ⊆ B ∧ ↑A'.card ≥ K ^ (-C) * ↑N ∧ ↑B'.card ≥ K ^ (-C) * ↑N ∧ ↑(A' + B').card ≤ K ^ C * ↑N

Balog–Szemerédi–Gowers variant (energy form). Let A, B be subsets of an abelian group with |A| = |B| = N and additive energy E(A, B) ≥ K⁻¹ N³. Then there exist A' ⊆ A, B' ⊆ B with |A'|, |B'| ≥ K^{-C} N and |A' + B'| ≤ K^{C} N for some constant C > 0.