Theory Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality

section‹The Pl\"{u}nnecke-Ruzsa Inequality›

text‹Authors: Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson, University of Cambridge.›

text‹We formalise Pl\"{u}nnecke's inequality and the Pl\"{u}nnecke-Ruzsa inequality, 
following the notes by Timothy Gowers: "Introduction to Additive
Combinatorics" (2022) for the University of Cambridge. To this end, we first introduce basic definitions
and prove elementary facts on sumsets and difference sets. Then, we show (two versions of)
the Ruzsa triangle inequality. We follow with a proof due to Petridis. ›

theory Pluennecke_Ruzsa_Inequality
  imports
    "Jacobson_Basic_Algebra.Ring_Theory"
    Complex_Main

begin

notation plus (infixl "+" 65)
notation minus (infixl "-" 65)
notation uminus ("- _" [81] 80)

subsection ‹Key definitions (sumset, difference set) and basic lemmas ›

text ‹Working in an arbitrary Abelian group, with additive syntax›

locale additive_abelian_group = abelian_group G "(⊕)" 𝟬
  for G and addition (infixl "⊕" 65)  and zero ("𝟬") 

begin

abbreviation G_minus:: "'a ⇒ 'a ⇒ 'a" (infixl "⊖" 70)
  where "x ⊖ y ≡ x ⊕ inverse y "

lemma inverse_closed: "x ∈ G ⟹ inverse x ∈ G"
  by blast


subsubsection ‹Sumsets›

inductive_set sumset :: "'a set ⇒ 'a set ⇒ 'a set" for A B
  where
    sumsetI[intro]: "⟦a ∈ A; a ∈ G; b ∈ B; b ∈ G⟧ ⟹ a ⊕ b ∈ sumset A B"

lemma sumset_eq: "sumset A B = {c. ∃a ∈ A ∩ G. ∃b ∈ B ∩ G. c = a ⊕ b}"
  by (auto simp: sumset.simps elim!: sumset.cases)

lemma sumset: "sumset A B = (⋃a ∈ A ∩ G. ⋃b ∈ B ∩ G. {a ⊕ b})"
  by (auto simp: sumset_eq)

lemma sumset_subset_carrier: "sumset A B ⊆ G"
  by (auto simp: sumset_eq)

lemma sumset_Int_carrier [simp]: "sumset A B ∩ G = sumset A B"
  by (simp add: Int_absorb2 sumset_subset_carrier)

lemma sumset_mono: "⟦A' ⊆ A; B' ⊆ B⟧ ⟹ sumset A' B' ⊆ sumset A B"
  by (auto simp: sumset_eq)

lemma sumset_insert1: "NO_MATCH {} A ⟹ sumset (insert x A) B = sumset {x} B ∪ sumset A B"
  by (auto simp: sumset_eq)

lemma sumset_insert2: "NO_MATCH {} B ⟹ sumset A (insert x B) = sumset A {x} ∪ sumset A B"
  by (auto simp: sumset_eq)

lemma sumset_subset_Un1: "sumset (A ∪ A') B = sumset A B ∪ sumset A' B"
  by (auto simp: sumset_eq)

lemma sumset_subset_Un2: "sumset A (B ∪ B') = sumset A B ∪ sumset A B'"
  by (auto simp: sumset_eq)

lemma sumset_subset_insert: "sumset A B ⊆ sumset A (insert x B)" "sumset A B ⊆ sumset (insert x A) B"
  by (auto simp: sumset_eq)

lemma sumset_subset_Un: "sumset A B ⊆ sumset A (B∪C)" "sumset A B ⊆ sumset (A∪C) B"
  by (auto simp: sumset_eq)

lemma sumset_empty [simp]: "sumset A {} = {}" "sumset {} A = {}"
  by (auto simp: sumset_eq)

lemma sumset_empty':
  assumes "A ∩ G = {}"
  shows "sumset B A = {}" "sumset A B = {}"
  using assms by (auto simp: sumset_eq)

lemma sumset_is_empty_iff [simp]: "sumset A B = {} ⟷ A ∩ G = {} ∨ B ∩ G = {}"
  by (auto simp: sumset_eq)

lemma sumset_D [simp]: "sumset A {𝟬} = A ∩ G" "sumset {𝟬} A = A ∩ G"
  by (auto simp: sumset_eq)

lemma sumset_Int_carrier_eq [simp]: "sumset A (B ∩ G) = sumset A B" "sumset (A ∩ G) B = sumset A B"
  by (auto simp: sumset_eq)

lemma sumset_assoc:
  shows "sumset (sumset A B) C = sumset A (sumset B C)"
  by (fastforce simp add: sumset_eq associative Bex_def)

lemma sumset_commute:
  shows "sumset A B = sumset B A"
  by (auto simp: sumset_eq; meson Int_iff commutative)

lemma finite_sumset:
  assumes "finite A" "finite B"  shows "finite (sumset A B)"
  using assms by (auto simp: sumset_eq)

lemma finite_sumset':
  assumes "finite (A ∩ G)" "finite (B ∩ G)"
    shows "finite (sumset A B)"
  using assms by (auto simp: sumset_eq)

