```section‹Background material in additive combinatorics›

text ‹This section outlines some background definitions and basic lemmas in additive combinatorics
based on the notes by Gowers \cite{Gowersnotes}. ›
(*
Session: Balog_Szemeredi_Gowers
Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
Affiliation: University of Cambridge
Date: August 2022.
*)

imports
Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
begin

begin

"additive_quadruple a b c d  ≡ a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ d ∈ G ∧ a ⊕ b = c ⊕ d"

shows "d = a ⊕ b ⊖ c"
invertible_right_inverse2)

shows "a ⊖ c = d ⊖ b"
composition_closed inverse_closed invertible invertible_inverse_inverse invertible_right_inverse2)

definition additive_quadruple_set:: "'a set ⇒ ('a × 'a × 'a × 'a) set" where
"additive_quadruple_set A ≡ {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧

"additive_quadruple_set A ⊆ {(a, b, c, d) | a b c d. d = a ⊕ b ⊖ c ∧ a ∈ A ∧ b ∈ A ∧
by auto

definition additive_energy:: "'a set ⇒ real" where

assumes "finite A"

proof-
define f:: "'a × 'a × 'a × 'a ⇒ 'a × 'a × 'a" where "f = (λ (a, b, c, d) . (a, b, c))"
have hinj: "inj_on f {(a, b, c, d) | a b c d. d = a ⊕ b ⊖ c ∧ a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A}"
unfolding inj_on_def f_def by auto
moreover have himage: "f ` {(a, b, c, d) | a b c d. d = a ⊕ b ⊖ c ∧ a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A} ⊆ A × A × A"
unfolding f_def by auto
ultimately have "card (additive_quadruple_set A) ≤ card ({(a, b, c, d) | a b c d. d = a ⊕ b ⊖ c ∧ a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A})"
by (metis (no_types, lifting))
also have "... ≤ card (A × A × A)" using himage hinj assms card_inj_on_le finite_SigmaI
by (metis (no_types, lifting))
finally show ?thesis by (simp add: card_cartesian_product power3_eq_cube)
qed

proof (cases "finite A")
assume hA: "finite A"
card_cartesian_product power3_eq_cube by (simp add: divide_le_eq)
next
assume "infinite A"
thus ?thesis unfolding additive_energy_def by simp
qed

subsection‹On sums›

definition f_sum:: "'a ⇒'a set ⇒ nat" where
"f_sum d A ≡ card {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}"

lemma pairwise_disjnt_sum_1:
"pairwise (λs t. disjnt ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)}) s)
((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)}) t)) (sumset A A)"
unfolding disjnt_def by (intro pairwiseI) (auto)

lemma pairwise_disjnt_sum_2:
"pairwise disjnt ((λ d. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}) ` (sumset A A))"
unfolding disjnt_def by (intro pairwiseI) (auto)

lemma sum_Union_span:
assumes "A ⊆ G"
shows "⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)}) ` (sumset A A)) = A × A"

proof
show "⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)}) ` (sumset A A)) ⊆ A × A" by blast
next
show "A × A ⊆ ⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)}) ` (sumset A A))"
proof (intro subsetI)
fix x assume hxA: "x ∈ A × A"
then obtain y z where hxyz: "x = (y, z)" and hy: "y ∈ A" and hz:"z ∈ A" by blast
show "x ∈ (⋃d∈(sumset A A).{(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d})"
using hy hz assms hxA hxyz by auto
qed
qed

lemma f_sum_le_card:
assumes "finite A" and "A ⊆ G"
shows "f_sum d A ≤ card A"

