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

theorem quadruple_bound_right {α : Type u_1} [DecidableEq α] {B : Finset α} {x : α} [AddCommGroup α] {a b : α} (H : Finset (α × α)) (X : Finset α) (h : x = a - b) : ↑({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun (c : α) => {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 thing_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} {x : G} : (𝟭 B ○ 𝟭 A) x = ∑ y : G, 𝟭 A y * 𝟭 B (x + y)

theorem thing_one_right {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A 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] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} : ∑ s : G, (𝟭 A ○ 𝟭 B) s = ↑A.card * ↑B.card

theorem thing_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} : ∑ s : G, (𝟭 A ○ 𝟭 B) s ^ 2 = ↑(A.addEnergy B)

theorem claim_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} : ∑ s : G, (𝟭 A ○ 𝟭 B) s * ↑(A ∩ (s +ᵥ B)).card = ↑(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.card * ↑B.card) ≤ ∑ s : G, (𝟭 A ○ 𝟭 B) s * ↑(A ∩ (s +ᵥ B)).card ^ 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) : ∑ s : G, (𝟭 A ○ 𝟭 B) s * ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card = ∑ ab ∈ H, ∑ 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 B : Finset G} (ab : G × G) : ∑ 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 B : Finset G} {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) : ∑ s : G, (𝟭 A ○ 𝟭 B) s * ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card ≤ ↑B.card * ∑ ab ∈ H, (𝟭 B ○ 𝟭 B) (ab.1 - ab.2)

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

Equations

• H_choice A B c = {ab ∈ A ×ˢ A | (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (↑(A.addEnergy B) ^ 2 / (↑A.card ^ 3 * ↑B.card ^ 2))}

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

theorem claim_seven {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (c : ℝ) (hc : 0 ≤ c) (hA : 0 < ↑A.card) (hB : 0 < ↑B.card) : ∑ s : G, (𝟭 A ○ 𝟭 B) s * (c / 2 * (↑(A.addEnergy B) ^ 2 / (↑A.card ^ 2 * ↑B.card ^ 2)) + ↑((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤ ∑ 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 B : Finset G} (c : ℝ) (hc : 0 ≤ c) (hA : 0 < ↑A.card) (hB : 0 < ↑B.card) : ∃ (s : G), c / 2 * (↑(A.addEnergy 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 B : Finset G} {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy 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 ≤ ↑{x ∈ X ×ˢ X | match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) (a - b)}.card

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.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy 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 ≤ ↑{x ∈ X ×ˢ X | match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) (a - b)}.card

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

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

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, 1 / 8 / 2 * (K ^ 2)⁻¹ * ↑A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) : (↑A.card / (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

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, 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 ≤ ↑({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

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, 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) ≤ ↑{x_1 ∈ (B ×ˢ B) ×ˢ B ×ˢ B | match x_1 with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ - (a₃ - a₄) = x}.card

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, 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 B : Finset G} {K : ℝ} (hK : 0 < K) (hA : 0 < ↑A.card) (hB : 0 < ↑B.card) (hAB : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy 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 B : Finset G} {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy 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 B : Finset G} {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (↑A.card ^ 2 * ↑B.card) ≤ ↑(A.addEnergy 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 ≤ ↑(A.addEnergy 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 ≤ ↑(A.addEnergy A)) : ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * ↑A.card ≤ ↑A'.card ∧ ↑(A' - A').card ≤ 2 ^ 14 * K ^ 6 * ↑A'.card