lemma sumsetdiff_sing: "sumset (A - B) {x} = sumset A {x} - sumset B {x}"
  by (auto simp: sumset_eq)

lemma card_sumset_singleton_eq:
  assumes "finite A" shows "card (sumset A {a}) = (if a ∈ G then card (A ∩ G) else 0)"
proof (cases "a ∈ G")
  case True
  then have "sumset A {a} = (λx. x ⊕ a) ` (A ∩ G)"
    by (auto simp: sumset_eq)
  moreover have "inj_on (λx. x ⊕ a) (A ∩ G)"
    by (auto simp: inj_on_def True)
  ultimately show ?thesis
    by (metis True card_image)
qed (auto simp: sumset_eq)

lemma card_sumset_le:
  assumes "finite A" shows "card (sumset A {a}) ≤ card A"
  by (simp add: assms card_mono card_sumset_singleton_eq)

lemma infinite_sumset_aux:
  assumes "infinite (A ∩ G)"
  shows "infinite (sumset A B) ⟷ B ∩ G ≠ {}"
proof (cases "B ∩ G = {}")
  case False
  then obtain b where b: "b ∈ B" "b ∈ G" by blast
  with assms commutative have "((⊕)b) ` (A ∩ G) ⊆ sumset A B"
    by (auto simp: sumset)
  moreover have "inj_on ((⊕)b) (A ∩ G)"
    by (meson IntD2 b inj_onI invertible invertible_left_cancel)
  ultimately show ?thesis
    by (metis False assms inj_on_finite)
qed (auto simp: sumset_eq)