proof-
define f:: "('a × 'a) ⇒ 'a" where "f ≡ (λ (a, b). a)"
have "inj_on f {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}"
unfolding f_def proof (intro inj_onI)
fix x y assume "x ∈ {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}" and
"y ∈ {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}" and
hcase: "(case x of (a, b) ⇒ a) = (case y of (a, b) ⇒ a)"
then obtain x1 x2 y1 y2 where hx: "x = (x1, x2)" and hy:"y = (y1, y2)" and h1: "x1 ⊕ x2 = d" and
h2: "y1 ⊕ y2 = d" and hx1: "x1 ∈ A" and hx2: "x2 ∈ A" and hy1: "y1 ∈ A" and hy2: "y2 ∈ A" by blast
have hxsub: "x2 = d ⊖ x1"
using h1 hx1 hx2 assms by (metis additive_abelian_group.inverse_closed composition_closed
have hysub: "y2 = d ⊖ y1"
using h2 hy1 hy2 assms by (metis inverse_closed commutative composition_closed hy1 hy2
invertible invertible_left_inverse2 subset_iff)
show "x = y" using hx hy hxsub hysub hcase by auto
qed
moreover have "f ` {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d} ⊆ A" using f_def by auto
ultimately show ?thesis using card_mono assms f_sum_def card_image[of "f"]
by (metis (mono_tags, lifting))
qed

lemma f_sum_card:
assumes "A ⊆ G" and hA: "finite A"
shows "(∑ d ∈ (sumset A A). (f_sum d A)) = (card A)^2"

proof-
have fin: "∀ X ∈ ((λ d. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d) }) ` (sumset A A)). finite X"
proof
fix X assume hX: "X ∈ (λd. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}) ` (sumset A A)"
then obtain d where hXd: "X = {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}" by blast
show "finite X" using hA hXd finite_subset finite_cartesian_product
by (smt (verit, best) mem_Collect_eq mem_Sigma_iff rev_finite_subset subrelI)
qed
have "(∑d∈(sumset A A). f_sum d A) = card (A × A)"
unfolding f_sum_def
using sum_card_image[of "sumset A A" "(λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊕ b = d)})"]
pairwise_disjnt_sum_1 hA finite_sumset card_Union_disjoint[of "((λd. {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = d}) ` sumset A A)"]
fin pairwise_disjnt_sum_2 hA finite_sumset sum_Union_span assms by auto
thus ?thesis using card_cartesian_product power2_eq_square by metis
qed

lemma f_sum_card_eq:
assumes "A ⊆ G"
shows "∀ x ∈ sumset A A.  (f_sum x A)^2 =
card {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}"

proof
fix x assume "x ∈ sumset A A"
define C where hC: "C = {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}"
define f:: "'a × 'a × 'a × 'a ⇒ ('a × 'a) × ('a × 'a)" where "f = (λ (a, b, c, d). ((a, b), (c, d)))"
have hfinj: "inj_on f C" unfolding f_def by (intro inj_onI) (auto)
have "f ` C = {((a,b), (c,d)) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊕ b = x ∧ c ⊕ d = x}"
proof
show "f ` C ⊆ {((a, b), (c, d)) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊕ b = x ∧ c ⊕ d = x}"
unfolding f_def hC by auto
next
show "{((a, b), c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊕ b = x ∧ c ⊕ d = x} ⊆ f ` C"
proof
fix z assume "z ∈ {((a, b), (c, d)) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊕ b = x ∧ c ⊕ d = x}"
then obtain a b c d where hz: "z = ((a, b), (c, d))" and ha: "a ∈ A" and hb: "b ∈ A" and hc: "c ∈ A" and hd: "d ∈ A"
and hab: "a ⊕ b = x" and hcd: "c ⊕ d = x" by blast
then have habcd: "(a, b, c, d) ∈ C" using additive_quadruple_def assms hC by auto
show "z ∈ f ` C" using hz f_def habcd by force
qed
qed
moreover have "{((a, b), c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊕ b = x ∧ c ⊕ d = x} =
{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = x} × {(c, d) | c d. c ∈ A ∧ d ∈ A ∧ c ⊕ d = x}" by blast
ultimately have "card C = card ({(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊕ b = x}) ^ 2"
using hfinj card_image[of "f"]  card_cartesian_product by (metis (no_types, lifting) Sigma_cong power2_eq_square)
thus "(f_sum x A)^2 = card ({(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x})" using hC f_sum_def by auto
qed

lemma pairwise_disjoint_sum:
"pairwise (λs t. disjnt ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) s)
((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) t)) (sumset A A)"
unfolding disjnt_def by (intro pairwiseI) (auto)

