diff --git a/thys/Balog_Szemeredi_Gowers/Additive_Combinatorics_Preliminaries.thy b/thys/Balog_Szemeredi_Gowers/Additive_Combinatorics_Preliminaries.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Additive_Combinatorics_Preliminaries.thy @@ -0,0 +1,452 @@ +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)\<^sup>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)\<^sup>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)\<^sup>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 \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Additive_Energy_Lower_Bounds.thy b/thys/Balog_Szemeredi_Gowers/Additive_Energy_Lower_Bounds.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Additive_Energy_Lower_Bounds.thy @@ -0,0 +1,99 @@ +section\Results on lower bounds on additive energy\ + +(* + Session: Balog_Szemeredi_Gowers + Title: Additive_Energy_Lower_Bounds.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Additive_Energy_Lower_Bounds + imports + Additive_Combinatorics_Preliminaries + Miscellaneous_Lemmas +begin + +context additive_abelian_group + +begin + +text\The following corresponds to Proposition 2.11 in Gowers's notes \cite{Gowersnotes}.\ + +proposition additive_energy_lower_bound_sumset: fixes C::real + assumes "finite A" and "A \ G" and "(card (sumset A A)) \ C * card A" and "card A \ 0" + shows "additive_energy A \ 1/C" + +proof- + have "(card A)^2 = (\ x \ sumset A A. real (f_sum x A))" + using assms f_sum_card by (metis of_nat_sum) + also have "... \ (card((sumset A A)) powr(1/2)) * (\ x \ sumset A A . (f_sum x A)^2) powr(1/2)" + using Cauchy_Schwarz_ineq_sum2[of "\ d. 1" "\ d. f_sum d A"] by auto + also have "...\ ((C * (card A)) powr(1/2)) * ((\ x \ sumset A A . (f_sum x A)^2)) powr(1/2) " + by (metis mult.commute mult_left_mono assms(3) of_nat_0_le_iff powr_ge_pzero powr_mono2 + zero_le_divide_1_iff zero_le_numeral) + finally have "((card A)^2)^2 \ (((C * (card A)) powr(1/2)) * ((\ x \ sumset A A . (f_sum x A)^2)) powr(1/2))^2" + by (metis of_nat_0_le_iff of_nat_power_eq_of_nat_cancel_iff power_mono) + then have "(card A)^4 \ (((C * (card A)) * ((\ x \ sumset A A. (f_sum x A)^2))) powr (1/2))^2" + by (smt (verit) assms of_nat_0_le_iff powr_mult + mult.left_commute power2_eq_square power3_eq_cube power4_eq_xxxx power_commutes) + then have "(card A)^4 \ (( C * (card A)) * ((\ x \ sumset A A. (f_sum x A)^2)))" + using assms powr_half_sqrt of_nat_0 of_nat_le_0_iff power_mult_distrib + real_sqrt_pow2 by (smt (verit, best) powr_mult) + moreover have "additive_energy A = (\ x \ sumset A A. (f_sum x A)^2)/ (card A)^3" + using additive_energy_def f_sum_card_quadruple_set assms by simp + moreover then have "additive_energy A * (card A)^3 = (\ x \ sumset A A. (f_sum x A)^2)" + using assms by simp + ultimately have "(additive_energy A) \ ((card A)^4)/ ( C * (card A)^4 )" + using additive_energy_upper_bound + additive_abelian_group_axioms assms divide_le_eq divide_le_eq_1_pos mult.left_commute + mult_left_mono of_nat_0_eq_iff of_nat_0_le_iff power_eq_0_iff power3_eq_cube power4_eq_xxxx + linorder_not_less mult.assoc mult_zero_left of_nat_0_less_iff of_nat_mult + order_trans_rules(23) times_divide_eq_right by (smt (verit) card_sumset_0_iff + div_by_1 mult_cancel_left1 nonzero_mult_div_cancel_left nonzero_mult_divide_mult_cancel_right + nonzero_mult_divide_mult_cancel_right2 of_nat_1 of_nat_le_0_iff times_divide_eq_left) + then show ?thesis by (simp add: assms) +qed + + +text\An analogous version of Proposition 2.11 where the assumption is on a difference set is given +below. The proof is identical to the proof of @{term additive_energy_lower_bound_sumset} +above (with the obvious modifications). \ + +proposition additive_energy_lower_bound_differenceset: fixes C::real + assumes "finite A" and "A \ G" and "(card (differenceset A A)) \ C * card A" and "card A \ 0" + shows "additive_energy A \ 1/C" + +proof- + have "(card A)^2 = (\ x \ differenceset A A. real (f_diff x A))" + using assms f_diff_card by (metis of_nat_sum) + also have "... \ (card((differenceset A A)) powr (1/2)) * (\ x \ differenceset A A . (f_diff x A)^2) powr(1/2)" + using Cauchy_Schwarz_ineq_sum2[of "\ d. 1" "\ d. f_diff d A"] by auto + also have "...\ ((C * (card A))powr (1/2)) * ((\ x \ differenceset A A . (f_diff x A)^2)) powr(1/2)" + by (metis mult.commute mult_left_mono assms(3) of_nat_0_le_iff powr_ge_pzero powr_mono2 + zero_le_divide_1_iff zero_le_numeral) + finally have "((card A)^2)^2 \ (((C * (card A))powr (1/2)) * ((\ x \ differenceset A A . (f_diff x A)^2)) powr(1/2))^2" + by (metis of_nat_0_le_iff of_nat_power_eq_of_nat_cancel_iff power_mono) + then have "(card A)^4 \ (((C * (card A)) * ((\ x \ differenceset A A. (f_diff x A)^2))) powr (1/2))^2" + by (smt (verit) assms of_nat_0_le_iff powr_mult + mult.left_commute power2_eq_square power3_eq_cube power4_eq_xxxx power_commutes) + then have "(card A)^4 \ ((C * (card A)) * ((\ x \ differenceset A A . (f_diff x A)^2)))" + using assms powr_half_sqrt of_nat_0 of_nat_le_0_iff power_mult_distrib + real_sqrt_pow2 by (smt (verit, best) powr_mult) + moreover have "additive_energy A = (\ x \ differenceset A A. (f_diff x A)^2)/ (card A)^3" + using additive_energy_def f_diff_card_quadruple_set assms by simp + moreover then have "additive_energy A * (card A)^3 = (\ x \ differenceset A A. (f_diff x A)^2)" + using assms by simp + ultimately have "(additive_energy A) \ ((card A)^4)/ (C * (card A)^4 )" + using additive_energy_upper_bound + additive_abelian_group_axioms assms divide_le_eq divide_le_eq_1_pos mult.left_commute + mult_left_mono of_nat_0_eq_iff of_nat_0_le_iff power_eq_0_iff power3_eq_cube power4_eq_xxxx + linorder_not_less mult.assoc mult_zero_left of_nat_0_less_iff of_nat_mult + order_trans_rules(23) times_divide_eq_right by (smt (verit) card_sumset_0_iff + div_by_1 mult_cancel_left1 nonzero_mult_div_cancel_left nonzero_mult_divide_mult_cancel_right + nonzero_mult_divide_mult_cancel_right2 of_nat_1 of_nat_le_0_iff times_divide_eq_left) + then show ?thesis by (simp add: assms) +qed + +end +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy b/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy @@ -0,0 +1,1268 @@ +section\Towards the proof of the Balog--Szemer\'{e}di--Gowers Theorem\ + +(* + Session: Balog_Szemeredi_Gowers + Title: Balog_Szemeredi_Gowers_Main_Proof.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Balog_Szemeredi_Gowers_Main_Proof + imports + Prob_Space_Lemmas + Graph_Theory_Preliminaries + Sumset_Triangle_Inequality + Additive_Combinatorics_Preliminaries +begin + +context additive_abelian_group + +begin + +text\After having introduced all the necessary preliminaries in the imported files, we are now + ready to follow the chain of the arguments for the main proof as in Gowers's notes \cite{Gowersnotes}.\ + +text\The following lemma corresponds to Lemma 2.13 in Gowers's notes \cite{Gowersnotes}.\ + +lemma (in fin_bipartite_graph) proportion_bad_pairs_subset_bipartite: + fixes c::real + assumes "c > 0" + obtains X' where "X' \ X" and "card X' \ density * card X / sqrt 2" and + "card (bad_pair_set X' Y c) / (card X')^2 \ 2 * c / density^2" +proof (cases "density = 0") (* Edge case *) + case True + then show ?thesis using that[of "{}"] bad_pair_set_def by auto +next + case False + then have dgt0: "density > 0" using density_simp by auto + let ?M = "uniform_count_measure Y" + interpret P: prob_space ?M + by (simp add: Y_not_empty partitions_finite prob_space_uniform_count_measure) + have sp: "space ?M = Y" + by (simp add: space_uniform_count_measure) + (* First show that the expectation of the size of X' is the average degree of a vertex *) + have avg_degree: "P.expectation (\ y . card (neighborhood y)) = density * (card X)" + proof - + have "density = (\y \ Y . degree y)/(card X * card Y)" + using edge_size_degree_sumY density_simp by simp + then have d: "density * (card X) = (\y \ Y . degree y)/(card Y)" + using card_edges_between_set edge_size_degree_sumY partitions_finite(1) partitions_finite(2) by auto + have "P.expectation (\ y . card (neighborhood y)) = P.expectation (\ y . degree y)" + using alt_deg_neighborhood by simp + also have "... =(\ y \ Y. degree y)/(card Y)" using P.expectation_uniform_count + by (simp add: partitions_finite(2)) + finally show ?thesis using d by simp + qed +(* Conclude an inequality by Cauchy-Schwarz variation *) + then have card_exp_gt: "P.expectation (\ y. (card (neighborhood y))^2) \ density^2 * (card X)^2" + proof - + have "P.expectation (\ y. (card (neighborhood y))^2) \ (P.expectation (\ y . card (neighborhood y)))^2" + using P.cauchy_schwarz_ineq_var_uniform partitions_finite(2) by auto + thus ?thesis using avg_degree + by (metis of_nat_power power_mult_distrib) + qed +(* Define our bad pair sets in this context *) + define B where "B \ bad_pair_set X Y c" + define B' where "B' \ \ y. bad_pair_set (neighborhood y) Y c" + have finB: "finite B" using bad_pair_set_finite partitions_finite B_def by auto + have "\ x. x \ X \ x \ V" using partitions_ss(1) by auto + have "card B \ (card (X \ X))" using B_def bad_pair_set_ss partitions_finite + card_mono finite_cartesian_product_iff by metis + then have card_B: "card B \ (card X)^2" + by (metis card_cartesian_prod_square partitions_finite(1)) + (* Find a bound on the probability of both x and x' belonging to X' *) + have "\ x x' . (x, x') \ B \ P.prob {y \ Y . {x, x'} \ neighborhood y} < c" + proof - + fix x x' assume assm: "(x, x') \ B" + then have "x \ X" "x' \ X" unfolding B_def bad_pair_set_def bad_pair_def by auto + then have card_eq: "card {v \ V . vert_adj v x \ vert_adj v x'} = card {y \ Y. vert_adj y x \ vert_adj y x'}" + by (metis (no_types, lifting) X_vert_adj_Y vert_adj_edge_iff2 vert_adj_imp_inV) + have ltc: "card {v \ V . vert_adj v x \ vert_adj v x'}/(card Y) < c" + using assm by (auto simp add: B_def bad_pair_set_def bad_pair_def codegree_normalized_def codegree_def vert_adj_sym) + have "{y \ Y . {x, x'} \ neighborhood y} = {y \ Y . vert_adj y x \ vert_adj y x'}" + using bad_pair_set_def bad_pair_def neighborhood_def vert_adj_imp_inV vert_adj_imp_inV by auto + then have "P.prob {y \ Y . {x, x'} \ neighborhood y} = card {y \ Y. vert_adj y x \ vert_adj y x'}/ card Y" + using measure_uniform_count_measure partitions_finite(2) by fastforce + thus "P.prob {y \ Y . {x, x'} \ neighborhood y} < c" using card_eq ltc by simp + qed + then have "\ x x' . (x, x') \ B \ P.prob {y \ Y . (x, x') \ B' y} < c" + by (simp add: B_def B'_def bad_pair_set_def) + then have prob: "\ p .p \ B \ P.prob {y \ Y . indicator (B' y) p = 1} \ c" + unfolding indicator_def by fastforce +(* Conclude a bound on the expected number of bad pairs in X' *) + have dsimp: "(density^2 - (density^2/(2 * c)) * c) * (card X)^2 =(density^2/2) * (card X)^2" + using assms by (simp add: algebra_simps) + then have gt0: "(density^2/2) * (card X)^2 > 0" + using dgt0 by (metis density_simp division_ring_divide_zero half_gt_zero linorder_neqE_linordered_idom + of_nat_less_0_iff of_nat_mult power2_eq_square zero_less_mult_iff) + have Cgt0: "(density^2/(2 * c)) > 0" using dgt0 assms by auto + have "\ y . y \ Y \ card (B' y) = (\ p \ B. indicator (B' y) p)" + proof - + fix y assume "y \ Y" + then have "neighborhood y \ X" by (simp add: neighborhood_subset_oppY) + then have ss: "B' y \ B" unfolding B_def B'_def bad_pair_set_def + using set_pairs_filter_subset by blast + then show "card (B' y) = (\ p \ B. indicator (B' y) p)" + using card_set_ss_indicator[of "B' y" "B"] finB by auto + qed + then have "P.expectation (\ y. card (B' y)) = P.expectation (\ y. (\ p \ B. indicator (B' y) p))" + by (metis (mono_tags, lifting) P.prob_space_axioms of_nat_sum partitions_finite(2) + prob_space.expectation_uniform_count real_of_nat_indicator sum.cong) + also have "... = (\ p \ B . P.expectation (\ y. indicator (B' y) p))" + by (rule Bochner_Integration.integral_sum[of "B" ?M "\ p y . indicator (B' y) p"]) + (auto simp add: P.integrable_uniform_count_measure_finite partitions_finite(2)) + finally have "P.expectation (\ y. card (B' y)) = (\ p \ B . P.prob {y \ Y. indicator (B' y) p = 1})" + using P.expectation_finite_uniform_indicator[of "Y" "B'"] using partitions_finite(2) + by (smt (verit, best) sum.cong) + then have "P.expectation (\ y. card (B' y)) \ (\ p \ B . c)" + using prob sum_mono[of B "\ p. P.prob {y \ Y. indicator (B' y) p = 1}" "\ p. c"] + by (simp add: indicator_eq_1_iff) + then have lt1: "P.expectation (\ y. card (B' y)) \ c * (card B)" using finB + by (simp add: mult_of_nat_commute) +(* State the inequality for any positive constant C *) + have "c * (card B) \ c * (card X)^2" using assms card_B by auto + then have "P.expectation (\ y. card (B' y)) \ c * (card X)^2" + using lt1 by linarith + then have "\ C. C> 0 \ C * P.expectation (\ y. card (B' y)) \ C * c * (card X)^2" + by auto + then have "\ C . C> 0 \(P.expectation (\ y. (card (neighborhood y))^2) - C * (P.expectation (\ y. card (B' y))) + \ (density^2 *(card X)^2) - (C*c*(card X)^2))" + using card_exp_gt diff_strict1_mono by (smt (verit)) + then have "\ C .C> 0 \ (P.expectation (\ y. (card (neighborhood y))^2) - C * (P.expectation (\ y. card (B' y))) + \ (density^2 - C * c) * (card X)^2)" + by (simp add: field_simps) +(* Choose a value for C *) + then have "(P.expectation (\ y. (card (neighborhood y))^2) - (density^2/(2 * c)) * (P.expectation (\ y. card (B' y))) + \ (density^2 - (density^2/(2 * c)) * c) * (card X)^2)" + using Cgt0 assms by blast + then have "P.expectation (\ y. (card (neighborhood y))^2) - (density^2/(2 * c)) * (P.expectation (\ y. card (B' y))) + \ (density^2/2) * (card X)^2" using dsimp by linarith + then have "P.expectation (\ y. (card (neighborhood y))^2) - (P.expectation (\ y. (density^2/(2 * c)) * card (B' y))) + \ (density^2/2) * (card X)^2" by auto + then have "P.expectation (\ y. (card (neighborhood y))^2 - ((density^2/(2*c)) * card (B' y))) + \ (density^2/2) * (card X)^2" + using Bochner_Integration.integral_diff[of ?M "(\ y. (card (neighborhood y))^2)" "(\ y. (density^2/(2 * c)) * card (B' y))"] + P.integrable_uniform_count_measure_finite partitions_finite(2) by fastforce + (* Obtain an X' with the required inequalities *) + then obtain y where yin: "y \ Y" and ineq: "(card (neighborhood y))^2 - ((density^2/(2 * c)) * card (B' y)) \ (density^2/2) * (card X)^2" + using P.expectation_obtains_ge partitions_finite(2) by blast +(* Show the result follows *) + let ?X' = "neighborhood y" + have ss: "?X' \ X" + using yin by (simp add: neighborhood_subset_oppY) + have "local.density\<^sup>2 / (2 * c) * real (card (B' y)) \ 0" + using assms density_simp by simp + then have d1: "(card ?X')^2 \ (density^2/2) * (card X)^2" + using ineq by linarith + then have "(card ?X') \ sqrt(((density) * (card X))^2/2)" + by (simp add: field_simps real_le_lsqrt) + then have den: "((card ?X') \ (density * (card X)/(sqrt 2)))" + by (smt (verit, del_insts) divide_nonneg_nonneg divide_nonpos_nonneg real_sqrt_divide + real_sqrt_ge_0_iff real_sqrt_unique zero_le_power2) + have xgt0: "(card ?X') > 0" using dgt0 gt0 + using d1 gr0I by force (* long *) + then have "(card ?X')^2 \ (density^2/(2 * c)) * card (B' y)" + using gt0 ineq by simp + then have "(card ?X')^2/(density^2/(2 * c)) \ card (B' y)" + using Cgt0 by (metis mult.commute pos_le_divide_eq) + then have "((2 * c)/(density^2)) \ card (B' y)/(card ?X')^2" + using pos_le_divide_eq xgt0 by (simp add: field_simps) + thus ?thesis using that[of "?X'"] den ss B'_def by auto +qed + +text\The following technical probability lemma corresponds to Lemma 2.14 in Gowers's notes \cite{Gowersnotes}. \ + +lemma (in prob_space) expectation_condition_card_1: + fixes X::"'a set" and f::"'a \ real" and \::real + assumes "finite X" and "\ x \ X. f x \ 1" and "M = uniform_count_measure X" and "expectation f \ \" + shows "card {x \ X. (f x \ \ / 2)} \ \ * card X / 2" +proof (cases "\ \ 0") + assume h\: "\ \ 0" + have ineq1: "real (card (X - {x \ X. \ \ f x * 2})) * \ \ real (card X) * \" + using card_mono assms Diff_subset h\ mult_le_cancel_right nat_le_linear of_nat_le_iff + by (smt (verit, best)) + have ineq2: "\ x \ X - {x. x \ X \ (f x \ \/2)}. f x \ \ / 2" by auto + have "expectation f * card X = (\x \ X. f x)" + using assms(1) expectation_uniform_count assms(3) by force + also have "... = (\ x \{x. x \ X \ (f x \ \/2)}. f x) + +(\ x \ X - {x. x \ X \ (f x \ \/2)}. f x)" + using assms + by (metis (no_types, lifting) add.commute mem_Collect_eq subsetI sum.subset_diff) + also have "... \ (\ x \ {x. x \ X \ (f x \ \/2)}. 1) + + (\ x \ X - {x. x \ X \ (f x \ \/2)} . \ / 2)" + using assms sum_mono ineq2 by (smt (verit, ccfv_SIG) mem_Collect_eq) + also have "... \ card ({x. x \ X \ (f x \ \/2)}) + (card X) * \ / 2 " + using ineq1 by auto + finally have "\ * card X \ card {x. x \ X \ (f x \ \/2)}+ (\/2)*(card X)" + using ineq1 mult_of_nat_commute assms(4) mult_right_mono le_trans + by (smt (verit, del_insts) of_nat_0_le_iff times_divide_eq_left) + then show ?thesis by auto +next + assume "\ \ \ 0" + thus ?thesis by (smt (verit, del_insts) divide_nonpos_nonneg mult_nonpos_nonneg of_nat_0_le_iff) +qed + +text\The following technical probability lemma corresponds to Lemma 2.15 in Gowers's notes. \ + +lemma (in prob_space) expectation_condition_card_2: + fixes X::"'a set" and \::real and \::real and f:: "'a \ real" + assumes "finite X" and "\ x. x \ X \ f x \ 1" and "\ > 0" and "\ > 0" + and "expectation f \ 1 - \" and "M = uniform_count_measure X" + shows "card {x \ X. f x \ 1 - \} \ (1- \ / \) * card X" + +proof- + have hcard: "card {x \ X. 1 - \ \ f x} \ card X" using card_mono assms(1) by fastforce + have h\: "\ x \ X- {x. x \ X \ (f x \ 1 - \)}. f x \ 1 - \" by auto + have "expectation f * card X = (\ x \ X. f x)" + using assms(1) expectation_uniform_count assms(6) by force + then have "(1 - \) * card X \ (\ x \ X. f x)" using assms + by (metis mult.commute sum_bounded_below sum_constant) + also have "... = (\ x \ {x. x \ X \ (f x \ 1 - \)}. f x) + + (\ x \ X - {x. x \ X \ (f x \ 1 - \)}. f x)" using assms + by (metis (no_types, lifting) add.commute mem_Collect_eq subsetI sum.subset_diff) + also have "... \ (\ x \ {x. x \ X \ (f x \ 1 - \)}. 1) + + (\ x \ X - {x. x \ X \ (f x \ 1 - \)}. (1 - \))" + using assms h\ sum_mono by (smt (verit, ccfv_SIG) mem_Collect_eq) + also have "... = card {x. x \ X \ (f x \ 1 - \)} + (1-\) * card ( X- {x. x \ X \ (f x \ 1 - \)})" + by auto + also have "... = (card {x. x \ X \ (f x \ 1 - \)} + + card (X- {x. x \ X \ (f x \ 1 - \)})) - \ * card (X -{x. x \ X \ (f x \ 1 - \)})" + using left_diff_distrib + by (smt (verit, ccfv_threshold) mult.commute mult.right_neutral of_nat_1 of_nat_add of_nat_mult) + also have heq: "... = card X - \ * card (X -{x. x \ X \ (f x \ 1 - \)})" + using assms(1) card_Diff_subset[of "{x. x \ X \ (f x \ 1 - \)}" "X"] hcard by auto + finally have "(1- \) * card X \ card X - \ * card ( X -{x. x \ X \ (f x \ 1 - \)})" by blast + then have "- (1- \) * card X + card X \ \ * card ( X -{x. x \ X \ (f x \ 1 - \)})" by linarith + then have "- card X + \ * card X + card X \ \ * card(X - {x. x \ X \ (f x \ 1 - \)})" + using add.assoc add.commute + add.right_neutral add_0 add_diff_cancel_right' add_diff_eq add_uminus_conv_diff diff_add_cancel + distrib_right minus_diff_eq mult.commute mult_1 of_int_minus of_int_of_nat_eq uminus_add_conv_diff + cancel_comm_monoid_add_class.diff_cancel by (smt (verit, del_insts) mult_cancel_right2) + then have "\ * card X \ \ * card(X - {x. x \ X \ (f x \ 1 - \)})" by auto + then have "\ * card X / \ \ card(X - {x. x \ X \ (f x \ 1 - \)})" using assms + by (smt (verit, ccfv_SIG) mult.commute pos_divide_less_eq) + then show ?thesis by (smt (verit) heq combine_common_factor left_diff_distrib' mult_of_nat_commute + nat_mult_1_right of_nat_1 of_nat_add of_nat_mult times_divide_eq_left scale_minus_left) +qed + +text\The following lemma corresponds to Lemma 2.16 in Gowers's notes \cite{Gowersnotes}. For the proof, we will apply +Lemma 2.13 (@{term proportion_bad_pairs_subset_bipartite}, the technical probability Lemmas 2.14 +(@{term expectation_condition_card_1}) and 2.15 (@{term expectation_condition_card_2}) as well +as background material on graphs with loops and bipartite graphs that was previously presented. \ + +lemma (in fin_bipartite_graph) walks_of_length_3_subsets_bipartite: + obtains X' and Y' where "X' \ X" and "Y' \ Y" and + "card X' \ (edge_density X Y)^2 * card X / 16" and + "card Y' \ edge_density X Y * card Y / 4" and + "\ x \ X'. \ y \ Y'. card {p. connecting_walk x y p \ walk_length p = 3} \ + (edge_density X Y)^6 * card X * card Y / 2^13" + +proof (cases "edge_density X Y > 0") + let ?\ = "edge_density X Y" + assume h\: "?\ > 0" + interpret P1: prob_space "uniform_count_measure X" + by (simp add: X_not_empty partitions_finite(1) prob_space_uniform_count_measure) + have hP1exp: "P1.expectation (\ x. degree_normalized x Y) \ ?\" + using P1.expectation_uniform_count partitions_finite sum_degree_normalized_X_density by auto + let ?X1 = "{x \ X. (degree_normalized x Y \ ?\/2)}" + have hX1X: "?X1 \ X" and hX1card: "card ?X1 \ ?\ * (card X)/2" + and hX1degree: "\ x \ ?X1. degree_normalized x Y \ ?\ /2" using + P1.expectation_condition_card_1 partitions_finite degree_normalized_le_1 hP1exp by auto + have hX1cardpos: "card ?X1 > 0" using hX1card h\ X_not_empty + by (smt (verit, del_insts) divide_divide_eq_right divide_le_0_iff density_simp gr0I + less_eq_real_def mult_is_0 not_numeral_le_zero of_nat_le_0_iff of_nat_less_0_iff) + interpret H: fin_bipartite_graph "(?X1 \ Y)" "{e \ E. e \ (?X1 \ Y)}" "?X1" "Y" + proof (unfold_locales, simp add: partitions_finite) + have "disjoint {?X1, Y}" using hX1X partition_on_def partition + by (metis (no_types, lifting) disjnt_subset2 disjnt_sym ne pairwise_insert singletonD) + moreover have "{} \ {?X1, Y}" using hX1cardpos Y_not_empty + by (metis (no_types, lifting) card.empty insert_iff neq0_conv singleton_iff) + ultimately show "partition_on (?X1 \ Y) {?X1, Y}" using partition_on_def by auto + next + show "?X1 \ Y" using ne partition by (metis Int_absorb1 Y_not_empty hX1X part_intersect_empty) + next + show "\e. e \ {e \ E. e \ ?X1 \ Y} \ e \ all_bi_edges {x \ X. edge_density X Y / 2 \ + degree_normalized x Y} Y" + using Un_iff Y_verts_not_adj edge_betw_indiv in_mono insert_subset mem_Collect_eq + subset_refl that vert_adj_def all_bi_edges_def[of "?X1" "Y"] in_mk_uedge_img_iff + by (smt (verit, ccfv_threshold) all_edges_betw_I all_edges_between_bi_subset) + next + show "finite (?X1 \ Y)" using hX1X by (simp add: partitions_finite(1) partitions_finite(2)) + qed + have neighborhood_unchanged: "\ x \ ?X1. neighbors_ss x Y = H.neighbors_ss x Y" + using neighbors_ss_def H.neighbors_ss_def vert_adj_def H.vert_adj_def by auto + then have degree_unchanged: "\ x \ ?X1. degree x = H.degree x" + using H.degree_neighbors_ssX degree_neighbors_ssX by auto + have hHdensity: "(H.edge_density ?X1 Y) \ ?\ / 2" + proof- + have "?\ / 2 = (\ x \ ?X1. (?\ / 2)) / card ?X1" using hX1cardpos by auto + also have "... \ (\ x \ ?X1. degree_normalized x Y) / card ?X1" + using sum_mono hX1degree hX1cardpos divide_le_cancel + by (smt (z3) H.X_not_empty H.partitions_finite(1) + calculation divide_pos_pos h\ sum_pos zero_less_divide_iff) + also have "... = (H.edge_density ?X1 Y)" + using H.degree_normalized_def degree_normalized_def degree_unchanged sum.cong + H.degree_neighbors_ssX degree_neighbors_ssX H.sum_degree_normalized_X_density by auto + finally show ?thesis by simp + qed + have h\3pos: "?\^3 / 128 > 0" using h\ by auto + then obtain X2 where hX2subX1: "X2 \ ?X1" and hX2card: "card X2 \ (H.edge_density ?X1 Y) * + (card ?X1)/ (sqrt 2)" and hX2badtemp: "(card (H.bad_pair_set X2 Y (?\^3 / 128))) / real ((card X2)^2) + \ 2 * (?\^3 / 128) / (H.edge_density ?X1 Y)^2" using H.proportion_bad_pairs_subset_bipartite + by blast + have "(H.edge_density ?X1 Y) * (card ?X1)/ (sqrt 2) > 0" using hHdensity hX1cardpos h\ hX2card + by auto + then have hX2cardpos: "card X2 > 0" using hX2card by auto + then have hX2finite: "finite X2" using card_ge_0_finite by auto + have hX2bad: "(card (H.bad_pair_set X2 Y (?\^3 / 128))) \ (?\ / 16) * (card X2)^2" + proof- + have hpos: "real ((card X2)^2) > 0" using hX2cardpos by auto + have trivial: "(3:: nat) - 2 = 1" by simp + then have h\pow: "?\ ^ 3 / ?\ ^ 2 = ?\^1" using power_diff h\ + by (metis div_greater_zero_iff less_numeral_extra(3) numeral_Bit1_div_2 zero_less_numeral) + have "card (H.bad_pair_set X2 Y (?\^3 / 128)) \ (2 * (?\^3 / 128) / (H.edge_density ?X1 Y)^2) * + (card X2)^2" using hX2badtemp hX2cardpos by (simp add: field_simps) + also have "... \ (2 * (?\^3 / 128) / (?\ / 2)^2) * (card X2)^2" + using h\ hHdensity divide_left_mono frac_le hpos by (smt (verit) divide_pos_pos + edge_density_ge0 le_divide_eq power_mono zero_le_divide_iff zero_less_power) + also have "... = (?\^3 / ?\^2) * (1/16) * (card X2)^2" by (simp add: field_simps) + also have "... = (?\ / 16) * (card X2) ^ 2" using h\pow by auto + finally show ?thesis by simp + qed + let ?E_loops = "mk_edge ` {(x, x') | x x'. x \ X2 \ x' \ X2 \ + (H.codegree_normalized x x' Y) \ ?\ ^ 3 / 128}" + interpret \: ulgraph "X2" "?E_loops" + proof(unfold_locales) + show "\e. e \ ?E_loops \ e \ X2" by auto + next + have "\a b. a \ X2 \ b \ X2 \ 0 < card {a, b}" + by (meson card_0_eq finite.emptyI finite_insert insert_not_empty neq0_conv) + moreover have "\ a b. a \ X2 \ b \ X2 \ card {a, b} \ 2" + by (metis card_2_iff dual_order.refl insert_absorb2 is_singletonI + is_singleton_altdef one_le_numeral) + ultimately show "\e. e \ ?E_loops \ 0 < card e \ card e \ 2" by auto + qed + have h\_edges: "\ a b. a \ X2 \ b \ X2 \ + {a, b} \ ?E_loops \ H.codegree_normalized a b Y \ ?\^3/128" + proof + fix a b assume "{a, b} \ ?E_loops" + then show "H.codegree_normalized a b Y \ ?\^3/128" + using in_mk_uedge_img_iff[of "a" "b" "{(x, x') | x x'. x \ X2 \ x' \ X2 \ + (H.codegree_normalized x x' Y) \ ?\ ^ 3 / 128}"] doubleton_eq_iff H.codegree_normalized_sym + by auto + next + fix a b assume "a \ X2" and "b \ X2" and "H.codegree_normalized a b Y \ ?\^3/128" + then show "{a, b} \ ?E_loops" using in_mk_uedge_img_iff[of "a" "b" "{(x, x') | x x'. x \ X2 \ + x' \ X2 \ (H.codegree_normalized x x' Y) \ ?\ ^ 3 / 128}"] H.codegree_normalized_sym by auto + qed + interpret P2: prob_space "uniform_count_measure X2" + using hX2finite hX2cardpos prob_space_uniform_count_measure by fastforce + have hP2exp: "P2.expectation (\ x. \.degree_normalized x X2) \ 1 - ?\ / 16" + proof- + have h\all: "\.all_edges_between X2 X2 = (X2 \ X2) - H.bad_pair_set X2 Y (?\^3 / 128)" + proof + show "\.all_edges_between X2 X2 \ X2 \ X2 - H.bad_pair_set X2 Y (?\ ^ 3 / 128)" + proof + fix x assume "x \ \.all_edges_between X2 X2" + then obtain a b where "a \ X2" and "b \ X2" and "x = (a, b)" and + "H.codegree_normalized a b Y \ ?\^3 / 128" + using \.all_edges_between_def in_mk_uedge_img_iff h\_edges + by (smt (verit, del_insts) \.all_edges_betw_D3 \.wellformed_alt_snd edge_density_commute + mk_edge.cases mk_edge.simps that) + then show "x \ X2 \ X2 - H.bad_pair_set X2 Y (?\ ^ 3 / 128)" + using H.bad_pair_set_def H.bad_pair_def by auto + qed + next + show "X2 \ X2 - H.bad_pair_set X2 Y (?\ ^ 3 / 128) \ \.all_edges_between X2 X2" + using H.bad_pair_set_def H.bad_pair_def \.all_edges_between_def h\_edges by auto + qed + then have h\all_le: "card (\.all_edges_between X2 X2) \ (1 - ?\ / 16) * (card X2 * card X2)" + proof- + have hbadsub: "H.bad_pair_set X2 Y (?\ ^3 / 128) \ X2 \ X2" using H.bad_pair_set_def by auto + have "(1 - ?\ / 16) * (card X2 * card X2) = card (X2 \ X2) - ?\ / 16 * (card X2) ^2" + using card_cartesian_product power2_eq_square + by (metis Rings.ring_distribs(4) more_arith_simps(6) mult_of_nat_commute) + also have "... \ card (X2 \ X2) - card (H.bad_pair_set X2 Y (?\ ^ 3 / 128))" + using hX2bad by auto + also have "... = card (X2 \ X2 - H.bad_pair_set X2 Y (?\ ^ 3 / 128))" using card_Diff_subset + finite_cartesian_product[of "X2" "X2"] hX2finite hbadsub + by (metis (mono_tags, lifting) finite_subset) + finally show "card(\.all_edges_between X2 X2) \ (1 - ?\/16) * (card X2 * card X2)" + using h\all by simp + qed + have "1 - ?\ / 16 = ((1 - ?\ / 16) * (card X2 * card X2)) / (card X2 * card X2)" + using hX2cardpos by auto + also have "... \ card (\.all_edges_between X2 X2) / (card X2 * card X2)" + using h\all_le hX2cardpos divide_le_cancel of_nat_less_0_iff by fast + also have "... = (\ x \ X2. real (card (\.neighbors_ss x X2))) / card X2 / card X2" + using \.card_all_edges_betw_neighbor[of "X2" "X2"] hX2finite by (auto simp add: field_simps) + also have "... = (\ x \ X2. \.degree_normalized x X2) / card X2" + unfolding \.degree_normalized_def + using sum_divide_distrib[of "\ x. real (card (\.neighbors_ss x X2))" "X2" "card X2"] by auto + also have "... = P2.expectation (\ x. \.degree_normalized x X2)" + using P2.expectation_uniform_count hX2finite by auto + finally show ?thesis by simp + qed + let ?X' = "{x \ X2. \.degree_normalized x X2 \ 1 - ?\ / 8}" + have hX'subX2: "?X' \ X2" by blast + have hX'cardX2: "card ?X' \ card X2 / 2" using hX2finite divide_self h\ + P2.expectation_condition_card_2 [of "X2" "(\ x. \.degree_normalized x X2)" "?\ /8" "?\ / 16"] + hP2exp \.degree_normalized_le_1 by auto + interpret P3: prob_space "uniform_count_measure Y" + by (simp add: Y_not_empty partitions_finite(2) prob_space_uniform_count_measure) + have hP3exp: "P3.expectation (\ y. H.degree_normalized y X2) \ ?\ / 2" + proof- + have hHdegree_normalized: "\ x. x \ X2 \ (?\ / 2) \ H.degree_normalized x Y" + using hX1degree degree_normalized_def H.degree_normalized_def neighborhood_unchanged + hX2subX1 subsetD by (metis (no_types, lifting)) + have "?\ / 2 = (\ x \ X2. (?\ / 2)) / card X2" using hX2cardpos by auto + also have "... \ (\ x \ X2. real (card (H.neighbors_ss x Y))) / card Y / card X2" + using hHdegree_normalized sum_mono divide_le_cancel hX2cardpos of_nat_0_le_iff + H.degree_normalized_def sum.cong sum_divide_distrib by (smt (verit, best)) + also have "... = (card (H.all_edges_between Y X2)) / card X2 / card Y" + using H.card_all_edges_between_commute H.card_all_edges_betw_neighbor hX2finite + H.partitions_finite(2) by auto + also have "... = (\ y \ Y. real (card(H.neighbors_ss y X2))) / card X2 / card Y" using + H.card_all_edges_betw_neighbor hX2finite H.partitions_finite(2) by auto + also have "... = (\ y \ Y. H.degree_normalized y X2) / card Y" using H.degree_normalized_def + sum.cong sum_divide_distrib by (smt (verit, best)) + also have "... = P3.expectation (\ y. H.degree_normalized y X2)" + using P3.expectation_uniform_count H.partitions_finite(2) by auto + finally show ?thesis by linarith + qed + let ?Y' = "{x \ Y. H.degree_normalized x X2 \ ?\ / 4}" + have hY'subY: "?Y' \ Y" by blast + then have hY'card: "card ?Y' \ ?\ * card Y / 4" + using P3.expectation_condition_card_1[of "Y" "(\ y. H.degree_normalized y X2)" "?\ / 2"] H.partitions_finite(2) + hP3exp H.degree_normalized_le_1 by auto + + have hX2adjcard: "\ x y. x \ ?X' \ y \ ?Y' \ + card {x' \ X2. \.vert_adj x x' \ vert_adj y x'} \ ?\ / 8 * card X2" + proof- + fix x y assume hx: "x \ ?X'" and hy: "y \ ?Y'" + have hinter: "{x' \ X2. \.vert_adj x x' \ vert_adj y x'} = + {x' \ X2. \.vert_adj x x'} \ {x' \ X2. vert_adj y x'}" by auto + have huncardX2: "card ({x' \ X2. \.vert_adj x x'} \ {x' \ X2. vert_adj y x'}) \ card X2" + using card_mono hX2finite by fastforce + have fin1: "finite {x' \ X2. \.vert_adj x x'}" and fin2: "finite {x' \ X2. vert_adj y x'}" + using hX2finite by auto + have "{x' \ X2. \.vert_adj x x'} = \.neighbors_ss x X2" + using \.vert_adj_def vert_adj_def \.neighbors_ss_def hX2subX1 \.neighbors_ss_def by auto + then have hcard1: "card {x' \ X2. \.vert_adj x x'} \ (1 - ?\/8) * card X2" using hx + \.degree_normalized_def divide_le_eq hX2cardpos by (simp add: hX2card le_divide_eq) + have "{x' \ X2. vert_adj y x'} = H.neighbors_ss y X2" using H.vert_adj_def vert_adj_def + H.neighbors_ss_def hy hY'subY hX2subX1 H.neighbors_ss_def by auto + then have hcard2: "card {x' \ X2. vert_adj y x'} \ (?\ / 4) * card X2" + using hy H.degree_normalized_def divide_le_eq hX2cardpos by (simp add: hX2card le_divide_eq) + have "?\ / 8 * card X2 = (1 - ?\ / 8) * card X2 + ?\/4 * card X2 - card X2" + by (simp add: algebra_simps) + also have "... \ card {x' \ X2. \.vert_adj x x'} + card {x' \ X2. vert_adj y x'} - + card ({x' \ X2. \.vert_adj x x'} \ {x' \ X2. vert_adj y x'})" + using huncardX2 hcard1 hcard2 by linarith + also have "... = card {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" + using card_Un_Int fin1 fin2 hinter by fastforce + finally show "card {x' \ X2. \.vert_adj x x' \ vert_adj y x'} \ ?\ / 8 * card X2" + by linarith + qed + have hYpos: "real (card Y) > 0" using Y_not_empty partitions_finite(2) by auto + have "\ x y. x \ ?X' \ y \ ?Y' \ card {p. connecting_walk x y p \ walk_length p = 3} \ + (?\ ^ 3 / 128 * (card Y)) * ((?\ / 8) * (card X2))" + proof- + fix x y assume hx: "x \ ?X'" and hy: "y \ ?Y'" + then have hxV: "x \ V" and hyV: "y \ V" using hY'subY hX'subX2 hX2subX1 hX1X partitions_ss(1) + partitions_ss(2) subsetD by auto + define f:: "'a \ 'a list set" where "f \ (\ a. ((\ z. z @ [y]) ` {p. connecting_path x a p \ walk_length p = 2}))" + have h_norm: "\ a. a \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'} \ codegree_normalized x a Y \ ?\^3 / 128" + using \.vert_adj_def codegree_normalized_sym hx hX'subX2 subsetD + codegree_normalized_altX H.codegree_normalized_altX neighborhood_unchanged + h\_edges hX2subX1 hX1X by (smt (verit, del_insts) mem_Collect_eq) + have inj_concat: "inj (\ z. z @ [y])" using inj_def by blast + then have card_f_eq: "\ a. card (f a) = card {p. connecting_path x a p \ walk_length p = 2}" + using f_def card_image inj_eq by (smt (verit) inj_onI) + then have card_f_ge: "\ a. a \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'} \ + card (f a) \ ?\^3 / 128 * card Y" + using codegree_is_path_length_two codegree_normalized_def hYpos f_def h_norm by (simp add: field_simps) + have f_disjoint: "pairwise (\ s t. disjnt (f s) (f t)) {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" + proof (intro pairwiseI) + fix s t assume "s \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" and + "t \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" and "s \ t" + moreover have "\ a l. l \ f a \ l ! 2 = a" + proof- + fix a l assume "l \ f a" + then obtain z where hz: "z \ {p. connecting_path x a p \ walk_length p = 2}" and hlz: "l = z @ [y]" + using f_def by blast + then have "z ! 2 = a" using walk_length_conv connecting_path_def last_conv_nth + by (metis (mono_tags, lifting) diff_add_inverse length_tl list.sel(2) mem_Collect_eq + nat_1_add_1 one_eq_numeral_iff rel_simps(18)) + then show "l ! 2 = a" using hlz nth_append hz walk_length_conv less_diff_conv mem_Collect_eq + by (metis (mono_tags, lifting) nat_1_add_1 one_less_numeral_iff rel_simps(9)) + qed + ultimately show "disjnt (f s) (f t)" by (metis disjnt_iff) + qed + have hwalk_subset: "{p. connecting_walk x k p \ walk_length p = n} \ {p. set p \ V \ length p = n + 1}" for n k + using connecting_walk_def is_walk_def walk_length_conv by auto + have finite_walk: "finite {p. connecting_walk x k p \ walk_length p = n}" for n k + using finV finite_lists_length_eq finite_subset hwalk_subset[of "k" "n"] rev_finite_subset by blast + have f_finite: "\ A. A \ (f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'}) \ finite A" + proof- + fix A assume "A \ (f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'})" + then obtain a where "a \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" and hA: "A = f a" by blast + have "{p. connecting_path x a p \ walk_length p = 2} \ {p. connecting_walk x a p \ walk_length p = 2}" + using connecting_path_walk by blast + then have "finite {p. connecting_path x a p \ walk_length p = 2}" + using finite_walk finite_subset connecting_path_walk by blast + then show "finite A" using f_def hA by auto + qed + moreover have f_image_sub: + "(\ x \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}. f x) \ {p. connecting_walk x y p \ walk_length p = 3}" + proof(intro Union_least) + fix X assume "X \ f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" + then obtain a where ha: "a \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}" and haX: "f a = X" by blast + have "\z. connecting_path x a z \ walk_length z = 2 \ connecting_walk x y (z @ [y])" + proof- + fix z assume hpath: "connecting_path x a z" and hlen: "walk_length z = 2" + then obtain y' where "z ! 1 = y'" by blast + then have hz: "z = [x, y', a]" using list2_middle_singleton walk_length_conv + connecting_path_def hpath hlen add_diff_cancel_left' append_butlast_last_id + butlast.simps connecting_path_walk connecting_walk_def diff_diff_add diff_le_self + is_walk_not_empty is_walk_tl last_ConsL last_tl list.expand list.sel list.simps(3) + nat_1_add_1 le_imp_diff_is_add + by (metis (no_types, lifting) arith_simps(45) arithmetic_simps(2) numerals(1)) + moreover have hwalk: "connecting_walk x a z" using connecting_path_walk hpath by blast + then show "connecting_walk x y (z @ [y])" using connecting_walk_def is_walk_def + connecting_path_def is_gen_path_def is_walk_def ha hz hwalk hyV vert_adj_sym vert_adj_def by auto + qed + then show "X \ {p. connecting_walk x y p \ walk_length p = 3}" + using haX f_def walk_length_conv by auto + qed + ultimately have hUn_le: "card (\ x \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}. f x) \ card {p. connecting_walk x y p \ walk_length p = 3}" + using card_mono finite_walk[of "y" "3"] by blast + have "disjoint (f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'})" using f_disjoint pairwise_def + pairwise_image[of "disjnt" "f" "{x' \ X2. \.vert_adj x x' \ vert_adj y x'}"] by (metis (mono_tags, lifting)) + then have "card (\ (f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'})) = sum card (f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'})" + using card_Union_disjoint[of "f ` {x' \ X2. \.vert_adj x x' \ vert_adj y x'}"] f_finite by blast + also have "... = (\ a \ {x' \ X2. \.vert_adj x x' \ vert_adj y x'}. card (f a))" + using sum_card_image[OF _ f_disjoint] hX2finite finite_subset by fastforce + also have "... \ card {x' \ X2. \.vert_adj x x' \ vert_adj y x'} * ?\^3 / 128 * card Y" + using sum_mono[of "{x' \ X2. \.vert_adj x x' \ vert_adj y x'}" "(\ a. ?\^3 / 128 * card Y)" "(\ a. card (f a))"] + card_f_ge by auto + finally have "card {x' \ X2. \.vert_adj x x' \ vert_adj y x'} * ?\^3 / 128 * card Y \ card {p. connecting_walk x y p \ walk_length p = 3}" + using hUn_le by linarith + then have "(?\ ^ 3 / 128 * (card Y)) * card {x' \ X2. \.vert_adj x x' \ vert_adj y x'} \ card {p. connecting_walk x y p \ walk_length p = 3}" + by argo + then show "(?\ ^ 3 / 128 * (card Y)) * ((?\ / 8) * (card X2)) \ card {p. connecting_walk x y p \ walk_length p = 3}" + using hX2adjcard[OF hx hy] hYpos mult_left_mono h\3pos mult_pos_pos + by (smt (verit, del_insts)) + qed + moreover have hX2cardX: "card X2 \ (?\ ^2 / 8) *(card X)" + proof- + have "card X2 \ (H.edge_density ?X1 Y / sqrt 2) * (card ?X1)" + using hX2card by (simp add: algebra_simps) + moreover have "(H.edge_density ?X1 Y / sqrt 2) * (card ?X1) \ (?\ / (2 * sqrt 2)) * card ?X1" + using hHdensity hX1cardpos by (simp add: field_simps) + moreover have "(?\ / (2 * sqrt 2)) * card ?X1 \ (?\ / 4) * card ?X1" + using sqrt2_less_2 hX1cardpos h\ by (simp add: field_simps) + moreover have "(?\ / 4) * card ?X1 \ (?\ / 4) * (?\ / 2 * card X)" + using hX1card h\ by (simp add: field_simps) + moreover have "(?\ / 4) * (?\ / 2 * card X) = (?\ ^2 / 8) *(card X)" using power2_eq_square + by (metis (no_types, opaque_lifting) Groups.mult_ac(2) Groups.mult_ac(3) divide_divide_eq_left + num_double numeral_times_numeral times_divide_eq_left times_divide_eq_right) + ultimately show ?thesis by linarith + qed + moreover have "(?\ ^ 3 / 128 * (card Y)) * ((?\ / 8) * (card X2)) \ + ?\ ^ 6 * card X * card Y / 2 ^ 13" + proof- + have hinter: "(?\ / 8) * (?\ ^2 / 8 * card X) \ (?\ / 8) * (card X2)" + using hX2cardX h\ by (simp add: algebra_simps) + have "?\ ^ 6 * real (card X * card Y) / 2 ^ 13 = + ?\ ^ 3 * ?\ * ?\ ^ 2 * real (card X * card Y) / (128 * 8 * 8)" by algebra + also have "... = (?\ ^ 3 / 128 * (card Y)) * ((?\ / 8) * (?\ ^2 / 8 * card X))" by auto + also have "... \ (?\ ^ 3 / 128 * (card Y)) * ((?\ / 8) * (card X2))" + using hinter hYpos h\ power3_eq_cube + by (smt (verit) \0 < edge_density X Y ^ 3 / 128\ mult_left_mono zero_compare_simps(6)) + finally show ?thesis by simp + qed + moreover have hX'card: "card ?X' \ ?\ ^ 2 * card X / 16" using hX'cardX2 hX2cardX by auto + moreover have hX'subX: "?X' \ X" using hX'subX2 hX2subX1 hX1X by auto + ultimately show ?thesis using hY'card hX'card hY'subY hX'subX that + by (smt (verit, best)) +next + assume "\ 0 < edge_density X Y" + then have "edge_density X Y = 0" by (smt (verit, ccfv_threshold) edge_density_ge0) + then show "?thesis" using that by auto +qed + + +text\The following lemma corresponds to Lemma 2.17 in Gowers's notes \cite{Gowersnotes}. \ + +text\ Note that here we have set(@{term "additive_energy A = 2 * c"} (instead of +(@{term "additive_energy A = c"} as in the notes) and we are accordingly considering c-popular +differences (instead of c/2-popular differences as in the notes) so that we will still have +(@{term "\ = additive_energy A / 2"}.\ + +lemma popular_differences_card: fixes A::"'a set" and c::real + assumes "finite A" and "A \ G" and "additive_energy A = 2 * c" + shows "card (popular_diff_set c A) \ c * card A" + (* typo in the notes, square must not be there *) + +proof(cases "card A \ 0") + assume hA: "card A \ 0" + have hc: "c \ 0" using assms additive_energy_def of_nat_0_le_iff + by (smt (verit, best) assms(3) divide_nonneg_nonneg of_nat_0_le_iff) + have "(2 * c) * (card A)^3 = (\d \ (differenceset A A). (f_diff d A)^2)" + using assms f_diff_card_quadruple_set_additive_energy by auto + also have "...= ((\d \ (popular_diff_set c A). (f_diff d A)^2)) + +((\ d \ ((differenceset A A) - (popular_diff_set c A)). (f_diff d A)^2))" + using popular_diff_set_def assms finite_minusset finite_sumset by (metis (no_types, lifting) + add.commute mem_Collect_eq subsetI sum.subset_diff) + also have "... \ ((card (popular_diff_set c A)) * (card A)^2) + + c * card A * ((\d \ (differenceset A A - (popular_diff_set c A)) . (f_diff d A)))" + proof- + have "\ d \ ((differenceset A A) - (popular_diff_set c A)) . (f_diff d A)^2 \ + (c * (card A)) * (f_diff d A)" + proof + fix d assume hd1: "d \ differenceset A A - popular_diff_set c A" + have hnonneg: "f_diff d A \ 0" by auto + have "\ popular_diff d c A" using hd1 popular_diff_set_def by blast + from this have "f_diff d A \ c * card A" using popular_diff_def by auto + thus "real ((f_diff d A)\<^sup>2) \ c * real (card A) * real (f_diff d A)" + using power2_eq_square hnonneg mult_right_mono of_nat_0 of_nat_le_iff of_nat_mult by metis + qed + moreover have "\ d \ (differenceset A A) . f_diff d A \ (card A)^2" + using f_diff_def finite_minusset finite_sumset assms + by (metis f_diff_le_card le_antisym nat_le_linear power2_nat_le_imp_le) + ultimately have "((\d \ ((differenceset A A) - popular_diff_set c A) . (f_diff d A)^2)) \ + ((\d \ ((differenceset A A) - popular_diff_set c A). (c * card A) * (f_diff d A)))" + using assms finite_minusset finite_sumset sum_distrib_left sum_mono by fastforce + then have "((\d \ ((differenceset A A) - popular_diff_set c A) . (f_diff d A)^2)) \ + (c * card A) * ((\d \ ((differenceset A A) - popular_diff_set c A) . (f_diff d A)))" + by (metis (no_types) of_nat_sum sum_distrib_left) + moreover have "(\d \ popular_diff_set c A. (f_diff d A)^2) \ + (\d \ popular_diff_set c A. (card A)^2)" using f_diff_le_card assms sum_mono assms popular_diff_set_def + by (metis (no_types, lifting) power2_nat_le_eq_le) + moreover then have ddd: "(\d \ popular_diff_set c A . (f_diff d A)^2) \ + (card (popular_diff_set c A)) * (card A)^2" + using sum_distrib_right by simp + ultimately show ?thesis by linarith + qed + also have "... \ ((card (popular_diff_set c A)) * (card A)^2) + (c * card A) * (card A)^2" + proof- + have "(\d \ (differenceset A A - popular_diff_set c A) . (f_diff d A)) \ + (\d \ differenceset A A . (f_diff d A))" using DiffD1 subsetI assms sum_mono2 + finite_minusset finite_sumset zero_le by metis + then have "(c * card A) * ((\d \ (differenceset A A - popular_diff_set c A). (f_diff d A))) + \ (c * card A) * (card A)^2" + using f_diff_card hc le0 mult_left_mono of_nat_0 of_nat_mono zero_le_mult_iff assms by metis + then show ?thesis by linarith + qed + finally have "(2 * c) * (card A)^3 \ ((card (popular_diff_set c A)) * (card A)^2) + + (c * card A) * (card A)^2" by linarith + then have "(card (popular_diff_set c A)) \ + ((2 * c) * (card A)^3 - (c * card A) * (card A)^2)/((card A)^2)" + using hA by (simp add: field_simps) + moreover have "((2 * c)* (card A)^3 - (c * card A) * (card A)^2)/((card A)^2) = 2 * c * card A - c * card A" + using hA by (simp add: power2_eq_square power3_eq_cube) + ultimately show ?thesis by linarith +next + assume "\ card A \ 0" + thus ?thesis by auto +qed + + +text\The following lemma corresponds to Lemma 2.18 in Gowers's notes \cite{Gowersnotes}. It includes the key argument +of the main proof and its proof applies Lemmas 2.16 (@{term walks_of_length_3_subsets_bipartite}) +and 2.17 (@{term popular_differences_card}). In the proof we will use an appropriately defined +bipartite graph as an intermediate/auxiliary construct so as to apply lemma +@{term walks_of_length_3_subsets_bipartite}. As each vertex set of the bipartite graph is constructed +to be a copy of a finite subset of an Abelian group, we need flexibility regarding types, which is +what prompted the introduction and use of the new graph theory library \cite{Undirected_Graph_Theory-AFP} (that does not impose any type +restrictions e.g. by representing vertices as natural numbers). \ + +lemma obtains_subsets_differenceset_card_bound: + fixes A::"'a set" and c::real + assumes "finite A" and "c>0" and "A \ {}" and "A \ G" and "additive_energy A = 2 * c" + obtains B and A' where "B \ A" and "B \ {}" and "card B \ c^4 * card A / 16" + and "A' \ A" and "A' \ {}" and "card A' \ c^2 * card A / 4" + and "card (differenceset A' B) \ 2^13 * card A / c^15" + +proof- + let ?X = "A \ {0:: nat}" (* Is this the best way to tag? *) + let ?Y = "A \ {1:: nat}" + let ?E = "mk_edge ` {(x, y)| x y. x \ ?X \ y \ ?Y \ (popular_diff (fst y \ fst x) c A)}" + interpret H: fin_bipartite_graph "?X \ ?Y" ?E ?X ?Y + proof (unfold_locales, auto simp add: partition_on_def assms(3) assms(1) disjoint_def) + show "{} = A \ {0} \ False" using assms(3) by auto + next + show "{} = A \ {Suc 0} \ False" using assms(3) by auto + next + show "A \ {0} = A \ {Suc 0} \ False" using assms(3) by fastforce + next + fix x y assume "x \ A" and "y \ A" and "popular_diff (y \ x) c A" + thus "{(x, 0), (y, Suc 0)} \ all_bi_edges (A \ {0}) (A \ {Suc 0})" + using all_bi_edges_def[of "A \ {0}" "A \ {Suc 0}"] + by (simp add: in_mk_edge_img) + qed + have edges1: "\ a \ A. \ b \ A. ({(a, 0), (b, 1)} \ ?E \ popular_diff (b \ a) c A)" + by (auto simp add: in_mk_uedge_img_iff) + have hXA: "card A = card ?X" by (simp add: card_cartesian_product) + have hYA: "card A = card ?Y" by (simp add: card_cartesian_product) + have hA: "card A \ 0" using assms card_0_eq by blast + have edge_density: "H.edge_density ?X ?Y \ c^2" + proof- + define f:: "'a \ ('a \ nat) edge set" where "f \ (\ x. {{(a, 0), (b, 1)} | a b. + a \ A \ b \ A \ b \ a = x})" + have f_disj: "pairwise (\ s t. disjnt (f s) (f t)) (popular_diff_set c A)" + proof (intro pairwiseI) + fix x y assume hx: "x \ popular_diff_set c A" and hy: "y \ popular_diff_set c A" + and hxy: "x \ y" + show "disjnt (f x) (f y)" + proof- + have "\a. \ (a \ f x \ a \ f y)" + proof (intro allI notI) + fix a assume "a \ f x \ a \ f y" + then obtain z w where hazw: "a = {(z, 0), (w, 1)}" and hx: "{(z,0), (w, 1)} \ f x" + and hy: "{(z, 0), (w, 1)} \ f y" using f_def by blast + have "w \ z = x" using f_def hx by (simp add: doubleton_eq_iff) + moreover have "w \ z = y" using f_def hy by (simp add: doubleton_eq_iff) + ultimately show "False" using hxy by auto + qed + thus ?thesis using disjnt_iff by auto + qed + qed + have f_sub_edges: "\ d \ popular_diff_set c A. (f d) \ ?E" + using popular_diff_set_def f_def edges1 by auto + have f_union_sub: "(\ d \ popular_diff_set c A. (f d)) \ ?E" using popular_diff_set_def + f_def edges1 by auto + have f_disj2: "disjoint (f ` (popular_diff_set c A))" using f_disj + pairwise_image[of "disjnt" "f" "popular_diff_set c A"] by (simp add: pairwise_def) + have f_finite: "\B. B \ f ` popular_diff_set c A \ finite B" + using finite_subset f_sub_edges H.fin_edges by auto + have card_eq_f_diff: "\ d \ popular_diff_set c A. card (f d) = f_diff d A" + proof + fix d assume "d \ popular_diff_set c A" + define g:: "('a \ 'a) \ ('a \ nat) edge" where "g = (\ (a, b). {(b, 0), (a, 1)})" + have g_inj: "inj_on g {(a, b) | a b. a \ A \ b \ A \ a \ b = d}" + 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 hg: "g x = g y" + then obtain a1 a2 b1 b2 where hx: "x = (a1, a2)" and hy: "y = (b1, b2)" by blast + thus "x = y" using g_def hg hx hy by (simp add: doubleton_eq_iff) + qed + have g_image: "g ` {(a, b) |a b. a \ A \ b \ A \ a \ b = d} = f d" using f_def g_def by auto + show "card (f d) = f_diff d A" using card_image g_inj g_image f_diff_def by fastforce + qed + have "c ^ 2 * (card A) ^ 2 = c * (card A) * (c * (card A))" using power2_eq_square + by (metis of_nat_power power_mult_distrib) + also have "... \ (card (popular_diff_set c A)) * (c * (card A))" + using assms popular_differences_card hA by force + also have "... \ (\ d \ popular_diff_set c A. f_diff d A)" using sum_mono popular_diff_set_def + popular_diff_def by (smt (verit, ccfv_SIG) mem_Collect_eq of_nat_sum of_real_of_nat_eq + sum_constant) + also have "... = (\ d \ popular_diff_set c A. card (f d))" + using card_eq_f_diff sum.cong by auto + also have "... = sum card (f ` (popular_diff_set c A))" + using f_disj sum_card_image[of "popular_diff_set c A" "f"] popular_diff_set_def + finite_minusset finite_sumset assms(1) finite_subset by auto + also have "... = card (\ d \ popular_diff_set c A. (f d))" + using card_Union_disjoint[of "f ` (popular_diff_set c A)"] f_disj2 f_finite by auto + also have "... \ card ?E" using card_mono f_union_sub H.fin_edges by auto + finally have "c ^ 2 * (card A) ^ 2 \ card ?E" by linarith + then have "c ^ 2 * (card A) ^ 2 \ card (H.all_edges_between ?X ?Y)" + using H.card_edges_between_set by auto + moreover have "H.edge_density ?X ?Y = card (H.all_edges_between ?X ?Y) / (card A) ^ 2" + using H.edge_density_def power2_eq_square hXA hYA + by (smt (verit, best)) + ultimately have "(c ^ 2 * (card A) ^ 2) / (card A) ^ 2 \ H.edge_density ?X ?Y" using hA + divide_le_cancel by (smt (verit, del_insts) H.edge_density_ge0 \c\<^sup>2 * real ((card A)\<^sup>2) = + c * real (card A) * (c * real (card A))\ divide_divide_eq_right zero_le_divide_iff) + thus ?thesis using hA assms(2) by auto + qed + obtain X' and Y' where X'sub: "X' \ ?X" and Y'sub: "Y' \ ?Y" and + hX': "card X' \ (H.edge_density ?X ?Y)^2 * (card ?X)/16" and + hY': "card Y' \ (H.edge_density ?X ?Y) * (card ?Y)/4" and + hwalks: "\ x \ X'. \ y \ Y'. card ({p. H.connecting_walk x y p \ H.walk_length p = 3}) + \ (H.edge_density ?X ?Y)^6 * card ?X * card ?Y / 2^13" + using H.walks_of_length_3_subsets_bipartite \c>0\ by auto + have "((c^2)^2) * (card A) \ (H.edge_density ?X ?Y)^2 * (card A)" + using edge_density assms(2) hA power_mono zero_le_power2 mult_le_cancel_right + by (smt (verit) of_nat_less_of_nat_power_cancel_iff of_nat_zero_less_power_iff + power2_less_eq_zero_iff power_0_left) + then have cardX': "card X' \ (c^4) * (card A)/16" using hX' divide_le_cancel hXA by fastforce + have "c^2 * (card A) / 4 \ (H.edge_density ?X ?Y) * card ?Y / 4" using hYA hA edge_density + mult_le_cancel_right by simp + then have cardY': "card Y' \ c^2 * (card A)/4" using hY' by linarith + have "(H.edge_density ?X ?Y)^6 * (card ?X * card ?Y)/ 2^13 \ (c^2)^6 * ((card A)^2) / 2^13" using + hXA hYA power2_eq_square edge_density divide_le_cancel mult_le_cancel_right hA + by (smt (verit, ccfv_SIG) of_nat_power power2_less_0 power_less_imp_less_base zero_le_power) + then have card_walks: "\ x \ X'. \ y \ Y'. + card ({p. H.connecting_walk x y p \ H.walk_length p = 3}) \ (c^12) * ((card A)^2) / 2^13" + using hwalks by fastforce + (* ?X and ?Y are subsets of the vertex set, now project down to G, giving subsets ?B and ?C of A, + respectively*) + let ?B = "(\ (a, b). a) ` X'" + let ?C = "(\ (a, b). a) ` Y'" + have hBA: "?B \ A" and hCA: "?C \ A" using Y'sub X'sub by auto + have inj_on_X': "inj_on (\ (a, b). a) X'" using X'sub by (intro inj_onI) (auto) + have inj_on_Y': "inj_on (\ (a, b). a) Y'" using Y'sub by (intro inj_onI) (auto) + have hBX': "card ?B = card X'" and hCY': "card ?C = card Y'" + using card_image inj_on_X' inj_on_Y' by auto + then have cardB: "card ?B \ (c^4) * (card A)/16" and cardC: "card ?C \ c^2 * (card A)/4" + using cardX' cardY' by auto + have card_ineq1: "\ x y. x \ ?B \ y \ ?C \ card ({(z, w) | z w. z \ A \ w \ A \ + popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ popular_diff (y \ w) c A}) \ + (c^12) * ((card A)^2) / 2^13" + proof- + fix x y assume hx: "x \ ?B" and hy: "y \ ?C" + have hxA: "x \ A" and hyA: "y \ A" using hx hy hBA hCA by auto + define f:: "'a \ 'a \ ('a \ nat) list" + where "f \ (\ (z, w). [(x, 0), (z, 1), (w, 0), (y, 1)])" + have f_inj_on: "inj_on f {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" using f_def by (intro inj_onI) (auto) + have f_image: "f ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} = + {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + proof + show "f ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} \ + {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + proof + fix p assume hp: "p \ f ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" + then obtain z w where hz: "z \ A" and hw: "w \ A" and hzx: "popular_diff (z \ x) c A" and + hzw: "popular_diff (z \ w) c A" and hyw: "popular_diff (y \ w) c A" and + hp: "p = [(x, 0), (z, 1), (w, 0), (y, 1)]" using f_def hp by fast + then have hcon: "H.connecting_walk (x, 0) (y, 1) p" + unfolding H.connecting_walk_def H.is_walk_def + using hxA hyA H.vert_adj_def H.vert_adj_sym edges1 by simp + thus "p \ {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + using hp H.walk_length_conv by auto + qed + next + show "{p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3} \ f ` {(z, w) |z w. + z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A}" + proof(intro subsetI) + fix p assume hp: "p \ {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + then have len: "length p = 4" using H.walk_length_conv by auto + have hpsub: "set p \ A \ {0} \ A \ {1}" using hp H.connecting_walk_def H.is_walk_def + by auto + then have fst_sub: "fst ` set p \ A" by auto + have h1A: "fst (p!1) \ A" and h2A: "fst (p!2) \ A" using fst_sub len by auto + have hpnum: "p = [p!0, p!1, p!2, p!3]" + proof (auto simp add: list_eq_iff_nth_eq len) + fix k assume "k < (4:: nat)" + then have "k = 0 \ k = 1 \ k = 2 \ k = 3" by auto + thus "p ! k = [p ! 0, p ! Suc 0, p ! 2, p ! 3] ! k" by fastforce + qed + then have "set (H.walk_edges p) = {{p!0, p!1} , {p!1, p!2}, {p!2, p!3}}" using + comp_sgraph.walk_edges.simps(2) comp_sgraph.walk_edges.simps(3) + by (metis empty_set list.simps(15)) + then have h1: "{p!0, p!1} \ ?E" and h2: "{p!2, p!1} \ ?E" and h3: "{p!2, p!3} \ ?E" + using hp H.connecting_walk_def H.is_walk_def len by auto + have hxp: "p!0 = (x, 0)" using hp len hd_conv_nth H.connecting_walk_def H.is_walk_def + by fastforce + have hyp: "p!3 = (y,1)" using hp len last_conv_nth H.connecting_walk_def H.is_walk_def + by fastforce + have h1p: "p!1 = (fst (p!1), 1)" + proof- + have "p!1 \ A \ {0} \ A \ {1}" using hpnum hpsub + by (metis (no_types, lifting) insertCI list.simps(15) subsetD) + then have hsplit: "snd (p!1) = 0 \ snd (p!1) = 1" by auto + then have "snd (p!1) = 1" + proof(cases "snd (p!1) = 0") + case True + then have 1: "{(x, 0), (fst (p!1), 0)} \ ?E" using h1 hxp doubleton_eq_iff + by (smt (verit, del_insts) surjective_pairing) + have hY: "(fst (p!1), 0) \ ?Y" and hX: "(x, 0) \ ?X" using hxA by auto + then have 2: "{(x, 0), (fst (p!1), 0)} \ ?E" using H.X_vert_adj_Y H.vert_adj_def by meson + then show ?thesis using 1 2 by blast + next + case False + then show ?thesis using hsplit by auto + qed + thus "(p ! 1) = (fst (p ! 1), 1)" + by (metis (full_types) split_pairs) + qed + have h2p: "p!2 = (fst (p!2), 0)" + proof- + have "p!2 \ A \ {0} \ A \ {1}" using hpnum hpsub + by (metis (no_types, lifting) insertCI list.simps(15) subsetD) + then have hsplit: "snd (p!2) = 0 \ snd (p!2) = 1" by auto + then have "snd (p!2) = 0" + proof(cases "snd (p!2) = 1") + case True + then have 1: "{(fst (p!2), 1), (y, 1)} \ ?E" using h3 hyp doubleton_eq_iff + by (smt (verit, del_insts) surjective_pairing) + have hY: "(y, 1) \ ?X" and hX: "(fst (p!2), 1) \ ?Y" using hyA h2A by auto + then have 2: "{(fst (p!2), 1), (y, 1)} \ ?E" using H.Y_vert_adj_X H.vert_adj_def + by meson + then show ?thesis using 1 2 by blast + next + case False + then show ?thesis using hsplit by auto + qed + thus "(p ! 2) = (fst (p ! 2), 0)" + by (metis (full_types) split_pairs) + qed + have hpop1: "popular_diff ((fst (p!1)) \ x) c A" using edges1 h1 hxp h1p hxA h1A + by (smt (z3)) + have hpop2: "popular_diff((fst (p!1)) \ (fst (p!2))) c A" using edges1 h2 h1p h2p h1A h2A + by (smt (z3)) + have hpop3: "popular_diff (y \ (fst (p!2))) c A" using edges1 h3 h2p hyp hyA h2A + by (smt (z3)) + thus "p \ f ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" using f_def hpnum hxp h1p h2p hyp + h1A h2A hpop1 hpop2 hpop3 by force + qed + qed + have hx1: "(x, 0) \ X'" and hy2: "(y, 1) \ Y'" using hx X'sub hy Y'sub by auto + have "card {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} = + card {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + using card_image f_inj_on f_image by fastforce + thus "card {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} \ c ^ 12 * ((card A)^2) / 2 ^ 13" + using hx1 hy2 card_walks by auto + qed + have card_ineq2: "\ x y z w. x \ ?B \ y \ ?C \ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ + popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ popular_diff (y \ w) c A} \ + card {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} \ c^3 * card A^3" + proof (auto) + fix x x2 y y2 z w assume "(x, x2) \ X'" and "(y, y2) \ Y'" and "z \ A" and "w \ A" and + 1: "popular_diff (z \ x) c A" and 2: "popular_diff (z \ w) c A" and + 3: "popular_diff (y \ w) c A" + define f:: "'a \ 'a \ 'a \ 'a \ 'a \ 'a \ ('a \ 'a) \ ('a \ 'a) \ ('a \ 'a)" where + "f \ (\ (p, q, r, s, t, u). ((p, q), (r, s), (t, u)))" + (* Types ('a \ 'a \ 'a \ 'a \ 'a \ 'a) and ('a \ 'a) \ ('a \ 'a) \ ('a \ 'a) are not + definitionally equal, so we need to define a bijection between them *) + have f_inj: "inj_on f {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" using f_def + by (intro inj_onI) (auto) + have f_image: "f ` {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} = + {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} \ + {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" using f_def by force (*slow *) + have "card {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} = card ({(p, q). p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q). p \ A \ q \ A \ p \ q = z \ w} \ {(p, q). p \ A \ q \ A \ p \ q = y \ w})" + using card_image f_inj f_image by fastforce + moreover have "card ({(p, q). p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q). p \ A \ q \ A \ p \ q = z \ w} \ {(p, q). p \ A \ q \ A \ p \ q = y \ w}) = + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" + using card_cartesian_product3 by auto + moreover have "c * card A \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x}" + using 1 popular_diff_def f_diff_def by auto + moreover then have "(c * card A) * (c * card A) \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} + * card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w}" + using 2 popular_diff_def f_diff_def mult_mono assms(2) mult_nonneg_nonneg + of_nat_0_le_iff of_nat_mult by fastforce + moreover then have "(c * card A) * (c * card A) * (c * card A) \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} + * card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" + using 3 popular_diff_def f_diff_def mult_mono assms(2) mult_nonneg_nonneg of_nat_0_le_iff + of_nat_mult by fastforce + moreover have "c ^ 3 * card A ^ 3 = (c * card A) * ((c * card A) * (c * card A))" + by (simp add: power3_eq_cube algebra_simps) + ultimately show "c ^ 3 * real (card A) ^ 3 \ + (card {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" by auto + qed + have card_ineq3: "\ x y. x \ ?B \ y \ ?C \ card (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ + popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) \ + c ^ 15 * ((card A)^5) / 2 ^ 13" + proof- + fix x y assume hx: "x \ ?B" and hy: "y \ ?C" + have hxG: "x \ G" and hyG: "y \ G" using hx hy hBA hCA assms(4) by auto + let ?f = "(\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + have h_pairwise_disjnt: "pairwise (\ a b. disjnt (?f a) (?f b)) + {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A}" + proof (intro pairwiseI) + fix a b assume "a \ {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" "b \ {(z, w) |z w. z \ A \ w \ A \ + popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" and + "a \ b" + then obtain a1 a2 b1 b2 where ha: "a = (a1, a2)" and hb: "b = (b1, b2)" and ha1: "a1 \ G" and + ha2: "a2 \ G" and hb1: "b1 \ G" and hb2: "b2 \ G" and hne: "(a1, a2) \ (b1, b2)" + using assms(4) by blast + have "(\x. \ (x \ (?f a) \ x \ (?f b)))" + proof(intro allI notI) + fix d assume "d \ (?f a) \ d \ (?f b)" + then obtain p q r s t u where "d = (p, q, r, s, t, u)" and hpq1: "p \ q = a1 \ x" and + htu1: "t \ u = y \ a2" and hpq2: "p \ q = b1 \ x" and htu2: "t \ u = y \ b2" + using ha hb by auto + then have "y \ a2 = y \ b2" using htu1 htu2 by auto + then have 2: "a2 = b2" using ha2 hb2 hyG + by (metis additive_abelian_group.inverse_closed additive_abelian_group_axioms + invertible invertible_inverse_inverse invertible_left_cancel) + have 1: "a1 = b1" using hpq1 hpq2 ha1 hb1 hxG by simp + show "False" using 1 2 hne by auto + qed + thus "disjnt (?f a) (?f b)" using disjnt_iff[of "(?f a)" "(?f b)"] by auto + qed + have hfinite_walks: "\ B. B \ ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A}) \ finite B" + proof- + fix B assume "B \ ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A})" + then have "B \ A \ A \ A \ A \ A \ A" by auto + thus "finite B" using assms(1) + by (auto simp add: finite_subset) + qed + have hdisj: "disjoint ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A})" using h_pairwise_disjnt pairwise_image[of "disjnt" "(\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + "{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A}"] by (simp add: pairwise_def) + have "{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} \ A \ A" by auto + then have hwalks_finite: "finite {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" using finite_subset assms(1) + by fastforce + have f_ineq: "\ a \ {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. c ^ 3 * (card A) ^ 3 \ + card (?f a)" using card_ineq2 hx hy by auto + have "c ^ 15 * ((card A)^5) / 2 ^ 13 = (c ^ 12 * (card A) ^ 2 / 2 ^ 13) * (c ^ 3 * card A ^ 3)" + by (simp add: algebra_simps) + also have "... \ card {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A} * (c ^ 3 * (card A) ^ 3)" + using card_ineq1[of "x" "y"] hx hy mult_le_cancel_right hA by (smt (verit, best) assms(2) + mult_pos_pos of_nat_0_less_iff of_nat_le_0_iff zero_less_power) + also have "... = (\ a \ {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. (c ^ 3 * (card A) ^ 3))" by auto + also have "... \ (\a\{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. card (?f a))" + using sum_mono f_ineq by (smt (verit, del_insts) of_nat_sum) + also have "... = sum card (?f ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A})" + using sum_card_image[of "{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" "?f"] h_pairwise_disjnt hwalks_finite by auto + also have "... = card (\ (z, w)\{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ + t \ u = y \ w})" using card_Union_disjoint hfinite_walks hdisj by (metis (no_types, lifting)) + finally show "c ^ 15 * real (card A ^ 5) / 2 ^ 13 \ real (card (\(z, w)\{(z, w) |z w. + z \ A \ w \ A \ popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ + popular_diff (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}))" by simp + qed + have hdsub: "\ d \ differenceset ?C ?B. \ y \ ?C. \ x \ ?B. + (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" + proof + fix d assume "d \ differenceset ?C ?B" + then obtain y x where hy: "y \ ?C" and hx: "x \ ?B" and hxy: "d = y \ x" + using sumset_def minusset_def hBA hCA assms(4) subset_trans + by (smt (verit, best) minusset.simps sumset.cases) + have hxG: "x \ G" and hyG: "y \ G" using hx hy hBA hCA assms(4) by auto + have "(\(z, w)\{(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + d = p \ q \ r \ s \ t \ u}" + proof (rule Union_least) + fix X assume "X \ (\(z, w). {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ + t \ u = y \ w}) ` {(z, w) |z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}" + then obtain z w where hX: "X = {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" + and hz: "z \ A" and hw: "w \ A" by auto + have hzG: "z \ G" and hwG: "w \ G" using hz hw assms(4) by auto + have "{(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} \ + {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + d = p \ q \ r \ s \ t \ u}" + proof + fix e assume "e \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" + then obtain p q r s t u where "p \ q = z \ x" and "r \ s = z \ w" and "t \ u = y \ w" + and hp: "p \ A" and hq: "q \ A" and hr: "r \ A" and hs: "s \ A" and ht: "t \ A" + and hu: "u \ A" and he: "e = (p, q, r, s, t, u)" by blast + then have "p \ q \ r \ s \ t \ u = (z \ x) \ (z \ w) \ (y \ w)" + by (smt (z3) additive_abelian_group.inverse_closed additive_abelian_group_axioms assms(4) + associative commutative_monoid.commutative commutative_monoid_axioms composition_closed + invertible invertible_inverse_inverse monoid.inverse_composition_commute monoid_axioms subsetD) + also have "... = (w \ x) \ (y \ w)" using hxG hyG hzG hwG associative commutative + inverse_composition_commute invertible_right_inverse2 by auto + also have "... = y \ x" using hxG hwG hyG associative commutative + by (simp add: monoid.invertible_right_inverse2 monoid_axioms) + finally have "p \ q \ r \ s \ t \ u = d" using hxy by simp + thus "e \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ + u \ A \ d = p \ q \ r \ s \ t \ u}" using he hp hq hr hs ht hu by auto + qed + thus "X \ {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" + using hX by auto + qed + thus "\y\(\(a, b). a) ` Y'. \x\(\(a, b). a) ` X'. (\(z, w)\{(z, w) |z w. z \ A \ w \ A \ + popular_diff (z \ x) c A \ popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. + {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) \ {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" + using hx hy by meson + qed + have pos: "0 < c ^ 15 * real (card A ^ 5) / 2 ^ 13" using hA \c>0\ by auto + have "(5:: nat) \ 6" by auto + then have "(card A ^ 6 / card A ^ 5) = (card A) ^ (6 - 5)" + using hA power_diff by (metis of_nat_eq_0_iff of_nat_power) + then have cardApow: "(card A ^ 6 / card A ^ 5) = card A" using power_one_right by simp + moreover have "\ d \ differenceset ?C ?B. card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)} \ c ^ 15 * (card A) ^ 5 / 2 ^13" + proof + fix d assume "d \ differenceset ?C ?B" + then obtain x y where hy: "y \ ?C" and hx: "x \ ?B" and hsub: + "(\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" using hdsub by meson + have "{(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u} \ A \ A \ A \ A \ A \ A" by auto + then have fin: "finite {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" + using finite_subset assms(1) finite_cartesian_product by fastforce + have "c ^ 15 * (card A) ^ 5 / 2 ^13 \ card (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_diff (z \ x) c A \ + popular_diff (z \ w) c A \ popular_diff (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + using card_ineq3 hx hy by auto + also have "... \ card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" + using hsub card_mono fin by auto + finally show "c ^ 15 * (card A) ^ 5 / 2 ^13 \ card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ r \ s \ t \ u}" by linarith + qed + moreover have "pairwise (\ s t. disjnt ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)}) s) + ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)}) t)) (differenceset ?C ?B)" + unfolding disjnt_def by (intro pairwiseI) (auto) + moreover have "\ d \ differenceset ?C ?B. ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)}) d) \ A \ A \ A \ A \ A \ A" + by blast + ultimately have "card (differenceset ?C ?B) \ ((card A) ^ 6) / (c^15 * (card A)^5 /2^13)" + using assms(1) hA finite_cartesian_product card_cartesian_product_6[of "A"] + pos card_le_image_div[of "A \ A \ A \ A \ A \ A" "(\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)})" "differenceset ?C ?B" + "(c^15 * (card A)^5 /2^13)"] by auto + also have "... = (card A ^ 6 / card A ^ 5) / (c^15 / 2^13)" + using hA assms(3) field_simps by simp + also have "... = (card A) / (c ^ 15 / 2 ^ 13)" + using cardApow by metis + finally have final: "card (differenceset ?C ?B) \ 2 ^ 13 * (1 / c ^ 15) * real (card A)" + by argo + have "0 < c ^ 4 * real (card A) / 16" and "0 < c ^ 2 * real (card A) / 4" using assms(2) hA by auto + then have "?B \ {}" and "?C \ {}" using cardB cardC by auto + then show ?thesis using hCA hBA cardC cardB final that by auto +qed + + +text\We now show the main theorem, which is a direct application of lemma +@{term obtains_subsets_differenceset_card_bound} and the Ruzsa triangle inequality. +(The main theorem corresponds to Corollary 2.19 in Gowers's notes \cite{Gowersnotes}.) \ + +theorem Balog_Szemeredi_Gowers: fixes A::"'a set" and c::real + assumes afin: "finite A" and "A \ {}" and "c>0" and "additive_energy A = 2 * c" and ass: "A \ G" + obtains A' where "A' \ A" and "card A' \ c^2 * card A / 4" and + "card (differenceset A' A') \ 2^30 * card A / c^34" +proof- + obtain B and A' where bss: "B \ A" and bne: "B \ {}" and bge: "card B \ (c^4) * (card A)/16" + and a2ss: "A' \ A" and a2ge: "card A' \ (c^2) * (card (A))/4" + and hcardle: "card (differenceset A' B) \ 2^13 * card A / c^15" + using assms obtains_subsets_differenceset_card_bound by metis + have Bg0: "(card B :: real) > 0" using bne afin bss infinite_super by fastforce + have "(card B) * card (differenceset A' A') \ + card (differenceset A' B) * card (differenceset A' B)" + using afin a2ss bss infinite_super ass Ruzsa_triangle_ineq1 card_minusset' differenceset_commute + sumset_subset_carrier subset_trans sumset_commute by (smt (verit, best)) + then have "card B * card (differenceset A' A') \ (card (differenceset A' B))^2" + using bss bss power2_eq_square by metis + then have "(card (differenceset A' A')) \ (card (differenceset A' B))^2/card B" + using Bg0 nonzero_mult_div_cancel_left[of "card B" "card(differenceset A' A')"] + divide_right_mono by (smt (verit) of_nat_0 of_nat_mono real_of_nat_div4) + moreover have "(card (differenceset A' B))^2 \ ((2^13) * (1/c^15)*(card A))^2" + using hcardle by simp + ultimately have "(card (differenceset A' A')) \ ((2^13) * (1/c^15)*(card A))^2/(card B)" + using pos_le_divide_eq[OF Bg0] by simp + moreover have "(c^4) * (card A)/16 >0" + using assms card_0_eq by fastforce + moreover have "((2^13) * (1/c^15) * (card A))^2/(card B) = + ((2^13)* (1/c^15)*(card A))^2 * (1/(card B))" by simp + moreover have "((2^13)* (1/c^15) * (card A))^2 * (1/(card B)) \ + ((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)" + using bge calculation(2, 3) frac_le less_eq_real_def zero_le_power2 by metis + ultimately have "(card (differenceset A' A')) \ ((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)" + by linarith + then have "(card (differenceset A' A')) \ (2^30) * (card A)/(c^34)" + using card_0_eq assms by (simp add: power2_eq_square) + then show ?thesis using a2ss a2ge that by blast +qed + +text\The following is an analogous version of the Balog--Szemer\'{e}di--Gowers +Theorem for a sumset instead of a difference set. The proof is similar to that of the original +version, again using @{term obtains_subsets_differenceset_card_bound}, however, instead +of the Ruzsa triangle inequality we will use the alternative triangle inequality for sumsets +@{term triangle_ineq_sumsets}. \ + +theorem Balog_Szemeredi_Gowers_sumset: fixes A::"'a set" and c::real + assumes afin: "finite A" and "A \ {}" and "c>0" and "additive_energy A = 2 * c" and ass: "A \ G" + obtains A' where "A' \ A" and "card A' \ c^2 * card A / 4" and + "card (sumset A' A') \ 2^30 * card A / c^34" + +proof- + obtain B and A' where bss: "B \ A" and bne: "B \ {}" and bge: "card B \ (c^4) * (card A)/16" + and a2ss: "A' \ A" and a2ne: "A' \ {}" and a2ge: "card A' \ (c^2) * (card (A))/4" + and hcardle: "card (differenceset A' B) \ 2^13 * card A / c^15" + using assms obtains_subsets_differenceset_card_bound by metis + have finA': "finite A'" and finB: "finite B" using afin a2ss bss using infinite_super by auto + have bg0: "(card B :: real) > 0" using bne afin bss infinite_super by fastforce + have "card (minusset B) * card (sumset A' A') \ + card (sumset (minusset B) A') * card (sumset (minusset B) A')" + using finA' finB ass a2ss bss triangle_ineq_sumsets + finite_minusset minusset_subset_carrier subset_trans by metis + then have "card B * card (sumset A' A') \ (card (differenceset A' B))^2" + using card_minusset bss ass power2_eq_square + by (metis card_minusset' subset_trans sumset_commute) + then have "(card (sumset A' A')) \ (card (differenceset A' B))^2/card B" + using bg0 nonzero_mult_div_cancel_left[of "card B" "card(sumset A' A')"] + divide_right_mono by (smt (verit) of_nat_0 of_nat_mono real_of_nat_div4) + moreover have "(card (differenceset A' B))^2 \ ((2^13) * (1/c^15) * (card A))^2" + using hcardle by simp + ultimately have "(card (sumset A' A')) \ ((2^13) * (1/c^15) * (card A))^2/(card B)" + using pos_le_divide_eq[OF bg0] by simp + moreover have "(c^4) * (card A)/16 >0" + using assms card_0_eq by fastforce + moreover have "((2^13) * (1/c^15) * (card A))^2/(card B) = + ((2^13)* (1/c^15) * (card A))^2 * (1/(card B))" by simp + moreover have "((2^13) * (1/c^15)*(card A))^2 * (1/(card B)) \ + ((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)" using bge frac_le less_eq_real_def + zero_le_power2 calculation(2, 3) by metis + ultimately have "(card (sumset A' A')) \ ((2^13) * (1/c^15)*(card A))^2/ ((c^4) * (card A)/16)" + by linarith + then have "(card (sumset A' A')) \ (2^30) * (card A)/(c^34)" + using card_0_eq assms by (simp add: power2_eq_square) + then show ?thesis using a2ss a2ne a2ge that by blast +qed + +end +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Supplementary.thy b/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Supplementary.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Supplementary.thy @@ -0,0 +1,606 @@ +section\Supplementary results related to intermediate lemmas used in the proof of the + Balog--Szemer\'{e}di--Gowers Theorem\ + + +(* + Session: Balog_Szemeredi_Gowers + Title: Balog_Szemeredi_Gowers_Supplementary.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Balog_Szemeredi_Gowers_Supplementary + imports + Balog_Szemeredi_Gowers_Main_Proof +begin + +context additive_abelian_group + +begin + +text\Even though it is not applied anywhere in this development, for the sake of completeness we give +the following analogous version of Lemma 2.17 (@{term popular_differences_card}) but for popular sums +instead of popular differences. The proof is identical to that of Lemma 2.17, with the obvious +modifications.\ + +lemma popular_sums_card: + fixes A::"'a set" and c::real + assumes "finite A" and "additive_energy A = 2 * c" and "A \ G" + shows "card (popular_sum_set c A) \ c * card A" + +proof(cases "card A \ 0") + assume hA: "card A \ 0" + have hc: "c \ 0" using assms additive_energy_def of_nat_0_le_iff + by (smt (verit, best) assms(3) divide_nonneg_nonneg of_nat_0_le_iff) + have "(2 * c) * (card A)^3 = (\d \ (sumset A A). (f_sum d A)^2)" + using assms f_sum_card_quadruple_set_additive_energy by auto + also have "...= ((\d \ (popular_sum_set c A). (f_sum d A)^2)) + +((\ d \ ((sumset A A) - (popular_sum_set c A)). (f_sum d A)^2))" + using popular_sum_set_def assms finite_sumset by (metis (no_types, lifting) + add.commute mem_Collect_eq subsetI sum.subset_diff) + also have "... \ ((card (popular_sum_set c A)) * (card A)^2) + + c * card A * ((\d \ (sumset A A - (popular_sum_set c A)) . (f_sum d A)))" + proof- + have "\ d \ ((sumset A A) - (popular_sum_set c A)) . (f_sum d A)^2 \ + (c * (card A)) * (f_sum d A)" + proof + fix d assume hd1: "d \ sumset A A - popular_sum_set c A" + have hnonneg: "f_sum d A \ 0" by auto + have "\ popular_sum d c A" using hd1 popular_sum_set_def by blast + from this have "f_sum d A \ c * card A" using popular_sum_def by auto + thus "real ((f_sum d A)\<^sup>2) \ c * real (card A) * real (f_sum d A)" + using power2_eq_square hnonneg mult_right_mono of_nat_0 of_nat_le_iff of_nat_mult by metis + qed + moreover have "\ d \ (sumset A A) . f_sum d A \ (card A)^2" + using f_sum_def finite_sumset assms + by (metis f_sum_le_card le_antisym nat_le_linear power2_nat_le_imp_le) + ultimately have "((\d \ ((sumset A A) - popular_sum_set c A) . (f_sum d A)^2)) \ + ((\d \ ((sumset A A) - popular_sum_set c A). (c * card A) * (f_sum d A)))" + using assms finite_sumset sum_distrib_left sum_mono by fastforce + then have "((\d \ ((sumset A A) - popular_sum_set c A) . (f_sum d A)^2)) \ + (c * card A) * ((\d \ ((sumset A A) - popular_sum_set c A) . (f_sum d A)))" + by (metis (no_types) of_nat_sum sum_distrib_left) + moreover have "(\d \ popular_sum_set c A. (f_sum d A)^2) \ + (\d \ popular_sum_set c A. (card A)^2)" using f_sum_le_card assms sum_mono assms popular_sum_set_def + by (metis (no_types, lifting) power2_nat_le_eq_le) + moreover then have "(\d \ popular_sum_set c A . (f_sum d A)^2) \ + (card (popular_sum_set c A)) * (card A)^2" + using sum_distrib_right by simp + ultimately show ?thesis by linarith + qed + also have "... \ ((card (popular_sum_set c A)) * (card A)^2) + (c * card A) * (card A)^2" + proof- + have "(\d \ (sumset A A - popular_sum_set c A) . (f_sum d A)) \ + (\d \ sumset A A . (f_sum d A))" using DiffD1 subsetI assms sum_mono2 + finite_sumset zero_le by metis + then have "(c * card A) * ((\d \ (sumset A A - popular_sum_set c A). (f_sum d A))) + \ (c * card A) * (card A)^2" + using f_sum_card hc le0 mult_left_mono of_nat_0 of_nat_mono zero_le_mult_iff assms by metis + then show ?thesis by linarith + qed + finally have "(2 * c) * (card A)^3 \ ((card (popular_sum_set c A)) * (card A)^2) + + (c * card A) * (card A)^2" by linarith + then have "(card (popular_sum_set c A)) \ + ((2 * c)* (card A)^3 - (c * card A) * (card A)^2)/((card A)^2)" + using hA by (simp add: field_simps) + moreover have "((2 * c)* (card A)^3 - (c * card A) * (card A)^2)/((card A)^2) = 2 * c * card A - c * card A" + using hA by (simp add: power2_eq_square power3_eq_cube) + ultimately show ?thesis by linarith +next + assume "\ card A \ 0" + thus ?thesis by auto +qed + + +text\The following is an analogous version of lemma @{term obtains_subsets_differenceset_card_bound} +(2.18 in Gowers's notes \cite{Gowersnotes}) but for a sumset instead of a difference set. It is not used anywhere in this +development but we provide it for the sake of completeness. The proof is identical to that of +lemma @{term obtains_subsets_differenceset_card_bound} with @{term f_diff} changed to @{term f_sum}, +@{term popular_diff} changed to @{term popular_sum}, \oplus interchanged with \ominus, and instead of +lemma @{term popular_differences_card} we apply its analogous version for popular sums, that is +lemma @{term popular_sums_card}. \ + +lemma obtains_subsets_sumset_card_bound: fixes A::"'a set" and c::real + assumes "finite A" and "c>0" and "A \ {}" and "A \ G" and "additive_energy A = 2 * c" + obtains B and A' where "B \ A" and "B \ {}" and "card B \ c^4 * card A / 16" + and "A' \ A" and "A' \ {}" and "card A' \ c^2 * card A / 4" + and "card (sumset A' B) \ 2^13 * card A / c^15" + +proof- + let ?X = "A \ {0:: nat}" + let ?Y = "A \ {1:: nat}" + let ?E = "mk_edge ` {(x, y)| x y. x \ ?X \ y \ ?Y \ (popular_sum (fst y \ fst x) c A)}" + interpret H: fin_bipartite_graph "?X \ ?Y" ?E ?X ?Y + proof (unfold_locales, auto simp add: partition_on_def assms(3) assms(1) disjoint_def) + show "{} = A \ {0} \ False" using assms(3) by auto + next + show "{} = A \ {Suc 0} \ False" using assms(3) by auto + next + show "A \ {0} = A \ {Suc 0} \ False" using assms(3) by fastforce + next + fix x y assume "x \ A" and "y \ A" and "popular_sum (y \ x) c A" + thus "{(x, 0), (y, Suc 0)} \ all_bi_edges (A \ {0}) (A \ {Suc 0})" + using all_bi_edges_def[of "A \ {0}" "A \ {Suc 0}"] + by (simp add: in_mk_edge_img) + qed + have edges1: "\ a \ A. \ b \ A. ({(a, 0), (b, 1)} \ ?E \ popular_sum (b \ a) c A)" + by (auto simp add: in_mk_uedge_img_iff) + have hXA: "card A = card ?X" by (simp add: card_cartesian_product) + have hYA: "card A = card ?Y" by (simp add: card_cartesian_product) + have hA: "card A \ 0" using assms card_0_eq by blast + have edge_density: "H.edge_density ?X ?Y \ c^2" + proof- + define f:: "'a \ ('a \ nat) edge set" where "f \ (\ x. {{(a, 0), (b, 1)} | a b. + a \ A \ b \ A \ b \ a = x})" + have f_disj: "pairwise (\ s t. disjnt (f s) (f t)) (popular_sum_set c A)" + proof (intro pairwiseI) + fix x y assume hx: "x \ popular_sum_set c A" and hy: "y \ popular_sum_set c A" + and hxy: "x \ y" + show "disjnt (f x) (f y)" + proof- + have "\a. \ (a \ f x \ a \ f y)" + proof (intro allI notI) + fix a assume "a \ f x \ a \ f y" + then obtain z w where hazw: "a = {(z, 0), (w, 1)}" and hx: "{(z,0), (w, 1)} \ f x" + and hy: "{(z, 0), (w, 1)} \ f y" using f_def by blast + have "w \ z = x" using f_def hx by (simp add: doubleton_eq_iff) + moreover have "w \ z = y" using f_def hy by (simp add: doubleton_eq_iff) + ultimately show "False" using hxy by auto + qed + thus ?thesis using disjnt_iff by auto + qed + qed + have f_sub_edges: "\ d \ popular_sum_set c A. (f d) \ ?E" + using popular_sum_set_def f_def edges1 by auto + have f_union_sub: "(\ d \ popular_sum_set c A. (f d)) \ ?E" using popular_sum_set_def + f_def edges1 by auto + have f_disj2: "disjoint (f ` (popular_sum_set c A))" using f_disj + pairwise_image[of "disjnt" "f" "popular_sum_set c A"] by (simp add: pairwise_def) + have f_finite: "\B. B \ f ` popular_sum_set c A \ finite B" + using finite_subset f_sub_edges H.fin_edges by auto + have card_eq_f_diff: "\ d \ popular_sum_set c A. card (f d) = f_sum d A" + proof + fix d assume "d \ popular_sum_set c A" + define g:: "('a \ 'a) \ ('a \ nat) edge" where "g = (\ (a, b). {(b, 0), (a, 1)})" + have g_inj: "inj_on g {(a, b) | a b. a \ A \ b \ A \ a \ b = d}" + 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 hg: "g x = g y" + then obtain a1 a2 b1 b2 where hx: "x = (a1, a2)" and hy: "y = (b1, b2)" by blast + thus "x = y" using g_def hg hx hy by (simp add: doubleton_eq_iff) + qed + have g_image: "g ` {(a, b) |a b. a \ A \ b \ A \ a \ b = d} = f d" using f_def g_def by auto + show "card (f d) = f_sum d A" using card_image g_inj g_image f_sum_def by fastforce + qed + have "c ^ 2 * (card A) ^ 2 = c * (card A) * (c * (card A))" using power2_eq_square + by (metis of_nat_power power_mult_distrib) + also have "... \ (card (popular_sum_set c A)) * (c * (card A))" + using assms popular_sums_card hA by force + also have "... \ (\ d \ popular_sum_set c A. f_sum d A)" using sum_mono popular_sum_set_def + popular_sum_def by (smt (verit, ccfv_SIG) mem_Collect_eq of_nat_sum of_real_of_nat_eq + sum_constant) + also have "... = (\ d \ popular_sum_set c A. card (f d))" + using card_eq_f_diff sum.cong by auto + also have "... = sum card (f ` (popular_sum_set c A))" + using f_disj sum_card_image[of "popular_sum_set c A" "f"] popular_sum_set_def + finite_sumset assms(1) finite_subset by auto + also have "... = card (\ d \ popular_sum_set c A. (f d))" + using card_Union_disjoint[of "f ` (popular_sum_set c A)"] f_disj2 f_finite by auto + also have "... \ card ?E" using card_mono f_union_sub H.fin_edges by auto + finally have "c ^ 2 * (card A) ^ 2 \ card ?E" by linarith + then have "c ^ 2 * (card A) ^ 2 \ card (H.all_edges_between ?X ?Y)" + using H.card_edges_between_set by auto + moreover have "H.edge_density ?X ?Y = card (H.all_edges_between ?X ?Y) / (card A) ^ 2" + using H.edge_density_def power2_eq_square hXA hYA + by (smt (verit, best)) + ultimately have "(c ^ 2 * (card A) ^ 2) / (card A) ^ 2 \ H.edge_density ?X ?Y" using hA + divide_le_cancel by (smt (verit, del_insts) H.edge_density_ge0 \c\<^sup>2 * real ((card A)\<^sup>2) = + c * real (card A) * (c * real (card A))\ divide_divide_eq_right zero_le_divide_iff) + thus ?thesis using hA assms(2) by auto + qed + obtain X' and Y' where X'sub: "X' \ ?X" and Y'sub: "Y' \ ?Y" and + hX': "card X' \ (H.edge_density ?X ?Y)^2 * (card ?X)/16" and + hY': "card Y' \ (H.edge_density ?X ?Y) * (card ?Y)/4" and + hwalks: "\ x \ X'. \ y \ Y'. card ({p. H.connecting_walk x y p \ H.walk_length p = 3}) \ + (H.edge_density ?X ?Y)^6 * card ?X * card ?Y / 2^13" + using H.walks_of_length_3_subsets_bipartite \c>0\ by auto + have "((c^2)^2) * (card A) \ (H.edge_density ?X ?Y)^2 * (card A)" + using edge_density assms(2) hA power_mono zero_le_power2 mult_le_cancel_right + by (smt (verit) of_nat_less_of_nat_power_cancel_iff of_nat_zero_less_power_iff + power2_less_eq_zero_iff power_0_left) + then have cardX': "card X' \ (c^4) * (card A)/16" using hX' divide_le_cancel hXA by fastforce + have "c^2 * (card A) / 4 \ (H.edge_density ?X ?Y) * card ?Y / 4" using hYA hA edge_density + mult_le_cancel_right by simp + then have cardY': "card Y' \ c^2 * (card A)/4" using hY' by linarith + have "(H.edge_density ?X ?Y)^6 * (card ?X * card ?Y)/ 2^13 \ (c^2)^6 * ((card A)^2) / 2^13" using + hXA hYA power2_eq_square edge_density divide_le_cancel mult_le_cancel_right hA + by (smt (verit, ccfv_SIG) of_nat_power power2_less_0 power_less_imp_less_base zero_le_power) + then have card_walks: "\ x \ X'. \ y \ Y'. + card ({p. H.connecting_walk x y p \ H.walk_length p = 3}) \ (c^12) * ((card A)^2) / 2^13" + using hwalks by fastforce + (* ?X and ?Y are subsets of the vertex set, now project down to G, giving subsets ?B and ?C of A, + respectively*) + let ?B = "(\ (a, b). a) ` X'" + let ?C = "(\ (a, b). a) ` Y'" + have hBA: "?B \ A" and hCA: "?C \ A" using Y'sub X'sub by auto + have inj_on_X': "inj_on (\ (a, b). a) X'" using X'sub by (intro inj_onI) (auto) + have inj_on_Y': "inj_on (\ (a, b). a) Y'" using Y'sub by (intro inj_onI) (auto) + have hBX': "card ?B = card X'" and hCY': "card ?C = card Y'" + using card_image inj_on_X' inj_on_Y' by auto + then have cardB: "card ?B \ (c^4) * (card A)/16" and cardC: "card ?C \ c^2 * (card A)/4" + using cardX' cardY' by auto + have card_ineq1: "\ x y. x \ ?B \ y \ ?C \ card ({(z, w) | z w. z \ A \ w \ A \ + popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A}) \ + (c^12) * ((card A)^2) / 2^13" + proof- + fix x y assume hx: "x \ ?B" and hy: "y \ ?C" + have hxA: "x \ A" and hyA: "y \ A" using hx hy hBA hCA by auto + define f:: "'a \ 'a \ ('a \ nat) list" + where "f \ (\ (z, w). [(x, 0), (z, 1), (w, 0), (y, 1)])" + have f_inj_on: "inj_on f {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" using f_def by (intro inj_onI) (auto) + have f_image: "f ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} = + {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + proof + show "f ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} \ + {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + proof + fix p assume hp: "p \ f ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" + then obtain z w where hz: "z \ A" and hw: "w \ A" and hzx: "popular_sum (z \ x) c A" and + hzw: "popular_sum (z \ w) c A" and hyw: "popular_sum (y \ w) c A" and + hp: "p = [(x, 0), (z, 1), (w, 0), (y, 1)]" using f_def hp by fast + then have hcon: "H.connecting_walk (x, 0) (y, 1) p" + unfolding H.connecting_walk_def H.is_walk_def + using hxA hyA H.vert_adj_def H.vert_adj_sym edges1 by simp + thus "p \ {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + using hp H.walk_length_conv by auto + qed + next + show "{p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3} \ f ` {(z, w) |z w. + z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A}" + proof(intro subsetI) + fix p assume hp: "p \ {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + then have len: "length p = 4" using H.walk_length_conv by auto + have hpsub: "set p \ A \ {0} \ A \ {1}" using hp H.connecting_walk_def H.is_walk_def + by auto + then have fst_sub: "fst ` set p \ A" by auto + have h1A: "fst (p!1) \ A" and h2A: "fst (p!2) \ A" using fst_sub len by auto + have hpnum: "p = [p!0, p!1, p!2, p!3]" + proof (auto simp add: list_eq_iff_nth_eq len) + fix k assume "k < (4:: nat)" + then have "k = 0 \ k = 1 \ k = 2 \ k = 3" by auto + thus "p ! k = [p ! 0, p ! Suc 0, p ! 2, p ! 3] ! k" by fastforce + qed + then have "set (H.walk_edges p) = {{p!0, p!1} , {p!1, p!2}, {p!2, p!3}}" using + comp_sgraph.walk_edges.simps(2) comp_sgraph.walk_edges.simps(3) + by (metis empty_set list.simps(15)) + then have h1: "{p!0, p!1} \ ?E" and h2: "{p!2, p!1} \ ?E" and h3: "{p!2, p!3} \ ?E" + using hp H.connecting_walk_def H.is_walk_def len by auto + have hxp: "p!0 = (x, 0)" using hp len hd_conv_nth H.connecting_walk_def H.is_walk_def + by fastforce + have hyp: "p!3 = (y, 1)" using hp len last_conv_nth H.connecting_walk_def H.is_walk_def + by fastforce + have h1p: "p!1 = (fst (p!1), 1)" + proof- + have "p!1 \ A \ {0} \ A \ {1}" using hpnum hpsub + by (metis (no_types, lifting) insertCI list.simps(15) subsetD) + then have hsplit: "snd (p!1) = 0 \ snd (p!1) = 1" by auto + then have "snd (p!1) = 1" + proof(cases "snd (p!1) = 0") + case True + then have 1: "{(x, 0), (fst (p!1), 0)} \ ?E" using h1 hxp doubleton_eq_iff + by (smt (verit, del_insts) surjective_pairing) + have hY: "(fst (p!1), 0) \ ?Y" and hX: "(x, 0) \ ?X" using hxA by auto + then have 2: "{(x, 0), (fst (p!1), 0)} \ ?E" using H.X_vert_adj_Y H.vert_adj_def by meson + then show ?thesis using 1 2 by blast + next + case False + then show ?thesis using hsplit by auto + qed + thus "(p ! 1) = (fst (p ! 1), 1)" + by (metis (full_types) split_pairs) + qed + have h2p: "p!2 = (fst (p!2), 0)" + proof- + have "p!2 \ A \ {0} \ A \ {1}" using hpnum hpsub + by (metis (no_types, lifting) insertCI list.simps(15) subsetD) + then have hsplit: "snd (p!2) = 0 \ snd (p!2) = 1" by auto + then have "snd (p!2) = 0" + proof(cases "snd (p!2) = 1") + case True + then have 1: "{(fst (p!2), 1), (y, 1)} \ ?E" using h3 hyp doubleton_eq_iff + by (smt (verit, del_insts) surjective_pairing) + have hY: "(y, 1) \ ?X" and hX: "(fst (p!2), 1) \ ?Y" using hyA h2A by auto + then have 2: "{(fst (p!2), 1), (y, 1)} \ ?E" using H.Y_vert_adj_X H.vert_adj_def + by meson + then show ?thesis using 1 2 by blast + next + case False + then show ?thesis using hsplit by auto + qed + thus "(p ! 2) = (fst (p ! 2), 0)" + by (metis (full_types) split_pairs) + qed + have hpop1: "popular_sum ((fst (p!1)) \ x) c A" using edges1 h1 hxp h1p hxA h1A + by (smt (z3)) + have hpop2: "popular_sum((fst (p!1)) \ (fst (p!2))) c A" using edges1 h2 h1p h2p h1A h2A + by (smt (z3)) + have hpop3: "popular_sum (y \ (fst (p!2))) c A" using edges1 h3 h2p hyp hyA h2A + by (smt (z3)) + thus "p \ f ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" using f_def hpnum hxp h1p h2p hyp + h1A h2A hpop1 hpop2 hpop3 by force + qed + qed + have hx1: "(x, 0) \ X'" and hy2: "(y, 1) \ Y'" using hx X'sub hy Y'sub by auto + have "card {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} = + card {p. H.connecting_walk (x, 0) (y, 1) p \ H.walk_length p = 3}" + using card_image f_inj_on f_image by fastforce + thus "card {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} \ c ^ 12 * ((card A)^2) / 2 ^ 13" + using hx1 hy2 card_walks by auto + qed + have "\ x x2 y y2 z w . (x, x2) \ X'\ (y, y2) \ Y'\ z \ A \ w \ A + \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A \ + c ^ 3 * real (card A) ^ 3 \ + (card {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + proof - + fix x x2 y y2 z w assume "(x, x2) \ X'" and "(y, y2) \ Y'" and "z \ A" and "w \ A" and + 1: "popular_sum (z \ x) c A" and 2: "popular_sum (z \ w) c A" and + 3: "popular_sum (y \ w) c A" + define f:: "'a \ 'a \ 'a \ 'a \ 'a \ 'a \ ('a \ 'a) \ ('a \ 'a) \ ('a \ 'a)" where + "f \ (\ (p, q, r, s, t, u). ((p, q), (r, s), (t, u)))" + (* Types ('a \ 'a \ 'a \ 'a \ 'a \ 'a) and ('a \ 'a) \ ('a \ 'a) \ ('a \ 'a) are not + definitionally equal, so we need to define a bijection between them *) + have f_inj: "inj_on f {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" using f_def + by (intro inj_onI) (auto) + have f_image: "f ` {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} = + {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} \ + {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" using f_def by force + (* warning: this proof takes a while *) + have 4: "card {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} = + card ({(p, q). p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q). p \ A \ q \ A \ p \ q = z \ w} \ {(p, q). p \ A \ q \ A \ p \ q = y \ w})" + using card_image f_inj f_image by fastforce + moreover have 5: "card ({(p, q). p \ A \ q \ A \ p \ q = z \ x} \ + {(p, q). p \ A \ q \ A \ p \ q = z \ w} \ {(p, q). p \ A \ q \ A \ p \ q = y \ w}) = + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" + using card_cartesian_product3 by auto + have "c * card A \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x}" + using 1 popular_sum_def f_sum_def by auto + then have "(c * card A) * (c * card A) \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w}" + using 2 popular_sum_def f_sum_def mult_mono assms(2) mult_nonneg_nonneg + of_nat_0_le_iff of_nat_mult by fastforce + then have 6: "(c * card A) * (c * card A) * (c * card A) \ card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ x} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = z \ w} * + card {(p, q) | p q. p \ A \ q \ A \ p \ q = y \ w}" + using 3 popular_sum_def f_sum_def mult_mono assms(2) mult_nonneg_nonneg of_nat_0_le_iff + of_nat_mult by fastforce + have 7: "c ^ 3 * card A ^ 3 = (c * card A) * ((c * card A) * (c * card A))" + by (simp add: power3_eq_cube algebra_simps) + show "c ^ 3 * real (card A) ^ 3 \ + (card {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" using 4 5 6 7 by auto + qed + then have card_ineq2: "\ x y z w. x \ ?B \ y \ ?C \ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ + popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A} \ + card {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} \ c^3 * card A^3" + by auto + have card_ineq3: "\ x y. x \ ?B \ y \ ?C \ card (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ + popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) \ + c ^ 15 * ((card A)^5) / 2 ^ 13" + proof- + fix x y assume hx: "x \ ?B" and hy: "y \ ?C" + have hxG: "x \ G" and hyG: "y \ G" using hx hy hBA hCA assms(4) by auto + let ?f = "(\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + have hpair_disj: "pairwise (\ a b. disjnt (?f a) (?f b)) + {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A}" + proof (intro pairwiseI) + fix a b assume "a \ {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" "b \ {(z, w) |z w. z \ A \ w \ A \ + popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" and + "a \ b" + then obtain a1 a2 b1 b2 where ha: "a = (a1, a2)" and hb: "b = (b1, b2)" and ha1: "a1 \ G" and + ha2: "a2 \ G" and hb1: "b1 \ G" and hb2: "b2 \ G" and hne: "(a1, a2) \ (b1, b2)" + using assms(4) by blast + have "(\x. \ (x \ (?f a) \ x \ (?f b)))" + proof(intro allI notI) + fix d assume "d \ (?f a) \ d \ (?f b)" + then obtain p q r s t u where "d = (p, q, r, s, t, u)" and hpq1: "p \ q = a1 \ x" and + htu1: "t \ u = y \ a2" and hpq2: "p \ q = b1 \ x" and htu2: "t \ u = y \ b2" + using ha hb by auto + then have "y \ a2 = y \ b2" using htu1 htu2 by auto + then have 2: "a2 = b2" using ha2 hb2 hyG by (metis invertible invertible_left_cancel) + have 1: "a1 = b1" using hpq1 hpq2 ha1 hb1 hxG by simp + show "False" using 1 2 hne by auto + qed + thus "disjnt (?f a) (?f b)" using disjnt_iff[of "(?f a)" "(?f b)"] by auto + qed + have hfinite_walks: "\ B. B \ ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A}) \ finite B" + proof- + fix B assume "B \ ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A})" + then have "B \ A \ A \ A \ A \ A \ A" by auto + thus "finite B" using assms(1) + by (auto simp add: finite_subset) + qed + have hdisj: "disjoint ((\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) ` + {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A})" using hpair_disj pairwise_image[of "disjnt" "(\ (z, w). {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + "{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A}"] by (simp add: pairwise_def) + have "{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} \ A \ A" by auto + then have hwalks_finite: "finite {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" using finite_subset assms(1) + by fastforce + have f_ineq: "\ a \ {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. c ^ 3 * (card A) ^ 3 \ + card (?f a)" using card_ineq2 hx hy by auto + have "c ^ 15 * ((card A)^5) / 2 ^ 13 = (c ^ 12 * (card A) ^ 2 / 2 ^ 13) * (c ^ 3 * card A ^ 3)" + by (simp add: algebra_simps) + also have "... \ card {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A} * (c ^ 3 * (card A) ^ 3)" + using card_ineq1[of "x" "y"] hx hy mult_le_cancel_right hA by (smt (verit, best) assms(2) + mult_pos_pos of_nat_0_less_iff of_nat_le_0_iff zero_less_power) + also have "... = (\ a \ {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. (c ^ 3 * (card A) ^ 3))" by auto + also have "... \ (\a\{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. card (?f a))" + using sum_mono f_ineq by (smt (verit, del_insts) of_nat_sum) + also have "... = sum card (?f ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A})" + using sum_card_image[of "{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" "?f"] hpair_disj hwalks_finite by auto + also have "... = card (\ (z, w)\{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ + t \ u = y \ w})" using card_Union_disjoint hdisj hfinite_walks by (metis (no_types, lifting)) + finally show "c ^ 15 * real (card A ^ 5) / 2 ^ 13 \ real (card (\(z, w)\{(z, w) |z w. + z \ A \ w \ A \ popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ + popular_sum (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}))" by simp + qed + have pos: "0 < c ^ 15 * real (card A ^ 5) / 2 ^ 13" using hA \c>0\ by auto + have "(5:: nat) \ 6" by auto + then have "(card A ^ 6 / card A ^ 5) = (card A) ^ (6 - 5)" + using hA power_diff by (metis of_nat_eq_0_iff of_nat_power) + then have cardApow: "(card A ^ 6 / card A ^ 5) = card A" using power_one_right by simp + have hdsub: "\ d \ sumset ?C ?B. \ y \ ?C. \ x \ ?B. + (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" + proof + fix d assume "d \ sumset ?C ?B" + then obtain y x where hy: "y \ ?C" and hx: "x \ ?B" and hxy: "d = y \ x" + using sumset_def minusset_def hBA hCA assms(4) subset_trans + by (smt (verit, best) minusset.simps sumset.cases) + have hxG: "x \ G" and hyG: "y \ G" using hx hy hBA hCA assms(4) by auto + have "(\(z, w)\{(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + d = p \ q \ (r \ s) \ t \ u}" + proof (rule Union_least) + fix X assume "X \ (\(z, w). {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ + t \ u = y \ w}) ` {(z, w) |z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}" + then obtain z w where hX: "X = {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" + and hz: "z \ A" and hw: "w \ A" by auto + have hzG: "z \ G" and hwG: "w \ G" using hz hw assms(4) by auto + have "{(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w} \ + {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + d = p \ q \ (r \ s) \ t \ u}" + proof + fix e assume "e \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}" + then obtain p q r s t u where "p \ q = z \ x" and "r \ s = z \ w" and "t \ u = y \ w" + and hp: "p \ A" and hq: "q \ A" and hr: "r \ A" and hs: "s \ A" and ht: "t \ A" + and hu: "u \ A" and he: "e = (p, q, r, s, t, u)" by blast + then have "p \ q \ (r \ s) \ t \ u = z \ x \ (z \ w) \ y \ w" + by (smt (verit, ccfv_threshold) assms(4) associative composition_closed hwG hxG hyG hzG + inverse_closed subset_eq) + also have "... = y \ x" using hxG hyG hzG hwG + by (smt (verit) associative commutative composition_closed inverse_closed invertible + invertible_right_inverse2) + finally have "d = p \ q \ (r \ s) \ t \ u" using hxy by simp + thus "e \ {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ + u \ A \ d = p \ q \ (r \ s) \ t \ u}" using he hp hq hr hs ht hu by auto + qed + thus "X \ {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" + using hX by auto + qed + thus "\y\(\(a, b). a) ` Y'. \x\(\(a, b). a) ` X'. (\(z, w)\{(z, w) |z w. z \ A \ w \ A \ + popular_sum (z \ x) c A \ popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. + {(p, q, r, s, t, u) |p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ + p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) \ {(p, q, r, s, t, u) |p q r s t u. + p \ A \ q \ A \ r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" + using hx hy by meson + qed + moreover have "\ d \ sumset ?C ?B. card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u} \ c ^ 15 * (card A) ^ 5 / 2 ^13" + proof + fix d assume "d \ sumset ((\(a, b). a) ` Y') ((\(a, b). a) ` X')" + then obtain x y where hy: "y \ ?C" and hx: "x \ ?B" and hsub: + "(\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w}) + \ {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" using hdsub by meson + have "{(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u} \ A \ A \ A \ A \ A \ A" by auto + then have fin: "finite {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" + using finite_subset assms(1) finite_cartesian_product by fastforce + have "c ^ 15 * (card A) ^ 5 / 2 ^13 \ card (\ (z, w) \ {(z, w) | z w. z \ A \ w \ A \ popular_sum (z \ x) c A \ + popular_sum (z \ w) c A \ popular_sum (y \ w) c A}. + {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ r \ A \ s \ A \ + t \ A \ u \ A \ p \ q = z \ x \ r \ s = z \ w \ t \ u = y \ w})" + using card_ineq3 hx hy by auto + also have "... \ card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" + using hsub card_mono fin by auto + finally show "c ^ 15 * (card A) ^ 5 / 2 ^13 \ card {(p, q, r, s, t, u) | p q r s t u. p \ A \ q \ A \ r \ A \ + s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}" by linarith + qed + moreover have "pairwise (\ s t. disjnt ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}) s) + ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u}) t)) (sumset ?C ?B)" + unfolding disjnt_def by (intro pairwiseI) (auto) + moreover have "\ d \ sumset ?C ?B. ((\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ (d = p \ q \ r \ s \ t \ u)}) d) \ A \ A \ A \ A \ A \ A" + by blast + ultimately have "card (sumset ?C ?B) \ ((card A) ^ 6) / (c^15 *(card A)^5 /2^13)" + using assms(1) hA finite_cartesian_product card_cartesian_product_6[of "A"] + pos card_le_image_div[of "A \ A \ A \ A \ A \ A" "(\ d. {(p, q, r, s, t, u)| p q r s t u. p \ A \ q \ A \ + r \ A \ s \ A \ t \ A \ u \ A \ d = p \ q \ (r \ s) \ t \ u})" "sumset ?C ?B" + "(c^15 * (card A)^5 /2^13)"] by auto + also have "... = (card A ^ 6 / card A ^ 5) / (c^15 / 2^13)" + using hA assms(3) field_simps by simp + also have "... = (card A) / (c ^ 15 / 2 ^ 13)" + using cardApow by metis + finally have final: "card (sumset ?C ?B) \ 2 ^ 13 * (1 / c ^ 15) * real (card A)" + by argo + have "0 < c ^ 4 * real (card A) / 16" and "0 < c ^ 2 * real (card A) / 4" using assms(2) hA by auto + then have "?B \ {}" and "?C \ {}" using cardB cardC by auto + then show ?thesis using hCA hBA cardC cardB final that by auto +qed + + +end +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Graph_Theory_Preliminaries.thy b/thys/Balog_Szemeredi_Gowers/Graph_Theory_Preliminaries.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Graph_Theory_Preliminaries.thy @@ -0,0 +1,241 @@ +section\Background material for the graph-theoretic aspects of the main proof\ +text \This section includes a number of lemmas on project specific definitions for graph theory, +building on the general undirected graph theory library \cite{Undirected_Graph_Theory-AFP} \ + +(* + Session: Balog_Szemeredi_Gowers + Title: Graph_Theory_Preliminaries.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Graph_Theory_Preliminaries + imports + Miscellaneous_Lemmas + Undirected_Graph_Theory.Bipartite_Graphs + Undirected_Graph_Theory.Connectivity + Random_Graph_Subgraph_Threshold.Ugraph_Misc +begin + +subsection\On graphs with loops\ + +context ulgraph + +begin + +definition degree_normalized:: "'a \ 'a set \ real" where + "degree_normalized v S \ card (neighbors_ss v S) / (card S)" + +lemma degree_normalized_le_1: "degree_normalized x S \ 1" + +proof(cases "finite S") + assume hA: "finite S" + then have "card (neighbors_ss x S) \ card S" using neighbors_ss_def card_mono hA + by fastforce + then show ?thesis using degree_normalized_def divide_le_eq_1 + by (metis antisym_conv3 of_nat_le_iff of_nat_less_0_iff) +next + case False + then show ?thesis using degree_normalized_def by auto +qed + +end + +subsection\On bipartite graphs \ + + +context bipartite_graph +begin + +(* codegree counts the number of paths between two vertices, including loops *) +definition codegree:: "'a \ 'a \ nat" where + "codegree v u \ card {x \ V . vert_adj v x \ vert_adj u x}" + +lemma codegree_neighbors: "codegree v u = card (neighborhood v \ neighborhood u)" + unfolding codegree_def neighborhood_def + +proof - + have "{x \ V. vert_adj v x \ vert_adj u x} = {va \ V. vert_adj v va} \ {v \ V. vert_adj u v}" + by blast + thus "card {x \ V. vert_adj v x \ vert_adj u x} = card ({va \ V. vert_adj v va} \ {v \ V. vert_adj u v})" + by auto +qed + +lemma codegree_sym: "codegree v u = codegree u v" + by (simp add: Int_commute codegree_neighbors) + +definition codegree_normalized:: "'a \ 'a \ 'a set \ real" where + "codegree_normalized v u S \ codegree v u / card S" + +lemma codegree_normalized_altX: + assumes "x \ X" and "x' \ X" + shows "codegree_normalized x x' Y = card (neighbors_ss x Y \ neighbors_ss x' Y) / card Y" + +proof - + have "((neighbors_ss x Y) \ (neighbors_ss x' Y)) = neighborhood x \ neighborhood x'" + using neighbors_ss_eq_neighborhoodX assms by auto + then show ?thesis unfolding codegree_normalized_def + using codegree_def codegree_neighbors by presburger +qed + +lemma codegree_normalized_altY: + assumes "y \ Y" and "y' \ Y" + shows "codegree_normalized y y' X = card (neighbors_ss y X \ neighbors_ss y' X) / card X" + +proof - + have "neighbors_ss y X \ neighbors_ss y' X = neighborhood y \ neighborhood y'" + using neighbors_ss_eq_neighborhoodY assms by auto + then show ?thesis unfolding codegree_normalized_def + using codegree_def codegree_neighbors by presburger +qed + +lemma codegree_normalized_sym: "codegree_normalized u v S = codegree_normalized v u S" + unfolding codegree_normalized_def using codegree_sym by simp + +definition bad_pair:: " 'a \ 'a \ 'a set \ real \ bool" where + "bad_pair v u S c \ codegree_normalized v u S < c" + +lemma bad_pair_sym: + assumes "bad_pair v u S c" shows "bad_pair u v S c" + using assms bad_pair_def codegree_normalized_def + by (simp add: codegree_normalized_sym) + +definition bad_pair_set:: "'a set \ 'a set \ real \ ('a \ 'a) set" where + "bad_pair_set S T c \ {(u, v) \ S \ S. bad_pair u v T c}" + +lemma bad_pair_set_ss: "bad_pair_set S T c \ S \ S" + by (auto simp add: bad_pair_set_def) + +lemma bad_pair_set_filter_alt: + "bad_pair_set S T c = Set.filter (\ p . bad_pair (fst p) (snd p) T c) (S \ S)" + using bad_pair_set_def by auto + +lemma bad_pair_set_finite: + assumes "finite S" + shows "finite (bad_pair_set S T c)" +proof - + have "finite (S \ S)" using finite_cartesian_product assms by blast + thus ?thesis using bad_pair_set_filter_alt finite_filter by auto +qed + +lemma codegree_is_path_length_two: + "codegree x x' = card {p . connecting_path x x' p \ walk_length p = 2}" + unfolding codegree_def +proof- + define f:: "'a list \ 'a" where "f = (\ p. p!1)" + have f_inj: "inj_on f {p . connecting_path x x' p \ walk_length p = 2}" + unfolding f_def + proof (intro inj_onI, simp del: One_nat_def) + fix a b assume ha: "connecting_path x x' a \ walk_length a = 2" and + hb: "connecting_path x x' b \ walk_length b = 2" and 1: "a!1 = b!1" + then have len: "length a = 3" "length b = 3" using walk_length_conv by auto + show "a = b" using list2_middle_singleton 1 len list_middle_eq ha hb connecting_path_def len by metis + qed + have f_image: "f ` {p . connecting_path x x' p \ walk_length p = 2} = + {xa \ V. vert_adj x xa \ vert_adj x' xa}" + proof(intro subset_antisym) + show "f ` {p. connecting_path x x' p \ walk_length p = 2} + \ {xa \ V. vert_adj x xa \ vert_adj x' xa}" + proof (intro subsetI) + fix a assume "a \ f ` {p. connecting_path x x' p \ walk_length p = 2}" + then obtain p where ha: "p!1 = a" and hp: "connecting_path x x' p" and hpl: "length p = 3" + using f_def walk_length_conv by auto + have "p ! 0 = x" using hd_conv_nth[of p] hpl hp connecting_path_def by fastforce + then have va1: "vert_adj x a" using is_walk_index[of 0 p] hp connecting_path_def is_gen_path_def + vert_adj_def ha hpl by auto + have "p ! 2 = x'" using last_conv_nth[of p] hpl hp connecting_path_def by fastforce + then have "vert_adj a x'" using is_walk_index[of 1 p] hp connecting_path_def is_gen_path_def + vert_adj_def ha hpl by (metis One_nat_def le0 lessI numeral_3_eq_3 one_add_one) + then show "a \ {a \ V. vert_adj x a \ vert_adj x' a}" + using va1 vert_adj_sym by (simp add: vert_adj_imp_inV) + qed + show "{xa \ V. vert_adj x xa \ vert_adj x' xa} + \ f ` {p. connecting_path x x' p \ walk_length p = 2}" + proof (intro subsetI) + fix a assume ha: "a \ {xa \ V. vert_adj x xa \ vert_adj x' xa}" + then have "a \ V" and "x \ V" and "x' \ V" and "vert_adj x a" and "vert_adj x' a" + using vert_adj_imp_inV by auto + then have "is_gen_path [x, a, x']" + using is_walk_def vert_adj_def vert_adj_sym ha singleton_not_edge is_gen_path_def by auto (* Slow *) + then have "connecting_path x x' [x, a, x']" + unfolding connecting_path_def vert_adj_def hd_conv_nth last_conv_nth by simp + moreover have "walk_length [x, a, x'] = 2" using walk_length_conv by simp + ultimately show "a \ f ` {p. connecting_path x x' p \ walk_length p = 2}" using f_def by force + qed + qed + then show "card {xa \ V. vert_adj x xa \ vert_adj x' xa} = + card {p. connecting_path x x' p \ walk_length p = 2}" + using f_inj card_image by fastforce +qed + +lemma codegree_bipartite_eq: + "\ x \ X. \ x' \ X. codegree x x' = card {y \ Y. vert_adj x y \ vert_adj x' y}" + unfolding codegree_def using vert_adj_imp_inV X_vert_adj_Y + by (metis (no_types, lifting) Collect_cong) + +lemma (in fin_bipartite_graph) bipartite_deg_square_eq: + "\ y \ Y. (\ x' \ X. \ x \ X. indicator {z. vert_adj x z \ vert_adj x' z} y) = (degree y)^2" +proof + have hX: "finite X" by (simp add: partitions_finite(1)) + fix y assume hy: "y \ Y" + have 1: "\ x' \ X. \ x \ X. indicator {z. vert_adj x z \ vert_adj x' z} y = + indicator ({z. vert_adj x' z} \ {z. vert_adj x z}) y" + by (metis (mono_tags, lifting) Int_Collect indicator_simps(1) indicator_simps(2) mem_Collect_eq) + have 2: "\ x' \ X. \ x \ X. (indicator ({z. vert_adj x' z} \ {z. vert_adj x z}) y:: nat) = + indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y" using indicator_inter_arith + by auto + have "(\ x' \ X. \ x \ X. (indicator {z. vert_adj x z \ vert_adj x' z} y:: nat)) = + (\ x' \ X. \ x \ X. indicator ({z. vert_adj x' z} \ {z. vert_adj x z}) y)" + using 1 sum.cong by (metis (no_types, lifting)) + also have "... = (\ x' \ X. \ x \ X. indicator {z. vert_adj x' z} y * + indicator {z. vert_adj x z} y)" using 2 sum.cong by auto + also have "... = sum (\ x. indicator {z. vert_adj x z} y) X * sum (\ x. indicator {z. vert_adj x z} y) X" + using sum_product[of "(\ x. (indicator {z. vert_adj x z} y:: nat))" "X" + "(\ x. indicator {z. vert_adj x z} y)" "X"] by auto + finally have 3: "(\ x' \ X. \ x \ X. (indicator {z. vert_adj x z \ vert_adj x' z} y:: nat)) = + (sum (\ x. indicator {z. vert_adj x z} y) X) ^ 2" using power2_eq_square + by (metis (no_types, lifting)) + have "\ x \ X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x" + by (simp add: indicator_def) + from this have "(sum (\ x. indicator {z. vert_adj x z} y) X) = sum (\ x. indicator {x. vert_adj x y} x) X" + using sum.cong by fastforce + also have "... = card ({x \ X. vert_adj x y})" using sum_indicator_eq_card hX + by (metis Collect_conj_eq Collect_mem_eq) + finally show "(\x'\X. \x\X. indicator {z. vert_adj x z \ vert_adj x' z} y) = (degree y)^2" + using 3 hy degree_neighbors_ssY neighbors_ss_def vert_adj_sym by presburger +qed + +lemma (in fin_bipartite_graph) codegree_degree: + "(\ x' \ X. \ x \ X. (codegree x x')) = (\ y \ Y. (degree y)^2)" + +proof- + have hX: "finite X" and hY: "finite Y" + by (simp_all add: partitions_finite) + have "\ x' \ X. \ x \ X. {z \ V. vert_adj x z \ vert_adj x' z} = Y \ {z. vert_adj x z \ vert_adj x' z}" + using XY_union X_vert_adj_Y by fastforce + from this have "(\ x' \ X. \ x \ X. (codegree x x')) = (\ x' \ X. \ x \ X. card (Y \ {z. vert_adj x z \ vert_adj x' z}))" + using codegree_def sum.cong by auto + also have "... = (\ x' \ X. \ x \ X. \ y \ Y. indicator {z. vert_adj x z \ vert_adj x' z} y)" + using sum_indicator_eq_card hY by fastforce + also have "... = (\ x' \ X. \ y \ Y. (\ x \ X. indicator {z. vert_adj x z \ vert_adj x' z} y))" + using sum.swap by (metis (no_types)) + also have "... = (\ y \ Y. \ x' \ X. (\ x \ X. indicator {z. vert_adj x z \ vert_adj x' z} y))" + using sum.swap by fastforce + also have "... = (\ y \ Y. (degree y)^2)" using bipartite_deg_square_eq sum.cong by force + finally show ?thesis by simp +qed + +lemma (in fin_bipartite_graph) sum_degree_normalized_X_density: + "(\ x \ X. degree_normalized x Y) / card X = edge_density X Y" + by (smt (z3) card_all_edges_betw_neighbor card_edges_between_set degree_normalized_def + divide_divide_eq_left' density_simp of_nat_mult of_nat_sum partitions_finite(1) + partitions_finite(2) sum.cong sum_left_div_distrib) + +lemma (in fin_bipartite_graph) sum_degree_normalized_Y_density: + "(\ y \ Y. degree_normalized y X) / card Y = edge_density X Y" + using bipartite_sym fin_bipartite_graph.sum_degree_normalized_X_density fin_bipartite_graph_def + fin_graph_system_axioms edge_density_commute by fastforce + +end +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Miscellaneous_Lemmas.thy b/thys/Balog_Szemeredi_Gowers/Miscellaneous_Lemmas.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Miscellaneous_Lemmas.thy @@ -0,0 +1,114 @@ +section\Miscellaneous technical lemmas\ + +(* + Title: Miscellaneous_Lemmas.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Miscellaneous_Lemmas + imports + "HOL-Library.Indicator_Function" + "HOL-Analysis.Convex" +begin + +lemma set_pairs_filter_subset: "A \ B \ {p . p \ A \ A \ P p} \ {p. p \ B \ B \ P p}" + by (intro subsetI) blast + +lemma card_set_ss_indicator: + assumes "A \ B" + assumes "finite B" + shows "card A = (\ p \ B. indicator A p)" +proof - + obtain C where ceq: "C = B - A" by blast + then have beq: "B = A \ C" using assms by blast + have bint: "A \ C = {}" using ceq by blast + have finite: "finite A" using assms finite_subset by auto + have zero: "\ p. p \ C \ indicator (A) p = 0" + by (simp add: ceq) + then have "card A = (\ p \ A . indicator (A) p)" + by simp + also have "... = (\ p \ A . indicator A p) + (\ p \ C . indicator A p)" + using zero by (metis add_cancel_left_right sum.neutral) + finally show "card A = (\ p \ B. indicator A p)" using beq bint assms + by (metis add.commute ceq sum.subset_diff) +qed + +lemma card_cartesian_prod_square: "finite X \ card (X \ X) = (card X)^2" + using card_cartesian_product by (simp add: power2_eq_square) + +lemma (in ordered_ab_group_add) diff_strict1_mono: + assumes "a > a'" "b \ b'" + shows "a - b > a' - b'" + using diff_strict_mono assms + by (metis local.diff_strict_right_mono local.dual_order.not_eq_order_implies_strict) + +lemma card_cartesian_product_6: "card (A \ A \ A \ A \ A \ A) = (card A) ^ 6" +proof- + have "card (A \ A \ A \ A \ A \ A) = + card A * card A * card A * card A * card A * card A" + using card_cartesian_product mult.commute by metis + then show ?thesis by algebra +qed + +lemma card_cartesian_product3: "card (X \ Y \ Z) = card X * card Y * card Z" + using card_cartesian_product by (metis mult.commute mult.left_commute) + + +lemma card_le_image_div: + fixes A:: "'a set" and B:: "'b set" and f:: "'a \ 'b set" and r:: real + assumes "finite B" and "pairwise (\ s t. disjnt (f s) (f t)) A" and "\ d \ A. (card (f d)) \ r" + and "\ d \ A. f d \ B" and "r > 0" + shows "card A \ card B / r" + +proof (cases "finite A") + assume hA: "finite A" + have hpair_disj: "pairwise disjnt (f ` A)" using assms by (metis pairwiseD pairwise_imageI) + have "r * card A = (\ d \ A. r)" by simp + also have "... \ (\ d \ A. card (f d))" using assms sum_mono by fastforce + also have "... = sum card (f ` A)" using assms hA by (simp add: sum_card_image) + also have "... = card (\ d \ A. f d)" using assms hA hpair_disj + by (metis Sup_upper card_Union_disjoint finite_UN_I rev_finite_subset) + also have "... \ card B" using assms card_mono + by (metis UN_subset_iff of_nat_le_iff) + finally have "r * card A \ card B" by linarith + thus ?thesis using divide_le_eq assms by (simp add: mult_imp_le_div_pos mult_of_nat_commute) +next + assume "\ finite A" + thus ?thesis using assms by auto +qed + +lemma list_middle_eq: + "length xs = length ys \ hd xs = hd ys \ last xs = last ys + \ butlast (tl xs) = butlast (tl ys) \ xs = ys" + apply (induct xs ys rule: list_induct2, simp) + by (metis append_butlast_last_id butlast.simps(1) butlast.simps(2) butlast_tl hd_Cons_tl + impossible_Cons le_refl list.sel(3) neq_Nil_conv) + +lemma list2_middle_singleton: + assumes "length xs = 3" + shows "butlast (tl xs) = [xs ! 1]" +proof (simp add: list_eq_iff_nth_eq assms) + have l: "length (butlast (tl xs)) = 1" using length_butlast length_tl assms by simp + then have " butlast (tl xs) ! 0 = (tl xs) ! 0" using nth_butlast[of 0 "tl xs"] by simp + then show "butlast (tl xs) ! 0 = xs ! Suc 0" using nth_tl[of 0 xs] l by simp +qed + + +lemma le_powr_half_mult: + fixes x y z:: real + assumes "x ^ 2 \ y * z" and "0 \ y" and "0 \ z" + shows "x \ y powr(1/2) * z powr (1/2)" + using assms power2_eq_square + by (metis dual_order.trans linorder_linear powr_ge_pzero powr_half_sqrt powr_mult real_le_rsqrt + real_sqrt_le_0_iff) + +lemma Cauchy_Schwarz_ineq_sum2: + fixes f g:: "'a \ real" and A:: "'a set" + shows "(\ d \ A. f d * g d) \ + (\ d \ A. (f d)^2) powr (1/2) * (\ d \ A. (g d)^2) powr (1/2)" + using Convex.Cauchy_Schwarz_ineq_sum[of "f" "g" "A"] le_powr_half_mult sum_nonneg zero_le_power2 + by (metis (mono_tags, lifting)) + +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/Prob_Space_Lemmas.thy b/thys/Balog_Szemeredi_Gowers/Prob_Space_Lemmas.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Prob_Space_Lemmas.thy @@ -0,0 +1,135 @@ +section\Auxiliary probability space results\ + +(* + Session : Balog_Szemeredi_Gowers + Title: Prob_Space_Lemmas.thy + Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds + Affiliation: University of Cambridge + Date: August 2022. +*) + +theory Prob_Space_Lemmas + imports + Random_Graph_Subgraph_Threshold.Prob_Lemmas +begin + +context prob_space + +begin + +lemma expectation_uniform_count: + assumes "M = uniform_count_measure X" and "finite X" + shows "expectation f = (\ x \ X. f x) / card X" + +proof- + have "expectation f = (\ x \ X. (1 / (card X)) * f x)" + using assms uniform_count_measure_def bot_nat_0.extremum of_nat_0 of_nat_le_iff real_scaleR_def + lebesgue_integral_point_measure_finite[of _ "(\ x. 1 / card X)" "f"] + scaleR_sum_right sum_distrib_left zero_le_divide_1_iff by metis + then show ?thesis using sum_left_div_distrib by fastforce +qed + +text \A lemma to obtain a value for x where the inequality is satisfied \ +lemma expectation_obtains_ge: + fixes f :: "'a \ real" + assumes "M = uniform_count_measure X" and "finite X" + assumes "expectation f \ c" + obtains x where "x \ X" and "f x \ c" + +proof - + have ne: "X \ {}" + using assms(1) subprob_not_empty by auto + then have ne0: "card X > 0" + by (simp add: assms(2) card_gt_0_iff) + have "\ x \ X . f x \ c" + proof (rule ccontr) + assume "\ (\x\X. c \ f x)" + then have "\x\X. c > f x" by auto + then have "(\ x \ X. f x) < (\ x \ X. c)" + by (meson assms(2) ne sum_strict_mono) + then have lt: "(\ x \ X. f x) < (card X) * c" by simp + have "expectation f = (\ x \ X. f x) / card X" using expectation_uniform_count assms by auto + then have "(\ x \ X. f x) \ (card X) * c" using ne0 assms + by (simp add: le_divide_eq mult_of_nat_commute) + then show False using lt by auto + qed + then show ?thesis using that by auto +qed + +text \The following is the variation on the Cauchy-Schwarz inequality presented in Gowers's notes +before Lemma 2.13 \cite{Gowersnotes}.\ + +lemma cauchy_schwarz_ineq_var: + fixes X :: "'a \ real" + assumes "integrable M (\x. (X x)^2)" and "X \ borel_measurable M" + shows "expectation (\ x. (X x)^2) \ (expectation (\ x . (X x)))^2" + +proof - + have "expectation (\ x. (X x)^2) - (expectation (\ x . (X x)))^2 = expectation (\x. (X x - expectation X)^2)" + using variance_expectation assms(1) assms(2) by presburger + then have "expectation (\ x. (X x)^2) - (expectation (\ x . (X x)))^2 \ 0" by simp + thus ?thesis by simp +qed + +lemma integrable_uniform_count_measure_finite: + fixes g :: "'a \ 'b::{banach, second_countable_topology}" + shows "finite A \ integrable (uniform_count_measure A) g" + unfolding uniform_count_measure_def by (simp add: integrable_point_measure_finite) + +lemma cauchy_schwarz_ineq_var_uniform: + fixes X :: "'a \ real" + assumes "M = uniform_count_measure S" + assumes "finite S" + shows "expectation (\ x. (X x)^2) \ (expectation (\ x . (X x)))^2" + +proof - + have borel: "X \ borel_measurable M" using assms by (simp) + have "integrable M X" using assms by (simp add: integrable_uniform_count_measure_finite) + then have "integrable M (\ x. (X x)^2)" using assms by (simp add: integrable_uniform_count_measure_finite) + thus ?thesis using cauchy_schwarz_ineq_var borel by simp +qed + +text \An equation for expectation over a discrete random variables distribution: \ + +lemma expectation_finite_uniform_space: + assumes "M = uniform_count_measure S" and "finite S" + fixes X :: "'a \ real" + shows "expectation X = (\ y \ X ` S . prob {x \ S . X x = y} * y)" + +proof - + have "Bochner_Integration.simple_bochner_integrable M X" + proof (safe intro!: Bochner_Integration.simple_bochner_integrable.intros) + show "simple_function M X" unfolding simple_function_def using assms + by (auto simp add: space_uniform_count_measure) + show "emeasure M {y \ space M. X y \ 0} = \ \ False" + using emeasure_subprob_space_less_top by (auto) + qed + then have "expectation X = Bochner_Integration.simple_bochner_integral M X" + using simple_bochner_integrable_eq_integral by fastforce + thus ?thesis using Bochner_Integration.simple_bochner_integral_def space_uniform_count_measure + by (metis (no_types, lifting) Collect_cong assms(1) real_scaleR_def sum.cong) +qed + +lemma expectation_finite_uniform_indicator: + assumes "M = uniform_count_measure S" and "finite S" + shows "expectation (\ x. indicator (T x) y) = prob {x \ S . indicator (T x) y = 1}" (is "expectation ?X = _") + +proof - + have ss: "?X ` S \ {0, 1}" + by (intro subsetI, auto simp add: indicator_eq_1_iff) + have diff: "\ y'. y' \ ({0, 1} - ?X ` S) \ prob {x \ S . ?X x = y'} = 0" + by (metis (mono_tags, lifting) DiffD2 empty_Collect_eq image_eqI measure_empty) + have "expectation ?X = (\ y \ ?X ` S . prob {x \ S . ?X x = y} * y)" + using expectation_finite_uniform_space assms by auto + also have "... = (\ y \ ?X ` S . prob {x \ S . ?X x = y} * y) + + (\ y \ ({0, 1} - ?X ` S) . prob {x \ S . ?X x = y} * y)" + using diff by auto + also have "... = (\ y \ {0, 1} . prob {x \ S . ?X x = y} * y)" + using sum.subset_diff[of "?X ` S" "{0, 1}" "\ y. prob {x \ S . ?X x = y} * y"] ss by fastforce + also have "... = prob {x \ S . ?X x = 0} * 0 + prob {x \ S. ?X x = 1} * 1" by auto + finally have "expectation ?X = prob {x \ S. ?X x = 1}*1" by auto + thus ?thesis by (smt (verit) Collect_cong indicator_eq_1_iff) +qed + +end +end \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/ROOT b/thys/Balog_Szemeredi_Gowers/ROOT new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/ROOT @@ -0,0 +1,20 @@ +chapter AFP + +session Balog_Szemeredi_Gowers (AFP) = "HOL-Probability" + + options [timeout = 800] + sessions + Pluennecke_Ruzsa_Inequality Random_Graph_Subgraph_Threshold + Undirected_Graph_Theory + theories + Miscellaneous_Lemmas + Graph_Theory_Preliminaries + Prob_Space_Lemmas + Sumset_Triangle_Inequality + Additive_Combinatorics_Preliminaries + Additive_Energy_Lower_Bounds + Balog_Szemeredi_Gowers_Main_Proof + Balog_Szemeredi_Gowers_Supplementary + document_files + root.bib + root.tex + diff --git a/thys/Balog_Szemeredi_Gowers/Sumset_Triangle_Inequality.thy b/thys/Balog_Szemeredi_Gowers/Sumset_Triangle_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/Sumset_Triangle_Inequality.thy @@ -0,0 +1,255 @@ +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 + +context additive_abelian_group + +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" + by (smt (verit, ccfv_threshold) add_divide_distrib add_mult_distrib2 of_nat_add of_nat_mult) + 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 \ No newline at end of file diff --git a/thys/Balog_Szemeredi_Gowers/document/root.bib b/thys/Balog_Szemeredi_Gowers/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/document/root.bib @@ -0,0 +1,51 @@ +%% This BibTeX bibliography file was created using BibDesk. +%% http://bibdesk.sourceforge.net/ + + + + +%% Saved with string encoding Unicode (UTF-8) + +@article{GowersnewSzemeredi, + author = {Gowers, W. T.}, + date-modified = {2022-03-07 16:02:40 +0000}, + doi = {10.1007/s00039-001-0332-9}, + isbn = {1420-8970}, + journal = {Geometric \& Functional Analysis GAFA}, + number = {3}, + pages = {465-588}, + title = {A New Proof of {Szemer{\'e}di's} Theorem}, + volume = {11}, + year = {2001}, + bdsk-url-1 = {https://doi.org/10.1007/s00039-001-0332-9} +} + +@misc{Gowersnotes, + author = {Gowers, W. T.}, + note = {Lecture notes for Part III of the Mathematics Tripos taught at the University of Cambridge, available at \url{https://drive.google.com/file/d/1ut0mUqSyPMweoxoDTfhXverEONyFgcuO/view}}, + title = {Introduction to Additive Combinatorics}, + year = {2022} +} + + +@misc{Zhaobook, + author = {Yufei Zhao}, + date-added = {2022-04-01 15:01:03 +0100}, + date-modified = {2022-04-01 15:01:41 +0100}, + howpublished = {Online at \url{https://yufeizhao.com/gtacbook/}}, + note = {book draft}, + title = {Graph Theory and Additive Combinatorics}, + year = {2022} +} + +@article{Undirected_Graph_Theory-AFP, + author = {Chelsea Edmonds}, + title = {Undirected Graph Theory}, + journal = {Archive of Formal Proofs}, + month = {September}, + year = {2022}, + note = {\url{https://isa-afp.org/entries/Undirected_Graph_Theory.html}, + Formal proof development}, + ISSN = {2150-914x}, +} + diff --git a/thys/Balog_Szemeredi_Gowers/document/root.tex b/thys/Balog_Szemeredi_Gowers/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Balog_Szemeredi_Gowers/document/root.tex @@ -0,0 +1,62 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amssymb} +\usepackage{isabelle,isabellesym} +\usepackage[english]{babel} % for guillemots + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{The Balog--Szemer\'{e}di--Gowers Theorem} +\author{Angeliki Koutsoukou-Argyraki, Mantas Bak\v{s}ys, and Chelsea Edmonds\\ +University of Cambridge\\ +\texttt{\{ak2110, mb2412, cle47\}@cam.ac.uk}} + +\maketitle + +\begin{abstract} +We formalise the Balog--Szemer\'{e}di--Gowers Theorem, a profound result in additive combinatorics which played a central role in Gowers's proof deriving the first effective bounds for Szemer\'{e}di's Theorem \cite{GowersnewSzemeredi}. +The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects. +This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging. We demonstrate how locales, Isabelle's module system, can be employed to handle such interplays. +To treat the graph-theoretic aspects of the +proof, we make use of a new, more general undirected graph theory library developed recently by Chelsea Edmonds, which is both flexible and extensible \cite{Undirected_Graph_Theory-AFP}. +For the formalisation we followed a proof presented in the 2022 lecture notes by Timothy +Gowers "Introduction to Additive Combinatorics" for Part III of the Mathematics Tripos taught at the University of Cambridge \cite{Gowersnotes}. + In addition to the main theorem, which, following our source, is formulated for difference sets, we +also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality +following a proof by Yufei Zhao from his book "Graph Theory and Additive +Combinatorics" \cite{Zhaobook}. +We moreover formalise a few +additional results in additive combinatorics that are not used in the proof of the main theorem. +This is the first formalisation of the Balog--Szemer\'{e}di--Gowers Theorem in any proof assistant to our knowledge. + +\end{abstract} +\newpage +\tableofcontents + +\subsection*{Acknowledgements} +Angeliki Koutsoukou-Argyraki is funded by the ERC Advanced Grant ALEXANDRIA (Project GA +742178) funded by the European Research Council and led by Lawrence C. Paulson +(University of Cambridge, Department of Computer Science and Technology). +Mantas Bak\v{s}ys received funding for his internship supervised by Koutsoukou-Argyraki by the +Cambridge Mathematics Placements (CMP) Programme and by the ALEXANDRIA Project. +Chelsea Edmonds is jointly funded by the Cambridge Trust +(Cambridge Australia Scholarship) and a Cambridge Department of Computer Science and Technology Premium Research +Studentship. +\newpage + +% include generated text of all theories +\input{session} + + +\bibliographystyle{abbrv} +\bibliography{root} + + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,711 +1,712 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory +Balog_Szemeredi_Gowers BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Maximum_Segment_Sum Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL