The Balog-Szemerédi-Gowers theorem

A straightforward calculation shows that sets of small doubling have large additive energy. The converse is almost true, in the sense that a set of large additive energy contains a large set of small doubling. This is the content of the Balog-Szemerédi-Gowers theorem, which this file proves.

theorem BSG {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.dens ^ 2 * ↑B.dens) ≤ ↑(A.addEnergy' B)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.dens ≤ ↑A'.dens ∧ ↑(A' - A').dens ≤ 2 ^ 10 * K ^ 5 * ↑B.dens ^ 4 / ↑A.dens ^ 3

The Balog-Szemerédi-Gowers theorem for two sets.

If two sets A and B have large energy, then there exists a large subset A' of A of small difference.

theorem BSG₂ {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.dens ^ 2 * ↑B.dens) ≤ ↑(A.addEnergy' B)) : ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.dens ≤ ↑A'.dens ∧ (2 ^ 4)⁻¹ * K⁻¹ * ↑A.dens ≤ ↑B'.dens ∧ ↑(A' - B').dens ≤ 2 ^ 10 * K ^ 5 * ↑B.dens ^ 4 / ↑A.dens ^ 3

The Balog-Szemerédi-Gowers theorem for two sets.

If two sets A and B have large energy, then there exist large subsets A' of A and B' of B of small difference.

Note that the statement is subtly asymmetric in A and B, because largeness of both A' and B' is measured in terms of A.

theorem BSG_self {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * ↑A.dens ^ 3 ≤ ↑(A.addEnergy' A)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.dens ≤ ↑A'.dens ∧ ↑(A' - A').dens ≤ 2 ^ 10 * K ^ 5 * ↑A.dens

The Balog-Szemerédi-Gowers theorem for two sets.

If a set A has large energy, then there exists a large subset A' of A of small difference.

theorem BSG_self' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * ↑A.dens ^ 3 ≤ ↑(A.addEnergy' A)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.dens ≤ ↑A'.dens ∧ ↑(A' - A').dens ≤ 2 ^ 14 * K ^ 6 * ↑A'.dens

The Balog-Szemerédi-Gowers theorem for two sets.

If a set A has large energy, then there exists a large subset A' of A of small difference.