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⇧^{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)⇧^{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⇧^{2}* real ((card A)⇧^{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 ∧