"pairwise disjnt ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` (sumset A A))"
unfolding disjnt_def by (intro pairwiseI) (auto)

"⋃ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` (sumset A A)) = additive_quadruple_set A"

proof
show "(⋃x∈sumset A A.
{(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧
a ⊕ b = x ∧ c ⊕ d = x}) ⊆ additive_quadruple_set A"
next
{(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x})"
qed

assumes hAG: "A ⊆ G" and hA: "finite A"
shows "(∑ d ∈ (sumset A A). (f_sum d A)^2) = card (additive_quadruple_set A)"

proof-
have fin: "∀ X ∈ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` (sumset A A)). finite X"
proof
fix X assume "X ∈  (λx. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` sumset A A"
then obtain x where hX: "X = {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}"
by blast
show "finite X" using hA hX finite_subset finite_cartesian_product
by (smt (verit, best) mem_Collect_eq mem_Sigma_iff rev_finite_subset subrelI)
qed
have "(∑d∈sumset A A. (f_sum d A)⇧2) =
card (⋃ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` (sumset A A)))"
using f_sum_card_eq hAG sum_card_image[of "sumset A A" "(λx. {(a, b, c, d) |a b c d.
a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x})"]
pairwise_disjoint_sum card_Union_disjoint[of "(λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧
c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊕ b = x ∧ c ⊕ d = x}) ` (sumset A A)"]
fin pairwise_disjnt_quadruple_sum hA finite_sumset by auto
then show ?thesis using quadruple_sum_Union_eq by auto
qed

shows "(∑ d ∈ sumset A A. (f_sum d A)^2) = additive_energy A * (card A)^3"

definition popular_sum:: "'a ⇒ real ⇒ 'a set ⇒ bool" where
"popular_sum d θ A  ≡ f_sum d A ≥ θ * of_real (card A)"

definition popular_sum_set:: "real ⇒ 'a set ⇒ 'a set" where
"popular_sum_set θ A ≡ {d ∈ sumset A A. popular_sum d θ A}"

subsection‹On differences›

text‹The following material is directly analogous to the material given previously on sums.
All definitions and lemmas are the corresponding ones for differences.
E.g. @{term f_diff} corresponds to  @{term f_sum}. ›

definition f_diff:: "'a ⇒'a set ⇒ nat" where
"f_diff d A ≡ card {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}"

lemma pairwise_disjnt_diff_1:
"pairwise (λs t. disjnt ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d)}) s)
((λ d. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d)}) t)) (differenceset A A)"
using disjnt_def by (intro pairwiseI) (auto)

lemma pairwise_disjnt_diff_2:
"pairwise disjnt ((λ d. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}) ` (differenceset A A))"
unfolding disjnt_def by (intro pairwiseI) (auto)

lemma diff_Union_span:
assumes "A ⊆ G"
shows "⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d)}) ` (differenceset A A)) = A × A"

proof
show "⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d)}) ` (differenceset A A)) ⊆ A × A"
by blast
next
show "A × A ⊆ ⋃ ((λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d)}) ` (differenceset A A))"
proof (intro subsetI)
fix x assume hxA: "x ∈ A × A"
then obtain y z where hxyz: "x = (y, z)" and hy: "y ∈ A" and hz:"z ∈ A" by blast
show "x ∈ (⋃d∈(differenceset A A).{(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d})"
using hy hz assms hxA hxyz by auto
qed
qed

