# 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"

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
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"
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 = {𝟬}"

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"
finally show ?thesis .
qed

lemma sumset_iterated_2:
shows "sumset_iterated A 2 = sumset A A"

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"

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)"

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)"

lemma finite_differenceset: "finite A ⟹ finite B ⟹ finite (differenceset A B)"

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
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"
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"
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"
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
```