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 oneOfPair_aux {α : Type u_1} [DecidableEq α] {H : Finset (α × α)} {X : Finset α} {x : α} (hH : H ⊆ X ×ˢ X) : {yz ∈ H | yz.1 = x}.card = {c ∈ X | (x, c) ∈ H}.card

noncomputable def oneOfPair {α : Type u_1} [Fintype α] [DecidableEq α] (H : Finset (α × α)) (X : Finset α) : Finset α

Elements of X with at least the threshold density of partners in H.

Equations

• oneOfPair H X = {x ∈ X | 3 / 4 * ↑X.dens ≤ ↑{c ∈ X | (x, c) ∈ H}.dens}

theorem oneOfPair_subset {α : Type u_1} [Fintype α] [DecidableEq α] {H : Finset (α × α)} {X : Finset α} : oneOfPair H X ⊆ X

theorem mem_oneOfPair {α : Type u_1} [Fintype α] [DecidableEq α] {H : Finset (α × α)} {X : Finset α} {x : α} : x ∈ oneOfPair H X ↔ x ∈ X ∧ 3 / 4 * ↑X.dens ≤ ↑{c ∈ X | (x, c) ∈ H}.dens

theorem oneOfPair_bound_one {α : Type u_1} [Fintype α] [DecidableEq α] {H : Finset (α × α)} {X : Finset α} : (∑ x ∈ X \ oneOfPair H X, ↑{c ∈ X | (x, c) ∈ H}.dens) / ↑(Fintype.card α) ≤ 3 / 4 * ↑X.dens ^ 2

theorem oneOfPair_bound_two {α : Type u_1} [Fintype α] [DecidableEq α] {H : Finset (α × α)} {X : Finset α} (hH : H ⊆ X ×ˢ X) (Hcard : 7 / 8 * ↑X.dens ^ 2 ≤ ↑H.dens) : 1 / 8 * ↑X.dens ^ 2 ≤ ↑X.dens * ↑(oneOfPair H X).dens