lemma f_diff_le_card:
assumes "finite A" and "A ⊆ G"
shows "f_diff d A ≤ card A"

proof-
define f:: "('a × 'a) ⇒ 'a" where "f ≡ (λ (a, b). a)"
have "inj_on f {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}"
unfolding f_def proof (intro inj_onI)
fix x y assume "x ∈ {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}" and
"y ∈ {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}" and
hcase: "(case x of (a, b) ⇒ a) = (case y of (a, b) ⇒ a)"
then obtain x1 x2 y1 y2 where hx: "x = (x1, x2)" and hy:"y = (y1, y2)" and h1: "x1 ⊖ x2 = d" and
h2: "y1 ⊖ y2 = d" and hx1: "x1 ∈ A" and hx2: "x2 ∈ A" and hy1: "y1 ∈ A" and hy2: "y2 ∈ A" by blast
have hxsub: "x2 = x1 ⊖ d"
using h1 assms associative commutative composition_closed hx1 hx2
by (smt (verit, best) inverse_closed invertible invertible_left_inverse2 subset_iff)
have hysub: "y2 = y1 ⊖ d"
using h2 assms associative commutative composition_closed hy1 hy2
by (smt (verit, best) inverse_closed invertible invertible_left_inverse2 subset_iff)
show "x = y" using hx hy hxsub hysub hcase by auto
qed
moreover have "f ` {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d} ⊆ A" using f_def by auto
ultimately show ?thesis using card_mono assms f_diff_def card_image[of "f"]
by (metis (mono_tags, lifting))
qed

lemma f_diff_card:
assumes "A ⊆ G" and hA: "finite A"
shows "(∑ d ∈ (differenceset A A). f_diff d A) = (card A)^2"

proof-
have fin: "∀ X ∈ ((λ d. {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d) }) ` (differenceset A A)).
finite X"
proof
fix X assume hX: "X ∈ (λd. {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}) ` (differenceset A A)"
then obtain d where hXd: "X = {(a, b) | a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}" and
"d ∈ (differenceset A A)" by blast
have hXA: "X ⊆ A × A" using hXd by blast
show "finite X" using hXA hA finite_subset by blast
qed
have "(∑d∈(differenceset A A). f_diff d A) = card (A × A)"
unfolding f_diff_def using sum_card_image[of "differenceset A A"
"(λ d .{(a, b) | a b. a ∈ A ∧ b ∈ A ∧ (a ⊖ b = d) })"] pairwise_disjnt_diff_1
card_Union_disjoint[of "((λd. {(a, b) |a b. a ∈ A ∧ b ∈ A ∧ a ⊖ b = d}) ` differenceset A A)"]
fin pairwise_disjnt_diff_2 diff_Union_span assms hA finite_minusset finite_sumset by auto
thus ?thesis using card_cartesian_product power2_eq_square by metis
qed

lemma f_diff_card_eq:
assumes "A ⊆ G"
shows "∀ x ∈ differenceset A A. (f_diff x A)^2 =
card {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}"

