Theory Additive_Combinatorics_Preliminaries

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
  Title:   Additive_Combinatorics_Preliminaries.thy
  Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds 
  Affiliation: University of Cambridge
  Date: August 2022.
*)

theory Additive_Combinatorics_Preliminaries
  imports 
    Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
begin

subsection‹Additive quadruples and additive energy›

context additive_abelian_group

begin

definition additive_quadruple:: "'a ⇒'a ⇒'a ⇒ 'a ⇒ bool" where 
  "additive_quadruple a b c d  ≡ a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ d ∈ G ∧ a ⊕ b = c ⊕ d"

lemma additive_quadruple_aux:
  assumes "additive_quadruple a b c d"
  shows "d = a ⊕ b ⊖ c"
  by (metis additive_quadruple_def assms associative commutative inverse_closed invertible 
    invertible_right_inverse2)

lemma additive_quadruple_diff:
  assumes "additive_quadruple a b c d"
  shows "a ⊖ c = d ⊖ b"
  by (smt (verit, del_insts) additive_quadruple_def assms associative commutative 
      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 a b c d}"

lemma additive_quadruple_set_sub:
  "additive_quadruple_set A ⊆ {(a, b, c, d) | a b c d. d = a ⊕ b ⊖ c ∧ a ∈ A ∧ b ∈ A ∧ 
    c ∈ A ∧ d ∈ A}" using additive_quadruple_set_def additive_quadruple_def additive_quadruple_aux 
  by auto

definition additive_energy:: "'a set ⇒ real" where 
  "additive_energy A ≡ card (additive_quadruple_set A) / (card A)^3" 

lemma card_ineq_aux_quadruples:
  assumes "finite A"
  shows "card (additive_quadruple_set A) ≤ (card A)^3"

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})"
    using card_mono inj_on_finite[of "f"] assms additive_quadruple_set_sub finite_SigmaI
    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
  
lemma additive_energy_upper_bound: "additive_energy A ≤ 1"

proof (cases "finite A")
  assume hA: "finite A"
  show ?thesis unfolding additive_energy_def using card_ineq_aux_quadruples hA 
    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 
     additive_abelian_group_axioms commutative invertible invertible_left_inverse2 subsetD)
  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)


lemma pairwise_disjnt_quadruple_sum:
  "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)

lemma quadruple_sum_Union_eq:
   "⋃ ((λ 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"
    unfolding additive_quadruple_set_def by (intro Union_least) (auto)
next
  show "additive_quadruple_set A ⊆ (⋃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})"
  unfolding additive_quadruple_set_def additive_quadruple_def by (intro subsetI) (auto)
qed

lemma f_sum_card_quadruple_set: 
  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


lemma  f_sum_card_quadruple_set_additive_energy: assumes "A ⊆ G" and "finite A"
  shows "(∑ d ∈ sumset A A. (f_sum d A)^2) = additive_energy A * (card A)^3"
  using assms f_sum_card_quadruple_set additive_energy_def by force


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
      have "additive_quadruple a b c d"
        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)

lemma pairwise_disjnt_quadruple_diff:
 "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)

lemma quadruple_diff_Union_eq:
  "⋃ ((λ 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)) = 
    additive_quadruple_set A"

proof
  show "(⋃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}) ⊆ additive_quadruple_set A"
    unfolding additive_quadruple_set_def by (intro Union_least)(auto)
next
  show "additive_quadruple_set A ⊆ (⋃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})"
  proof (intro subsetI)
    fix x assume"x ∈ additive_quadruple_set A"
    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" 
      and hx4: "x4 ∈ A" and hxadd: "additive_quadruple x1 x2 x3 x4" 
      using additive_quadruple_set_def by auto
    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}"
      using additive_quadruple_diff hx1 hx2 hx3 hx4 hxadd by auto
    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})"
      using hx hxmem hx1 hx3 additive_quadruple_def hxadd by auto
  qed
qed

lemma f_diff_card_quadruple_set: 
  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


lemma f_diff_card_quadruple_set_additive_energy: assumes "A ⊆ G" and "finite A"
  shows "(∑ d ∈ differenceset A A. (f_diff d A)^2) = additive_energy A * (card A)^3"
  using assms f_diff_card_quadruple_set additive_energy_def by force

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

definition popular_diff_set:: "real ⇒ 'a set ⇒ 'a set" where
  "popular_diff_set θ A ≡ {d ∈ differenceset A A. popular_diff d θ A}"

end
end