theorem thing_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {β : Type u_2} [CommSemiring β] [StarRing β] {A : Finset G} {B : Finset G} {x : G} : (𝟭 B ○ 𝟭 A) x = Finset.sum Finset.univ fun (y : G) => 𝟭 A y * 𝟭 B (x + y)

theorem thing_one_right {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {β : Type u_2} [CommSemiring β] [StarRing β] {A : Finset G} {B : Finset G} {x : G} : (𝟭 A ○ 𝟭 B) x = ↑(A ∩ (x +ᵥ B)).card

theorem thing_two {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {β : Type u_2} [CommSemiring β] [StarRing β] {A : Finset G} {B : Finset G} : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s) = ↑A.card * ↑B.card

theorem thing_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {β : Type u_2} [CommSemiring β] [StarRing β] {A : Finset G} {B : Finset G} : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s ^ 2) = ↑E[A, B]

theorem claim_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {β : Type u_2} [CommSemiring β] [StarRing β] {A : Finset G} {B : Finset G} : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * ↑(A ∩ (s +ᵥ B)).card) = ↑E[A, B]

theorem claim_two {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} : ↑E[A, B] ^ 2 / (↑A.card * ↑B.card) ≤ Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * ↑(A ∩ (s +ᵥ B)).card ^ 2

theorem claim_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card) = Finset.sum H fun (ab : G × G) => Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s))

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

theorem claim_five {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card) ≤ ↑B.card * Finset.sum H fun (ab : G × G) => (𝟭 B ○ 𝟭 B) (ab.1 - ab.2)

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

Equations

• H_choice A B c = Finset.filter (fun (ab : G × G) => (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (↑E[A, B] ^ 2 / (↑A.card ^ 3 * ↑B.card ^ 2))) (A ×ˢ A)

theorem claim_six {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} (c : ℝ) (hc : 0 ≤ c) : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤ c / 2 * (↑E[A, B] ^ 2 / (↑A.card * ↑B.card))

theorem claim_seven {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} (c : ℝ) (hc : 0 ≤ c) (hA : 0 < ↑A.card) (hB : 0 < ↑B.card) : (Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * (c / 2 * (↑E[A, B] ^ 2 / (↑A.card ^ 2 * ↑B.card ^ 2)) + ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card)) ≤ Finset.sum Finset.univ fun (s : G) => (𝟭 A ○ 𝟭 B) s * (c * ↑(A ∩ (s +ᵥ B)).card ^ 2)

theorem claim_eight {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} (c : ℝ) (hc : 0 ≤ c) (hA : 0 < ↑A.card) (hB : 0 < ↑B.card) : ∃ (s : G), c / 2 * (↑E[A, B] ^ 2 / (↑A.card ^ 2 * ↑B.card ^ 2)) + ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card ≤ c * ↑(A ∩ (s +ᵥ B)).card ^ 2

theorem test_case {E : ℕ} {A : ℕ} {B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (↑A ^ 2 * ↑B) ≤ ↑E) (hA : 0 < A) (hB : 0 < B) : ↑A / (√2 * K) ≤ √2⁻¹ * (↑E / (↑A * ↑B))

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

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

theorem many_pairs {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} {K : ℝ} {x : G} (hab : 1 / 8 / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) x) : ↑A.card / (2 ^ 4 * K ^ 2) ≤ ↑(Finset.filter (fun (x_1 : G × G) => match x_1 with | (c, d) => c - d = x) (B ×ˢ B)).card

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

Equations

• oneOfPair H X = Finset.filter (fun (x : G) => 3 / 4 * ↑X.card ≤ ↑(Finset.filter (fun (yz : G × G) => yz.1 = x) H).card) X

theorem oneOfPair_mem {G : Type u_1} [DecidableEq G] {x : G} {H : Finset (G × G)} {X : Finset G} : x ∈ oneOfPair H X ↔ x ∈ X ∧ 3 / 4 * ↑X.card ≤ ↑(Finset.filter (fun (yz : G × G) => yz.1 = x) H).card

theorem oneOfPair_mem' {G : Type u_1} [AddCommGroup G] [DecidableEq G] {x : G} {H : Finset (G × G)} {X : Finset G} (hH : H ⊆ X ×ˢ X) : (Finset.filter (fun (yz : G × G) => yz.1 = x) H).card = (Finset.filter (fun (c : G) => (x, c) ∈ H) X).card

theorem oneOfPair_bound_one {G : Type u_1} [DecidableEq G] {H : Finset (G × G)} {X : Finset G} : (Finset.sum (X \ oneOfPair H X) fun (x : G) => ↑(Finset.filter (fun (xy : G × G) => xy.1 = x) H).card) ≤ 3 / 4 * ↑X.card ^ 2

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

theorem oneOfPair_bound {G : Type u_1} [AddCommGroup G] [DecidableEq G] {A : Finset G} {H : Finset (G × G)} {X : Finset G} {K : ℝ} (hH : H ⊆ X ×ˢ X) (hX : 0 < ↑X.card) (Hcard : 7 / 8 * ↑X.card ^ 2 ≤ ↑H.card) (h : ↑A.card / (2 * K) ≤ ↑X.card) : ↑A.card / (2 ^ 4 * K) ≤ ↑(oneOfPair H X).card

theorem quadruple_bound_part {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} {K : ℝ} (a : G) (c : G) (hac : 1 / 8 / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) (a - c)) : ↑A.card / (2 ^ 4 * K ^ 2) ≤ ↑(Finset.filter (fun (x : G × G) => match x with | (a₁, a₂) => a₁ - a₂ = a - c) (B ×ˢ B)).card

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

theorem quadruple_bound_c {G : Type u_1} [AddCommGroup G] [DecidableEq G] {X : Finset G} {a : G} {b : G} {H : Finset (G × G)} (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X) (hH : H ⊆ X ×ˢ X) : ↑X.card / 2 ≤ ↑(Finset.filter (fun (c : G) => (a, c) ∈ H ∧ (b, c) ∈ H) X).card

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

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

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

theorem big_quadruple_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {B : Finset G} {H : Finset (G × G)} {X : Finset G} {K : ℝ} (hH : ∀ x ∈ H, 1 / 8 / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) (hH' : H ⊆ X ×ˢ X) (hX : ↑A.card / (2 * K) ≤ ↑X.card) : ↑(oneOfPair H X - oneOfPair H X).card * (↑A.card ^ 3 / (2 ^ 10 * K ^ 5)) ≤ ↑B.card ^ 4

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

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

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

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.card ^ 3 ≤ ↑E[A]) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 10 * K ^ 5 * ↑A.card

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.card ^ 3 ≤ ↑E[A]) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 14 * K ^ 6 * ↑A'.card