lemma infinite_sumset_iff:
  shows  "infinite (sumset A B) ⟷ infinite (A ∩ G) ∧ B ∩ G ≠ {} ∨ A ∩ G ≠ {} ∧ infinite (B ∩ G)"
  by (metis (no_types, lifting) finite_sumset' infinite_sumset_aux sumset_commute)

lemma card_le_sumset:
  assumes A: "finite A" "a ∈ A" "a ∈ G"
    and   B: "finite B" "B ⊆ G"
  shows "card B ≤ card (sumset A B)"
proof -
  have "B ⊆ (⊕) (inverse a) ` sumset A B"
    using A B
    apply (clarsimp simp: sumset image_iff)
    by (metis Int_absorb2 Int_iff invertible invertible_left_inverse2)
  with A B show ?thesis
    by (meson  finite_sumset surj_card_le)
qed

lemma card_sumset_0_iff': "card (sumset A B) = 0 ⟷ card (A ∩ G) = 0 ∨ card (B ∩ G) = 0"
proof (cases "infinite (A ∩ G) ∨ infinite (B ∩ G)")
  case True
  then show ?thesis
    by (metis card_eq_0_iff infinite_sumset_iff sumset_empty')
qed (auto simp: sumset_eq)

lemma card_sumset_0_iff:
  assumes "A ⊆ G" "B ⊆ G"
  shows "card (sumset A B) = 0 ⟷ card A = 0 ∨ card B = 0"
  by (metis assms le_iff_inf card_sumset_0_iff')

lemma card_sumset_leq:
  assumes "A ⊆ G"
  shows "card(sumset A A) ≤ Suc(card A) choose 2"
  using assms
proof (induction "card A" arbitrary: A)
  case 0
  then show ?case
    by (metis card_sumset_0_iff zero_le)
next
  case (Suc n A)
  then obtain a A' where a: "a ∈ A" "A' = A - {a}" "a ∈ G"
    by (metis Zero_neq_Suc card_eq_0_iff subset_empty subset_eq)
  then have n: "card A' = n"
    by (metis Suc(2) card_Diff_singleton diff_Suc_Suc minus_nat.diff_0 One_nat_def)
  have "finite A"
    by (metis Suc(2) Zero_neq_Suc card.infinite)
  have "card (sumset A A) ≤ card (sumset A' A') + card A"
  proof -
    have A: "A = A' ∪ {a}"
      using a by auto
    then have "sumset A A = (sumset A' A') ∪ (sumset A {a})"
      by (auto simp: sumset_eq commutative)
    with a ‹finite A› card_sumset_le show ?thesis
      by (simp add: order_trans[OF card_Un_le])
  qed
  also have "… ≤ (card A) choose 2 + card A"
    using Suc a by (metis add_le_mono1 insert_Diff_single insert_absorb insert_subset n)
  also have "… ≤ Suc (card A) choose 2"
    by (simp add: numeral_2_eq_2)
  finally show ?case .
qed


subsubsection ‹Iterated sumsets›

definition sumset_iterated :: "'a set ⇒ nat ⇒ 'a set"
  where "sumset_iterated A r ≡ Finite_Set.fold (sumset ∘ (λ_. A)) {𝟬} {..<r}"

lemma sumset_iterated_0 [simp]: "sumset_iterated A 0 = {𝟬}"
  by (simp add: sumset_iterated_def)

lemma sumset_iterated_Suc [simp]: "sumset_iterated A (Suc k) = sumset A (sumset_iterated A k)"
  (is "?lhs = ?rhs")
proof -
  interpret comp_fun_commute_on "{..k}" "sumset ∘ (λ_. A)"
    using sumset_assoc sumset_commute by (auto simp: comp_fun_commute_on_def)
  have "?lhs = (sumset ∘ (λ_. A)) k (Finite_Set.fold (sumset ∘ (λ_. A)) {𝟬} {..<k})"
    unfolding sumset_iterated_def lessThan_Suc
    by (subst fold_insert, auto)
  also have "… = ?rhs"
    by (simp add: sumset_iterated_def)
  finally show ?thesis .
qed

lemma sumset_iterated_2:
  shows "sumset_iterated A 2 = sumset A A"
  by (simp add: eval_nat_numeral)

lemma sumset_iterated_r: "r > 0 ⟹ sumset_iterated A r = sumset A (sumset_iterated A (r-1))"
  using gr0_conv_Suc by force

lemma sumset_iterated_subset_carrier: "sumset_iterated A k ⊆ G"
  by (cases k; simp add: sumset_subset_carrier)

lemma finite_sumset_iterated: "finite A ⟹ finite (sumset_iterated A r)"
  by(induction r) (auto simp: finite_sumset)

lemma sumset_iterated_empty: "r>0 ⟹ sumset_iterated {} r = {}"
  by (induction r) auto

subsubsection ‹Difference sets›

inductive_set minusset :: "'a set ⇒ 'a set" for A
  where
    minussetI[intro]: "⟦a ∈ A; a ∈ G⟧ ⟹ inverse a ∈ minusset A"

lemma minusset_eq: "minusset A = inverse ` (A ∩ G)"
  by (auto simp: minusset.simps)


abbreviation "differenceset A B ≡ sumset A (minusset B)"

lemma minusset_is_empty_iff [simp]: "minusset A = {} ⟷ A ∩ G = {}"
  by (auto simp: minusset_eq)

lemma minusset_triv [simp]: "minusset {𝟬} = {𝟬}"
  by (auto simp: minusset_eq)

lemma minusset_subset_carrier: "minusset A ⊆ G"
  by (auto simp: minusset_eq)

lemma minus_minusset [simp]: "minusset (minusset A) = A ∩ G"
  apply (auto simp: minusset_eq)
  by (metis inverse_equality invertible invertibleE minusset.minussetI minusset_eq)

lemma card_minusset [simp]: "card (minusset A) = card (A ∩ G)"
proof (rule bij_betw_same_card)
  show "bij_betw (inverse) (minusset A) (A ∩ G)"
    unfolding minusset_eq by (force intro: bij_betwI)
qed

lemma card_minusset': "A ⊆ G ⟹ card (minusset A) = card A"
  by (simp add: Int_absorb2)

lemma diff_minus_set:
  "differenceset (minusset A) B = minusset (sumset A B)" (is "?lhs = ?rhs")
proof (rule Set.set_eqI)
  fix u
  have "u ∈ ?lhs ⟷
          (∃x ∈ A ∩ G. ∃y ∈ B ∩ G. u = inverse x ⊖ y)"
    by (auto simp: sumset minusset_eq)
  also have "… ⟷ (∃x ∈ A ∩ G. ∃y ∈ B ∩ G. u = inverse (y ⊕ x))"
    using inverse_composition_commute by auto
  also have "… ⟷ u ∈ ?rhs"
    by (auto simp: sumset minusset_eq commutative)
  finally show "u ∈ ?lhs ⟷ u ∈ ?rhs" .
qed

lemma differenceset_commute [simp]:
  shows "minusset (differenceset B A) = differenceset A B "
  by (metis diff_minus_set minus_minusset sumset_Int_carrier_eq(1) sumset_commute)

lemma card_differenceset_commute: "card (differenceset B A) = card (differenceset A B)"
    by (metis card_minusset' differenceset_commute sumset_subset_carrier)

lemma minusset_distrib_sum:
  shows "minusset (sumset A B) = sumset (minusset A) (minusset B)"
  by (simp add: diff_minus_set)

lemma minusset_iterated_minusset: "sumset_iterated (minusset A) k = minusset (sumset_iterated A k)"
  by (induction k) (auto simp: diff_minus_set)

lemma card_sumset_iterated_minusset:
  "card (sumset_iterated (minusset A) k) = card (sumset_iterated A k)"
  by (metis card_minusset' minusset_iterated_minusset sumset_iterated_subset_carrier)

lemma finite_minusset: "finite A ⟹ finite (minusset A)"
  by (simp add: minusset_eq)

lemma finite_differenceset: "finite A ⟹ finite B ⟹ finite (differenceset A B)"
  by (simp add: finite_minusset finite_sumset)


subsection‹The Ruzsa triangle inequality›

lemma Ruzsa_triangle_ineq1:
  assumes U: "finite U" "U ⊆ G"
    and   V: "finite V" "V ⊆ G"
    and   W: "finite W" "W ⊆ G"
  shows "(card U) * card(differenceset V W) ≤ card (differenceset U V) * card (differenceset U W)"
proof -
  have fin:  "finite (differenceset U V)" "finite (differenceset U W)"
    using U V W finite_minusset finite_sumset by auto
  have "∃v w. v ∈ V ∧ w ∈ W ∧ x = v ⊖ w" if "x ∈ differenceset V W" for x
    using that by (auto simp: sumset_eq minusset_eq)
  then obtain v w where vinV: "v x ∈ V" and winW: "w x ∈ W" and vw_eq: "v x ⊖ (w x) = x"
    if "x ∈ differenceset V W" for x    by metis
  have vinG: "v x ∈ G" and winG: "w x ∈ G" if "x ∈ differenceset V W" for x
    using V W that vinV winW by auto
  define φ where "φ ≡ λ(u,x). (u ⊖ (v x), u ⊖ (w x))"
  have "inj_on φ (U × differenceset V W)"
  proof (clarsimp simp add: φ_def inj_on_def)
    fix u1 :: 'a and x1 :: 'a and u2 :: 'a and x2 :: 'a
    assume "u1 ∈ U" "u2 ∈ U"
      and x1: "x1 ∈ differenceset V W"
      and x2: "x2 ∈ differenceset V W"
      and v: "u1 ⊖ v x1 = u2 ⊖ v x2"
      and w: "u1 ⊖ w x1 = u2 ⊖ w x2"
    then obtain "u1 ∈ G" "u2 ∈ G" "x1 ∈ G" "x2 ∈ G"
      by (meson ‹U ⊆ G› subset_iff sumset_subset_carrier)
    show "u1 = u2 ∧ x1 = x2"
    proof
      have "v x1 ⊖ w x1 = (u1 ⊖ w x1) ⊖ (u1 ⊖ v x1)"
        by (smt (verit, del_insts) ‹u1 ∈ G› associative commutative composition_closed inverse_closed 
            invertible invertible_right_inverse2 vinG winG x1)
      also have "… = (u2 ⊖ w x2) ⊖ (u2 ⊖ v x2)"
        using v w by presburger
      also have "… = v x2 ⊖ w x2"
        by (smt (verit, del_insts) ‹u2 ∈ G› associative commutative composition_closed inverse_equality 
            invertible invertible_def invertible_right_inverse2 vinG winG x2)
      finally have "v x1 ⊖ w x1 = v x2 ⊖ w x2" .
      then show "x1=x2"
        by (simp add: x1 x2 vw_eq)
      then show "u1=u2"
        using ‹u1 ∈ G› ‹u2 ∈ G› w winG x1 by force
    qed
  qed
  moreover have "φ ∈ (U × differenceset V W) → (differenceset U V) × (differenceset U W)"
    using ‹U ⊆ G› ‹V ⊆ G› ‹W ⊆ G›
    by (fastforce simp: φ_def intro: vinV winW)
  ultimately have "card (U × differenceset V W) ≤ card (differenceset U V × differenceset U W)"
    using card_inj fin by blast
  then show ?thesis
    by (simp flip: card_cartesian_product)
qed



definition Ruzsa_distance:: "'a set ⇒ 'a set ⇒ real"
    where "Ruzsa_distance A B ≡ card(differenceset A B)/(sqrt(card A) * sqrt(card B))"

lemma Ruzsa_triangle_ineq2:
  assumes U: "finite U" "U ⊆ G" "U ≠ {}"
    and   V: "finite V" "V ⊆ G"
    and   W: "finite W" "W ⊆ G"
  shows "Ruzsa_distance V W ≤ (Ruzsa_distance V U) * (Ruzsa_distance U W)"
proof -
  have  "card U * card (differenceset V W) ≤ card (differenceset U V) * card (differenceset U W)"
    using assms Ruzsa_triangle_ineq1 by metis
  ―‹now divide both sides with the same quantity›
  then have "card U * card (differenceset V W) / (card U * sqrt (card V) * sqrt (card W))
         ≤ card (differenceset U V) * card (differenceset U W) / (card U * sqrt (card V) * sqrt (card W))"
    using assms
    by (metis divide_right_mono mult_eq_0_iff mult_left_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_0_iff)
  then have *: "card(differenceset V W) / (sqrt(card V) * sqrt(card W)) ≤
                card (differenceset U V) * card (differenceset U W)
                / (card U * sqrt(card V) * sqrt(card W))"
    using assms by simp
  have "card (differenceset U V) * card (differenceset U W)/(card U * sqrt(card V) * sqrt(card W))
                  = card(differenceset V U) / (sqrt(card U) * sqrt(card V))*
                    card(differenceset U W) / (sqrt(card U) * sqrt(card W))"
    using assms
    by (simp add: divide_simps) (metis card_minusset differenceset_commute minus_minusset)
  then have
     "card(differenceset V W) / (sqrt(card V) * sqrt(card W)) ≤
       card(differenceset V U) / (sqrt(card U) * sqrt(card V)) *
       card(differenceset U W) / (sqrt(card U) * sqrt(card W))"
    using * assms by auto
  then show ?thesis unfolding Ruzsa_distance_def
    by (metis divide_divide_eq_left divide_divide_eq_left' times_divide_eq_right)
qed


subsection ‹Petridis's proof of the Pl\"{u}nnecke-Ruzsa inequality ›

lemma Plu_2_2:
  assumes K0: "card (sumset A0 B) ≤ K0 * real (card A0)"
    and   A0: "finite A0" "A0 ⊆ G" "A0 ≠ {}"
    and   B: "finite B" "B ⊆ G" "B ≠ {}"
  obtains A K
    where "A ⊆ A0" "A ≠ {}" "0 < K" "K ≤ K0"
      and "⋀C. C ⊆ G ⟹ finite C ⟹ card (sumset A (sumset B C)) ≤ K * real (card(sumset A C))"
proof
  define KS where "KS ≡ (λA. card (sumset A B) / real (card A)) ` (Pow A0 - {{}})"
  define K where "K ≡ Min KS"
  define A where "A ≡ @A. A ∈ Pow A0 - {{}} ∧ K = card (sumset A B) / real (card A)"
  obtain KS: "finite KS" "KS ≠ {}"
    using KS_def A0 by blast
  then have "K ∈ KS"
    using K_def Min_in by blast
  then have "∃A. A ∈ Pow A0 - {{}} ∧ K = card (sumset A B) / real (card A)"
    using KS_def by blast
  then obtain "A ∈ Pow A0 - {{}}" and Keq: "K = card (sumset A B) / real (card A)"
    by (metis (mono_tags, lifting) A_def someI_ex)
  then show A: "A ⊆ A0" "A ≠ {}"
    by auto
  with A0 finite_subset have "A ⊆ G" "finite A"
    by blast+
  have gt0: "0 < real (card (sumset A B)) / real (card A)" if "A ≠ {}" and "A ⊆ A0" for A
    using that assms
    by (smt (verit, best) order_trans card_0_eq card_sumset_0_iff divide_pos_pos of_nat_le_0_iff finite_subset)
  then show "K > 0"
    using A Keq by presburger
  have K_cardA: "K * (card A) = card (sumset A B)"
    unfolding Keq using Keq ‹0 < K› by force
  have K_le: "real (card (sumset A' B)) / card A' ≥ K" if "A' ⊆ A" "A' ≠ {}" for A'
    using KS K_def KS_def ‹A ⊆ A0› that by force
  with A0 have "card (sumset A0 B) / real (card A0) ∈ KS"
    by (auto simp: KS_def)
  with A0 show "K ≤ K0"
    by (metis KS K_def Min_le_iff card_gt_0_iff mult_imp_div_pos_le of_nat_0_less_iff K0)
  show "card (sumset A (sumset B C)) ≤ K * real (card(sumset A C))"
    if "finite C" "C ⊆ G" for C
    using that
  proof (induction C)
    case empty
    then show ?case by simp
      ― ‹This is actually trivial: it does not follow from @{term "card (sumset A B) = K * card A"} 
         as claimed in the notes.›
  next
    case (insert x C)
    then have "x ∈ G" "C ⊆ G" "finite C"
      by auto
    define A' where "A' ≡ A ∩ {a. (a⊕x) ∈ sumset A C}"
    with ‹finite A› have "finite A'" "A' ⊆ A" by auto
    then have [simp]: "real (card A - card A') = real (card A) - real (card A')"
      by (meson ‹finite A› card_mono of_nat_diff)
    have 0: "sumset A C ∩ sumset (A - A') {x} = {}"
      by (clarsimp simp add: A'_def sumset_eq disjoint_iff) (metis IntI)
    have 1: "sumset A (insert x C) = sumset A C ∪ sumset (A - A') {x}"
      by (auto simp: A'_def sumset_eq)
    have "card (sumset A (insert x C)) = card (sumset A C) + card (sumset (A - A') {x})"
      by (simp add: 0 1 ‹finite A› card_Un_disjoint finite_sumset local.insert)
    also have "… = card (sumset A C) + card ((A - A') ∩ G)"
      using ‹finite A› ‹x ∈ G› by (simp add: card_sumset_singleton_eq)
    also have "… = card (sumset A C) + card (A - A')"
      by (metis  ‹A ⊆ G› Int_absorb2 Int_Diff Int_commute)
    also have "… = card (sumset A C) + (card A - card A')"
      by (simp add: A'_def ‹finite A› card_Diff_subset)
    finally have *: "card (sumset A (insert x C)) = card (sumset A C) + (card A - card A')" .
    have "sumset A' (sumset B {x}) ⊆ sumset A (sumset B C)"
      by (clarsimp simp add: A'_def sumset_eq Bex_def) (metis associative commutative composition_closed) 
    then have "sumset A (sumset B (insert x C))
                 ⊆ sumset A (sumset B C) ∪ (sumset A (sumset B {x}) - sumset A' (sumset B {x}))"
      by (auto simp: sumset_insert2 sumset_subset_Un2)
    then have "card (sumset A (sumset B (insert x C))) ≤ card (sumset A (sumset B C))
                           + card ((sumset A (sumset B {x}) - sumset A' (sumset B {x})))"
      by (smt (verit, best) B(1) ‹finite A› ‹finite C› order_trans card_Un_le card_mono finite.emptyI
              finite.insertI finite_Diff finite_Un finite_sumset)
    also have "… = card (sumset A (sumset B C)) + (card (sumset A (sumset B {x})) - card (sumset A' (sumset B {x})))"
      by (simp add: ‹A' ⊆ A› ‹finite A'› ‹finite B› card_Diff_subset finite_sumset sumset_mono)
    also have "… ≤ card (sumset A (sumset B C)) + (card (sumset A B) - card (sumset A' B))"
      using ‹finite A› ‹finite A'› ‹finite B› by (simp add: card_sumset_singleton_eq finite_sumset flip: sumset_assoc)
    also have "… ≤ K * card (sumset A C) + (K * card A - K * card A')"
    proof (cases "A' =  {}")
      case True
      with local.insert ‹C ⊆ G› K_cardA show ?thesis by auto
    next
      case False
      then have "K * card A' ≤ real (card (sumset A' B))"
        using K_le[OF ‹A' ⊆ A›] by (simp add: divide_simps split: if_split_asm)
      then have "real (card (sumset A B) - card (sumset A' B)) ≤ K * real (card A) - K * real (card A')"
        by (simp add: B(1) K_cardA ‹A' ⊆ A› ‹finite A› card_mono finite_sumset of_nat_diff sumset_mono)
      with local.insert show ?thesis by simp
    qed
    also have "… ≤ K * real (card (sumset A (insert x C)))"
      using * ‹A' ⊆ A› by (simp add: algebra_simps)
    finally show ?case
      using of_nat_mono by blast
  qed
qed

lemma Cor_Plu_2_3:
  assumes K: "card (sumset A B) ≤ K * real (card A)"
    and   A: "finite A" "A ⊆ G" "A ≠ {}"
    and   B: "finite B" "B ⊆ G" 
  obtains A' where "A' ⊆ A" "A' ≠ {}"
                   "⋀r. card (sumset A' (sumset_iterated B r)) ≤ K^r * real (card A')"
proof (cases "B = {}")
  case True
  have "K ≥ 0"
    using assms by (simp add: True zero_le_mult_iff)
  moreover have *: "sumset_iterated B r = (if r=0 then {𝟬} else {})" for r
    by (metis True sumset_iterated_0 sumset_iterated_empty zero_less_iff_neq_zero)
  ultimately have "real (card (sumset A (sumset_iterated B r)))
          ≤ K ^ r * real (card A)" for r
    by (simp add: "*" Int_commute  Int_absorb2 ‹A ⊆ G›)
  with ‹A ≠ {}› that show ?thesis by blast
next
  case False
  obtain A' K'
    where A': "A' ⊆ A" "A' ≠ {}" "0 < K'" "K' ≤ K"
      and A'_card: "⋀C. C ⊆ G ⟹ finite C ⟹ card (sumset A' (sumset B C)) ≤ K' * real (card(sumset A' C))"
    by (metis A B Plu_2_2 K False)
  with A have "A' ⊆ G" by blast
  have *: "card (sumset A' (sumset_iterated B (Suc r))) ≤ K' * card (sumset A' (sumset_iterated B r))" 
          (is "?lhs ≤ ?rhs")
    for r
  proof -
    have "?lhs = card (sumset A' (sumset B (sumset_iterated B r)))"
      using that by (simp add: sumset_iterated_r)
    also have "… ≤ ?rhs"
      using A'_card B finite_sumset_iterated sumset_iterated_subset_carrier by meson
    finally show ?thesis .
  qed
  have **: "card (sumset A' (sumset_iterated B r)) ≤ K'^r * real (card A')" for r
  proof (induction r)
    case 0
    with ‹A' ⊆ G› show ?case
      by (simp add: Int_absorb2)
  next
    case (Suc r)
    then show ?case
      by (smt (verit) "*" ‹0 < K'› mult.commute mult.left_commute mult_le_cancel_left_pos power_Suc)
  qed
  show thesis
  proof
    show "real (card (sumset A' (sumset_iterated B r))) ≤ K ^ r * real (card A')" for r
      by (meson "**" A' order_trans less_eq_real_def mult_right_mono of_nat_0_le_iff power_mono)
  qed (use A' in auto)
qed


text‹The following Corollary of the above is an important special case,
also referred to as the original version of Pl\"{u}nnecke's inequality first shown by Pl\"{u}nnecke. ›

lemma Cor_Plu_2_3_Pluennecke_ineq:
  assumes K: "card (sumset A B) ≤ K * real (card A)"
    and   A: "finite A" "A ⊆ G" "A ≠ {}"
    and   B: "finite B" "B ⊆ G"
  shows "real (card (sumset_iterated B r)) ≤ K ^ r * real (card A)"
proof-
  obtain A' where *:"A' ⊆ A" "A' ≠ {}"
    "card (sumset A' (sumset_iterated B r)) ≤ K^r * real (card A')"
    using assms Cor_Plu_2_3 by metis
  with assms have  **: "card (sumset_iterated B r) ≤ card (sumset A' (sumset_iterated B r))"
    by (meson card_le_sumset finite_subset finite_sumset_iterated subset_empty subset_iff sumset_iterated_subset_carrier)
  with * show ?thesis
    by (smt (verit, best) A(1) K card_mono mult_left_mono of_nat_0_le_iff of_nat_le_iff zero_le_mult_iff zero_le_power)
qed

text ‹Special case where @{term "B=A"}›
lemma Cor_Plu_2_3_1:
  assumes K: "card (sumset A A) ≤ K * real (card A)"
    and   A: "finite A" "A ⊆ G" "A ≠ {}"
  shows "card (sumset_iterated A r) ≤ K^r * real (card A)"
proof -
  have "K > 0"
    by (meson A K Plu_2_2 less_le_trans)
  obtain A' where A': "A' ⊆ A" "A' ≠ {}"
    and A'_card: "⋀r. card (sumset A' (sumset_iterated A r)) ≤ K^r * real (card A')"
    by (meson A Cor_Plu_2_3 K)
  with A obtain a where "a ∈ A'" "a ∈ G" "finite A'"
    by (metis ex_in_conv finite_subset subset_iff)
  then have "card (sumset_iterated A r) ≤ card (sumset A' (sumset_iterated A r))"
    using A card_le_sumset finite_sumset_iterated sumset_iterated_subset_carrier by meson
  also have "… ≤ K^r * real (card A')"
    using A'_card by meson
  also have "… ≤ K^r * real (card A)"
    by (simp add: ‹A' ⊆ A› ‹finite A› ‹0 < K› card_mono)
  finally show ?thesis
    by linarith
qed


text ‹Special case where @{term "B=-A"}›
lemma Cor_Plu_2_3_2:
  assumes K: "card (differenceset A A) ≤ K * real (card A)"
    and   A: "finite A" "A ⊆ G" "A ≠ {}"
  shows "card (sumset_iterated A r) ≤ K^r * real (card A)"
proof -
  have "card A > 0"
    by (simp add: A card_gt_0_iff)
  with K have "K ≥ 0"
    by (smt (verit, del_insts) of_nat_0_less_iff of_nat_less_0_iff zero_le_mult_iff)
  obtain A' where A': "A' ⊆ A" "A' ≠ {}"
    and A'_card: "⋀r. card (sumset A' (sumset_iterated (minusset A) r)) ≤ K^r * real (card A')"
    by (metis A Cor_Plu_2_3 assms(1) card_eq_0_iff card_minusset' minusset_subset_carrier)
  with A obtain a where "a ∈ A'" "a ∈ G" "finite A'"
    by (metis ex_in_conv finite_subset subset_iff)
  then have "card (sumset_iterated A r) ≤ card (sumset A' (sumset_iterated (minusset A) r))"
    by (metis A(1) card_le_sumset card_sumset_iterated_minusset finite_minusset finite_sumset_iterated sumset_iterated_subset_carrier)
  also have "… ≤ K^r * real (card A')"
    using A'_card by meson
  also have "… ≤ K^r * real (card A)"
    by (simp add: ‹A' ⊆ A› ‹finite A› ‹0 ≤ K› card_mono mult_left_mono)
  finally show ?thesis
    by linarith
qed

text ‹The following result is known as the Pl\"{u}nnecke-Ruzsa inequality (Theorem 2.5
in Gowers's notes). The proof will make use of the Ruzsa triangle inequality.›

theorem Pluennecke_Ruzsa_ineq:
  assumes K:  "card (sumset A B) ≤ K * real (card A)"
    and   A: "finite A" "A ⊆ G" "A ≠ {}"
    and   B: "finite B" "B ⊆ G" 
    and "0 < r" "0 < s"
  shows "card (differenceset (sumset_iterated B r) (sumset_iterated B s)) ≤ K^(r+s) * real(card A)"
proof -
  have "card A > 0"
    by (simp add: A card_gt_0_iff)
  with K have "K ≥ 0"
    by (smt (verit, del_insts) of_nat_0_less_iff of_nat_less_0_iff zero_le_mult_iff)
  obtain A' where A': "A' ⊆ A" "A' ≠ {}"
    and A'_le: "⋀r. card (sumset A' (sumset_iterated B r)) ≤ K^r * real (card A')"
    using  Cor_Plu_2_3 assms by metis
  define C where "C ≡ minusset A'"
  have "minusset C = A'" and "C ≠{}" and cardA: "card A' ≤ card A" and cardC: "card C = card A'"
    using A' A card_mono by (auto simp: C_def card_minusset' Int_absorb2)
  then have cardCA: "card C ≤ card A" by linarith
  have "⋀r. card (differenceset C (sumset_iterated B r)) ≤ K^r * real (card A')"
    using A'_le C_def card_minusset' diff_minus_set sumset_subset_carrier by presburger
  then have r: "card (differenceset C (sumset_iterated B r)) ≤ K^r * real (card C)"
    and  s: "card (differenceset C (sumset_iterated B s)) ≤ K^s * real (card C)"
    using cardC by presburger+
  have "card C > 0"
    by (metis A' ‹finite A› cardC card_gt_0_iff finite_subset)
  moreover have "C ⊆ G"
    by (simp add: C_def minusset_subset_carrier)
  ultimately have "card C * card (differenceset (sumset_iterated B r) (sumset_iterated B s))
        ≤ card (differenceset C (sumset_iterated B r)) *
           card (differenceset C (sumset_iterated B s))"
    by (meson Ruzsa_triangle_ineq1 B card_gt_0_iff finite_sumset_iterated sumset_iterated_subset_carrier)
  also have "… ≤ K^(r+s) * card C * card C"
    using mult_mono [OF r s] ‹0 ≤ K› by (simp add: power_add field_simps)
  finally have "card (differenceset (sumset_iterated B r) (sumset_iterated B s)) ≤ K^(r+s) * card C"
    using ‹card C > 0› by (simp add: field_simps)
  then show ?thesis
    by (smt (verit, ccfv_SIG) ‹0 ≤ K› cardA cardC mult_left_mono of_nat_mono zero_le_power)
qed

text ‹The following is an alternative version of the Pl\"{u}nnecke-Ruzsa inequality (Theorem 2.1
in Gowers's notes).›

theorem Pluennecke_Ruzsa_ineq_alt:
  assumes "finite A" "A ⊆ G"
    and "card (sumset A A) ≤ K * real (card A)" "r > 0" "s > 0"
  shows "card (differenceset (sumset_iterated A r) (sumset_iterated A s)) ≤ K^(r+s) * real(card A)"
proof (cases "A = {}")
  case True
  then have "sumset_iterated A r = {}" if "r>0" for r
    using sumset_iterated_empty that by force
  with assms show ?thesis
    by (auto simp: True)
next
  case False
  with assms Pluennecke_Ruzsa_ineq show ?thesis by presburger
qed

theorem Pluennecke_Ruzsa_ineq_alt_2:
  assumes "finite A" "A ⊆ G"
    and "card (differenceset A A) ≤ K * real (card A)" "r > 0" "s > 0"
  shows "card (differenceset (sumset_iterated A r) (sumset_iterated A s)) ≤ K^(r+s) * real(card A)"
proof (cases "A = {}")
  case True
  then have "sumset_iterated A r = {}" if "r>0" for r
    using sumset_iterated_empty that by force
  with assms show ?thesis
    by (auto simp: True)
next
  case False
  with assms Pluennecke_Ruzsa_ineq show ?thesis
    by (smt (verit, ccfv_threshold) card_minusset' differenceset_commute finite_minusset 
        minusset_distrib_sum minusset_iterated_minusset minusset_subset_carrier) 
qed

end


subsection ‹Supplementary material on sumsets for sets of integers: basic inequalities›

lemma moninv_int: "monoid.invertible UNIV (+) 0 u" for u::int
  using monoid.invertibleI [where v = "-u"] by (simp add: Group_Theory.monoid_def)

interpretation int: additive_abelian_group UNIV "(+)" "0::int"
  by unfold_locales (use moninv_int in auto)

lemma card_sumset_geq1:
  assumes A: "A ≠ {}" "finite A" and B: "B ≠ {}" "finite B"
  shows "card(int.sumset A B) ≥ (card A) + (card B) - 1"
  using A
proof (induction "card A" arbitrary: A)
  case (Suc n)
  define a where "a = Max A"
  define A' where "A' ≡ A - {a}"
  then obtain a: "a ∈ A" "A' = A - {a}" "finite A'" "a ∉ A'" and A: "A = insert a A'"
    using Max_in Suc a_def by blast
  with Suc have n: "card A' = n"
    by (metis card_Diff_singleton diff_Suc_Suc minus_nat.diff_0 One_nat_def)
  show ?case
  proof (cases "A' = {}")
    case True
    then show ?thesis
      by (simp add: A B(2) int.card_sumset_singleton_eq int.sumset_commute)
  next
    case False
    have "a + Max B ∉ int.sumset A' B"
      using ‹finite A› ‹finite B›
      by (smt (verit, best) DiffE Max_ge a a_def int.sumset.cases singleton_iff)
    then have *: "¬ int.sumset A' B ∪ (+) a ` B ⊆ int.sumset A' B"
      using B Max_in by blast
    have "card A + card B - 1 ≤ Suc (card (int.sumset A' B))"
      using Suc False A a using le_diff_conv by force
    also have "… ≤ card (int.sumset A' B ∪ (+) a ` B)"
      using a B
      by (metis "*" card_seteq finite_Un finite_imageI int.finite_sumset not_less_eq_eq sup_ge1)
    also have "… ≤ card (int.sumset A B)"
    proof (rule card_mono)
      show "finite (int.sumset A B)"
        using B Suc.prems int.finite_sumset by blast
      show "int.sumset A' B ∪ (+) a ` B ⊆ int.sumset A B"
        using A by (force simp: int.sumset)
    qed
    finally show ?thesis .
  qed
qed auto

lemma card_sumset_geq2:
  shows "card(int.sumset A A) ≥ 2 * (card A) - 1"
  using card_sumset_geq1 [of A]
  by (metis mult.commute Nat.add_0_right card_eq_0_iff diff_0_eq_0 le0 mult_2_right)

end