# Theory Sumset_Triangle_Inequality

```section‹A triangle inequality for sumsets›

(*
Session: Balog_Szemeredi_Gowers
Title:   Sumset_Triangle_Inequality.thy
Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
Affiliation: University of Cambridge
Date: August 2022.
*)

theory Sumset_Triangle_Inequality
imports
Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality
begin

begin

text‹We show a useful triangle inequality for sumsets that does *not* follow from the Ruzsa triangle
inequality. The proof follows the exposition in Zhao's book \cite{Zhaobook}. ›

text‹The following auxiliary lemma corresponds to Lemma 7.3.4 in Zhao's book \cite{Zhaobook}.›

lemma triangle_ineq_sumsets_aux:
fixes X B Y :: "'a set"
assumes hX: "finite X" and hB: "finite B" and hXG: "X ⊆ G" and hBG: "B ⊆ G" and
hXne: "X ≠ {}" and hYX: "⋀ Y. Y ⊆ X ⟹ Y ≠ {} ⟹ card (sumset Y B) / card Y ≥
card (sumset X B) / card X" and hC: "finite C" and hCne: "C ≠ {}" and hCG: "C ⊆ G"
shows "card (sumset X (sumset C B)) / card (sumset X C) ≤ card (sumset X B) / card X"
using hC hCne hCG proof (induct)
case empty
then show ?case by blast
next
case hcase: (insert c C)
have hc : "c ∈ G" using hcase by auto
show "card (sumset X B) / card X ≥
card (sumset X (sumset (insert c C) B)) / card (sumset X (insert c C))"
proof(cases "C = {}")
case True
then have "card (sumset X (insert c C)) = card X" using hc hXG hX
by (simp add: card_sumset_singleton_eq le_iff_inf)
moreover have "card (sumset X (sumset (insert c C) B)) ≤ card (sumset X B)" using hX hB hBG hXG
hc by (metis True card_sumset_le finite_sumset sumset_assoc sumset_commute)
ultimately show ?thesis by (simp add: divide_right_mono)
next
case hCne: False
have hCG : "C ⊆ G" using hcase by auto
have hstep: "card (sumset X (sumset {c} B) - sumset X (sumset C B)) ≤
card (sumset X B) * card (sumset X {c} - sumset X C) / card X"
proof-
let ?Y = "{x ∈ X. sumset {x} (sumset {c} B) ⊆ sumset X (sumset C B)}"
have hYX : "?Y ⊆ X" and hY: "finite ?Y" using finite_subset hX by auto
have hsub1: "sumset X (sumset {c} B) - sumset X (sumset C B) ⊆
sumset (sumset X {c} - sumset X C) B"
by (metis Diff_subset_conv Un_Diff_cancel sumset_assoc sumset_subset_Un1 sup.cobounded2)
have hcard1 : "card (sumset X B) = card (sumset X (sumset {c} B))"
by (metis card_sumset_singleton_eq finite_sumset hB hX hc sumset_Int_carrier sumset_assoc
sumset_commute)
have hcard2 : "card (sumset ?Y B) = card (sumset (sumset ?Y {c}) B)"
using card_sumset_singleton_eq finite_sumset hB hY hc sumset_Int_carrier sumset_assoc
sumset_commute by (smt (verit, ccfv_threshold))
have "sumset (sumset ?Y {c}) B ⊆ sumset X (sumset C B)"
proof
fix d assume "d ∈ sumset (sumset ?Y {c}) B"
then obtain a b where ha: "a ∈ ?Y" and "b ∈ B" and hd: "d = a ⊕ c ⊕ b"
by (smt (verit) empty_iff insert_iff sumset.cases)
then have "a ⊕ c ⊕ b ∈ sumset {a} (sumset {c} B)"
by (smt (verit) associative composition_closed hBG hXG hc insertCI mem_Collect_eq subsetD
sumset.sumsetI)
then show "d ∈ sumset X (sumset C B)" using ha hd by blast
qed
then have hdisj : "disjnt ((sumset X (sumset {c} B)) - (sumset X (sumset C B)))
(sumset (sumset ?Y {c}) B)"
by (auto simp add : disjnt_iff)
have hsub2 : "sumset (sumset X {c} - sumset X C) B ∪ sumset (sumset ?Y {c}) B ⊆
sumset (sumset X {c}) B" by (simp add: sumset_mono)
then have ineq1: "card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset ?Y B) ≤
card (sumset X B)"
proof-
have "card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset ?Y B) =
card ((sumset X (sumset {c} B) - sumset X (sumset C B)) ∪ sumset (sumset ?Y {c}) B)"
using hdisj hcard2 card_Un_disjnt finite_sumset hX hYX finite_subset hB
by (metis (no_types, lifting) finite.emptyI finite.insertI finite_Diff)
also have "... ≤ card (sumset X (sumset {c} B))" using card_mono finite_sumset hX hB
by (metis (no_types, lifting) Diff_subset Un_subset_iff finite.emptyI finite.insertI
hsub2 sumset_assoc)
finally show "card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset ?Y B) ≤
card (sumset X B)" using hcard1 by auto
qed
have ineq2: "card (sumset X {c} - sumset X C)  ≥ card X - card ?Y"
proof-
let ?Z = "{x ∈ X. sumset {x} {c} ⊆ sumset X C}"
have hZY: "?Z ⊆ ?Y"
by (smt (verit, del_insts) Collect_mono_iff subset_refl sumset_assoc sumset_mono)
have hinj: "inj_on (λ x. x ⊕ c) (X - ?Z)"
proof (intro inj_onI)
fix x y assume "x ∈ X - ?Z" and "y ∈ X - ?Z" and h: "x ⊕ c = y ⊕ c"
then have "x ∈ G" and "y ∈ G" using hXG by auto
then show "x = y" using h hc by simp
qed
have himage: "(λ x. x ⊕ c) ` (X - ?Z) = sumset X {c} - sumset X C"
proof
show "(λx. x ⊕ c) ` (X - ?Z) ⊆ sumset X {c} - sumset X C"
proof(intro image_subsetI)
fix x assume hx: "x ∈ X - ?Z"
then have hxG : "x ∈ G" using hXG by auto
then have hxc1: "x ⊕ c ∈ sumset X {c}" using hXG hc hx by auto
have "x ⊕ c ∈ sumset {x} {c}" using hxG hc by auto
then have hxc2: "x ⊕ c ∉ sumset X C" using hx hXG hc hCG
using DiffD2 sumset.simps sumset.sumsetI by auto
then show "x ⊕ c ∈ sumset X {c} - sumset X C" using hxc1 hxc2 by simp
qed
show "sumset X {c} - sumset X C ⊆ (λx. x ⊕ c) ` (X - ?Z)"
proof
fix d assume "d ∈ sumset X {c} - sumset X C"
then obtain x where hd: "d = x ⊕ c" and hxc: "x ⊕ c ∉ sumset X C" and hx: "x ∈ X"
using sumset.cases by force
then show "d ∈ (λx. x ⊕ c) ` (X - ?Z)" using hd hxc hx hXG hc by auto
qed
qed
have hcard3: "card (X - ?Z) = card (sumset X {c} - sumset X C)"
using card_image hinj himage by fastforce
have "card X = card ?Z + card (X - ?Z)"
by (simp add: card_Diff_subset card_mono hX)
also have "... ≤ card ?Y + card (sumset X {c} - sumset X C)"
using hcard3 card_mono hZY hY by auto
finally show ?thesis by simp
qed
have ineq3: "card (sumset X B) - card (sumset ?Y B) ≤
card (sumset X B) * (card X - card ?Y) / card X"
proof(cases "?Y = {}")
case True
then show ?thesis using card_eq_0_iff
by (smt (verit) hX hXne minus_nat.diff_0 nonzero_mult_div_cancel_right of_nat_eq_0_iff
of_nat_mult sumset_empty(2))
next
case hYne: False
have "card (sumset ?Y B) ≥ card (sumset X B) / card X * card ?Y" using assms(6)[OF hYX hYne]
hX hYne hX hYX finite_subset divide_le_eq
by (smt (z3) card_gt_0_iff hY mult_imp_div_pos_less of_nat_0_less_iff)
moreover have "card (sumset X B) / card X * card ?Y = (card (sumset X B) * card ?Y) / card X"
by auto
moreover have "card (sumset X B) * card ?Y / card X  * card X = card (sumset X B) * card ?Y"
using hX by (simp add: field_simps)
ultimately have "card (sumset ?Y B) * card X ≥ card (sumset X B) * card ?Y"
using hX hXne of_nat_0_less_iff le_divide_eq
by (smt (z3) card_sumset_0_iff hBG hXG mult_cancel1 mult_cancel2 of_nat_le_0_iff
of_nat_le_iff of_nat_mult)
then have "real ((card (sumset X B) - card (sumset ?Y B)) * card X) ≤
card (sumset X B) * (card X - card ?Y)"
by (simp add: diff_mult_distrib diff_mult_distrib2)
thus ?thesis using le_divide_eq card_eq_0_iff hX hXne
by (smt (z3) of_nat_le_0_iff of_nat_mult)
qed
show ?thesis
proof-
have "real (card ((sumset X (sumset {c} B)) - (sumset X (sumset C B)))) ≤
card (sumset X B) - card (sumset ?Y B)" using ineq1 by auto
also have "... ≤ card (sumset X B) * (card X - card ?Y) / card X" using ineq3 by auto
also have "... ≤ card (sumset X B) * card (sumset X {c} - sumset X C) / card X" using ineq2
divide_le_cancel of_nat_less_0_iff of_nat_mono by (smt (verit, del_insts) mult_le_mono2)
finally show ?thesis by simp
qed
qed
have hinsert: "real (card (sumset X (sumset (insert c C) B))) / real (card (sumset X (insert c C))) =
(card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset X (sumset C B))) /
(card (sumset X {c} - sumset X C) + card (sumset X C))"
using sumset_insert2 card_Un_disjoint finite_sumset hX hB hC Diff_disjoint Int_commute
Un_commute finite.emptyI finite.insertI finite_Diff hcase.hyps(1)
by (smt (verit) Un_Diff_cancel2 insert_is_Un sumset_commute sumset_subset_Un2)
have hsplit: "real (card (sumset X B)) * (card (sumset X {c} - sumset X C) + card (sumset X C)) / card X =
real (card (sumset X B)) * card (sumset X {c} - sumset X C) / card X +
card (sumset X B) * card (sumset X C) / card X"
have hind: "card (sumset X B) * card (sumset X C) / card X ≥ card (sumset X (sumset C B))"
using hcase(3)[OF hCne hCG] hXne hCne hcase(1) hX finite_sumset card_gt_0_iff
add_mult_distrib2 of_nat_mult card_eq_0_iff card_sumset_0_iff hCG
hXG of_nat_0_less_iff by (metis (no_types, opaque_lifting) divide_le_eq times_divide_eq_left)
have "real (card (sumset X B)) * (card (sumset X {c} - sumset X C) + card (sumset X C)) / card X ≥
(card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset X (sumset C B)))"
using hsplit hind hstep by simp
then have "card (sumset X B) / card X ≥
(card (sumset X (sumset {c} B) - sumset X (sumset C B)) + card (sumset X (sumset C B))) /
(card (sumset X {c} - sumset X C) + card (sumset X C))" using card_sumset_0_iff hCG hXG
card_eq_0_iff hC hX hXne hCne divide_self le_divide_eq
by (smt (z3) add_is_0 hcase.hyps(1) of_nat_le_0_iff times_divide_eq_left)
thus "real (card (sumset X (sumset (insert c C) B))) / real (card (sumset X (insert c C))) ≤
real (card (sumset X B)) / real (card X)" using hinsert by auto
qed
qed

text‹The following inequality is the result corresponding to Corollary 7.3.6 in Zhao's book \cite{Zhaobook}.›

lemma triangle_ineq_sumsets:
assumes hA: "finite A" and hB: "finite B" and hC: "finite C" and
hAG : "A ⊆ G" and hBG: "B ⊆ G" and hCG: "C ⊆ G"
shows "card A * card (sumset B C) ≤ card (sumset A B) * card (sumset A C)"

proof(cases "A = {}")
case True
then show ?thesis by simp
next
case hAne: False
show "card A * card (sumset B C) ≤ card (sumset A B) * card (sumset A C)"
proof(cases "B = {}")
case True
then show ?thesis by simp
next
case hBne: False
define KS where "KS ≡ (λX. card (sumset X C) / real (card X)) ` (Pow A - {{}})"
define K where "K ≡ Min KS"
define X where "X ≡ @X. X ∈ Pow A - {{}} ∧ K = card (sumset X C) / real (card X)"
obtain KS: "finite KS" "KS ≠ {}"
using KS_def hA hAne by blast
then have "K ∈ KS"
using K_def Min_in by blast
then have "∃X. X ∈ Pow A - {{}} ∧ K = card (sumset X C) / real (card X)"
using KS_def by blast
then obtain "X ∈ Pow A - {{}}" and Keq: "K = card (sumset X C) / real (card X)"
by (metis (mono_tags, lifting) X_def someI_ex)
then have hX: "X ⊆ A" "X ≠ {}"
by auto
have hXmin : "⋀ Y. Y ⊆ A ⟹ Y ≠ {} ⟹
card (sumset X C) / card X ≤ card (sumset Y C) / card Y"
using K_def KS_def Keq Min_le KS(1) by auto
then have hXAineq: "card (sumset X C) / card X ≤ card (sumset A C) / card A"
by (metis hAne subset_refl)
have haux: "real (card (sumset X (sumset B C))) / real (card (sumset X B))
≤ real (card (sumset X C)) / real (card X)" using triangle_ineq_sumsets_aux[of "X" "C" "B"]
hXmin hX hA hAG finite_subset hB hC hBne hBG hC hCG subset_trans by metis
have hXAsumset : "real (card (sumset X B)) ≤ card (sumset A B)"
using hX(1) card_mono hA finite_sumset hB order_refl sumset_mono
by (metis of_nat_le_iff)
have "card (sumset B C) ≤ card (sumset X (sumset B C))" using assms hX
finite_sumset hAG card_le_sumset
by (metis bot.extremum_uniqueI dual_order.trans infinite_super subsetD subsetI
sumset_subset_carrier)
also have "... ≤ (card (sumset X C) / card X) * card (sumset X B)" using haux divide_le_eq
card_sumset_0_iff hBne hX hB hA finite_subset card_0_eq by (smt (verit) hCG mult_eq_0_iff
of_nat_0_eq_iff of_nat_0_le_iff sumset_assoc sumset_subset_carrier)
also have "... ≤ (card (sumset A C) / card A) * card (sumset A B)"
using hXAineq hXAsumset by (meson divide_nonneg_nonneg mult_mono' of_nat_0_le_iff)
finally have "card (sumset B C) ≤ (card (sumset A C) * card (sumset A B)) / card A" by simp
then have "card (sumset B C) * card A ≤ card (sumset A C) * card (sumset A B)"
using le_divide_eq hAne hA card_gt_0_iff by (smt (verit, ccfv_threshold)
card_0_eq of_nat_le_0_iff of_nat_le_iff of_nat_mult)
thus "card A * card (sumset B C) ≤ card (sumset A B) * card (sumset A C)"
by (simp add: mult.commute)
qed
qed

end
end```