proof
fix x assume "x ∈ differenceset A A"
define C where hC: "C= {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x }"
define f:: "'a × 'a × 'a × 'a ⇒ ('a × 'a) × ('a × 'a)" where "f = (λ (a, b, c, d). ((a, c), (d, b)))"
have hfinj: "inj_on f C" using f_def by (intro inj_onI) (auto)
have "f ` C = {((a,c), (d,b)) | a b c d.
a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊖ c = x ∧ d ⊖ b = x}"
proof
show "f ` C ⊆ {((a, c), (d, b)) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊖ c = x ∧ d ⊖ b = x}"
unfolding f_def hC by auto
next
show "{((a, c), d, b) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊖ c = x ∧ d ⊖ b = x} ⊆ f ` C"
proof
fix z assume "z ∈ {((a, c), (d, b)) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊖ c = x ∧ d ⊖ b = x}"
then obtain a b c d where hz: "z = ((a, c), (d, b))" and ha: "a ∈ A" and hb: "b ∈ A" and hc: "c ∈ A" and hd: "d ∈ A"
and hab: "a ⊖ c = x" and hcd: "d ⊖ b = x" by blast
using assms by (metis (no_types, lifting) ha hb hc hd additive_quadruple_def associative
commutative composition_closed hab hcd inverse_closed invertible invertible_right_inverse2 subset_eq)
then have habcd: "(a, b, c, d) ∈ C" using hab hcd hC ha hb hc hd by blast
show "z ∈ f ` C" using hz f_def habcd image_iff by fastforce
qed
qed
moreover have "{((a, c), (d, b))|a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a ⊖ c = x ∧ d ⊖ b = x} =
{(a, c) | a c. a ∈ A ∧ c ∈ A ∧ a ⊖ c = x} × {(d, b) | d b. d ∈ A ∧ b ∈ A ∧ d ⊖ b = x}" by blast
moreover have "card C = card (f ` C)" using hfinj card_image[of "f"] by auto
ultimately have "card C =  card ({(a, c) | a c. a ∈ A ∧ c ∈ A ∧ a ⊖ c = x}) ^ 2"
using hfinj card_image[of "f"] card_cartesian_product Sigma_cong power2_eq_square by (smt (verit, best))
thus "(f_diff x A)⇧2 = card  {(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}"
using f_diff_def hC by simp
qed

lemma pairwise_disjoint_diff:
"pairwise (λs t. disjnt ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) s)
((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) t)) (differenceset A A)"
unfolding disjnt_def by (intro pairwiseI) (auto)

"pairwise disjnt ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) ` (differenceset A A))"
unfolding disjnt_def by (intro pairwiseI) (auto)

"⋃ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) ` (differenceset A A)) =

proof
show "(⋃x∈differenceset A A. {(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
next
{(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x})"
proof (intro subsetI)
then obtain x1 x2 x3 x4 where hx: "x = (x1, x2, x3, x4)" and hx1: "x1 ∈ A" and hx2: "x2 ∈ A" and hx3: "x3 ∈ A"
have hxmem: "(x1, x2, x3, x4) ∈ {(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x1 ⊖ x3 ∧ d ⊖ b = x1 ⊖ x3}"
show "x ∈ (⋃x∈differenceset A A. {(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x})"
qed
qed

assumes hAG: "A ⊆ G" and hA: "finite A"
shows "(∑ d ∈ (differenceset A A). (f_diff d A)^2) = card (additive_quadruple_set A)"

proof-
have fin: "∀ X ∈ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) ` (differenceset A A)). finite X"
proof
fix X assume "X ∈ (λx. {(a, b, c, d) |a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) ` differenceset A A"
then obtain x where hX: "X = {(a, b, c, d) | a b c d. a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧
additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}" and "x ∈ differenceset A A" by blast
show "finite X" using hX hA finite_subset finite_cartesian_product
by (smt (verit, best) mem_Collect_eq mem_Sigma_iff rev_finite_subset subrelI) (*slow*)
qed
have "(∑d∈differenceset A A. (f_diff d A)⇧2) = card (⋃ ((λ x. {(a, b, c, d) | a b c d. a ∈ A ∧
b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) ` (differenceset A A)))"
using f_diff_card_eq hAG sum_card_image[of "differenceset A A" "(λx. {(a, b, c, d) |a b c d.
a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x})"]
pairwise_disjoint_diff card_Union_disjoint[of "(λ x. {(a, b, c, d) | a b c d. a ∈ A ∧
b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ additive_quadruple a b c d ∧ a ⊖ c = x ∧ d ⊖ b = x}) `
(differenceset A A)"] fin pairwise_disjnt_quadruple_diff hA finite_minusset finite_sumset by auto
thus ?thesis using quadruple_diff_Union_eq by auto
qed