theorem quadruple_bound_c {α : Type u_1} [Fintype α] [DecidableEq α] {H : Finset (α × α)} {X : Finset α} {a b : α} (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X) : ↑X.dens / 2 ≤ ↑{c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.dens

theorem quadruple_bound_right {G : Type u_1} [AddCommGroup G] [DecidableEq G] {B : Finset G} {x a b : G} (H : Finset (G × G)) (X : Finset G) (h : x = a - b) : ↑({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun (c : G) => {x ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c}).card ≤ ↑{x ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ - (a₃ - a₄) = a - b}.card

theorem claim_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : Type u_2} [Semifield K] [CharZero K] [StarRing K] : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ↑(A ∩ (x +ᵥ B)).dens) = ↑(A.addEnergy' B)

theorem claim_two {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} : ↑(A.addEnergy' B) ^ 2 / (↑A.dens * ↑B.dens) ≤ Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ↑(A ∩ (x +ᵥ B)).dens ^ 2

theorem claim_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ↑((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ H).dens) = (∑ ab ∈ H, Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ((↑B).indicator (fun (x : G) => 1) (ab.1 - x) * (↑B).indicator (fun (x : G) => 1) (ab.2 - x))) / ↑(Fintype.card G) ^ 2

theorem claim_four {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (ab : G × G) : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ((↑B).indicator (fun (x : G) => 1) (ab.1 - x) * (↑B).indicator (fun (x : G) => 1) (ab.2 - x))) ≤ ↑B.dens * (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (ab.1 - ab.2)

theorem claim_five {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ↑((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ H).dens) ≤ (↑B.dens * ∑ ab ∈ H, (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (ab.1 - ab.2)) / ↑(Fintype.card G) ^ 2

noncomputable def choiceH {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A B : Finset G) (c : ℝ) : Finset (G × G)

Pairs in A × A whose difference has bounded convolution weight in B.

Equations

• choiceH A B c = {ab ∈ A ×ˢ A | (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (ab.1 - ab.2) ≤ c / 2 * (↑(A.addEnergy' B) ^ 2 / (↑A.dens ^ 3 * ↑B.dens ^ 2))}

theorem choiceH_subset {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c : ℝ} : choiceH A B c ⊆ A ×ˢ A

theorem claim_six {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (c : ℝ) (hc : 0 ≤ c) : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * ↑((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ choiceH A B c).dens) ≤ c / 2 * (↑(A.addEnergy' B) ^ 2 / (↑A.dens * ↑B.dens))

theorem claim_seven {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c : ℝ} (hc : 0 ≤ c) : (Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * (c / 2 * (↑(A.addEnergy' B) ^ 2 / (↑A.dens ^ 2 * ↑B.dens ^ 2)) + ↑((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ choiceH A B c).dens)) ≤ Finset.univ.expect fun (x : G) => (((↑A).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) x * (c * ↑(A ∩ (x +ᵥ B)).dens ^ 2)

theorem claim_eight {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {c : ℝ} (hc : 0 ≤ c) (A B : Finset G) : ∃ (x : G), c / 2 * (↑(A.addEnergy' B) ^ 2 / (↑A.dens ^ 2 * ↑B.dens ^ 2)) + ↑((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ choiceH A B c).dens ≤ c * ↑(A ∩ (x +ᵥ B)).dens ^ 2

theorem lemma_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (↑A.dens ^ 2 * ↑B.dens) ≤ ↑(A.addEnergy' B)) (hA : A.Nonempty) (hB : B.Nonempty) : ∃ (x : G), ∃ X ⊆ A ∩ (x +ᵥ B), ↑A.dens / (√2 * K) ≤ ↑X.dens ∧ (1 - c) * ↑X.dens ^ 2 ≤ ↑{x ∈ X ×ˢ X | match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * ↑A.dens ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (a - b)}.dens

theorem lemma_one' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (↑A.dens ^ 2 * ↑B.dens) ≤ ↑(A.addEnergy' B)) (hA : A.Nonempty) (hB : B.Nonempty) : ∃ (x : G), ∃ X ⊆ A ∩ (x +ᵥ B), ↑A.dens / (2 * K) ≤ ↑X.dens ∧ (1 - c) * ↑X.dens ^ 2 ≤ ↑{x ∈ X ×ˢ X | match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * ↑A.dens ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (a - b)}.dens

theorem quadruple_bound_other {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {a b c : G} {K : ℝ} {H : Finset (G × G)} (hac : (a, c) ∈ H) (hbc : (b, c) ∈ H) (hH : ∀ x ∈ H, ↑A.dens / (2 ^ 4 * K ^ 2) ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (x.1 - x.2)) : (↑A.dens / (2 ^ 4 * K ^ 2)) ^ 2 ≤ ↑{x ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c}.card / ↑(Fintype.card G) ^ 2

theorem quadruple_bound_left {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B X : Finset G} {a b : G} {K : ℝ} {H : Finset (G × G)} (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X) (hH : ∀ x ∈ H, ↑A.dens / (2 ^ 4 * K ^ 2) ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (x.1 - x.2)) : ↑X.dens / 2 * (↑A.dens / (2 ^ 4 * K ^ 2)) ^ 2 ≤ ↑({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun (c : G) => {x ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c}).card / ↑(Fintype.card G) ^ 3

theorem quadruple_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} {X : Finset G} {K : ℝ} {x : G} (hx : x ∈ oneOfPair H X - oneOfPair H X) (hH : ∀ x ∈ H, ↑A.dens / (2 ^ 4 * K ^ 2) ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (x.1 - x.2)) : ↑A.dens ^ 2 * ↑X.dens / (2 ^ 9 * K ^ 4) ≤ ↑{x_1 ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x_1 with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ - (a₃ - a₄) = x}.card / ↑(Fintype.card G) ^ 3

theorem big_quadruple_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} {X : Finset G} {K : ℝ} (hH : ∀ x ∈ H, ↑A.dens / (2 ^ 4 * K ^ 2) ≤ (((↑B).indicator fun (x : G) => 1) ○ (↑B).indicator fun (x : G) => 1) (x.1 - x.2)) (hX : ↑A.dens / (2 * K) ≤ ↑X.dens) : ↑(oneOfPair H X - oneOfPair H X).dens * (↑A.dens ^ 3 / (2 ^ 10 * K ^ 5)) ≤ ↑B.dens ^ 4

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

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_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.