# Theory Balog_Szemeredi_Gowers_Main_Proof

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

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}.›

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"
(* 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
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'}"
have ltc: "card {v ∈ V . vert_adj v x ∧ vert_adj v x'}/(card Y) < c"
have "{y ∈ Y . {x, x'} ⊆ neighborhood y} = {y ∈ Y . vert_adj y x ∧ vert_adj y x'}"
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"
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"])
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"]
then have lt1: "P.expectation (λ y. card (B' y)) ≤ c * (card B)" using finB
(* 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)"
(* 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)"
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 - β)})"
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"
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"
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) *
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)"
qed
next
show "X2 × X2 - H.bad_pair_set X2 Y (?δ ^ 3 / 128) ⊆ Γ.all_edges_between X2 X2"
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))"
also have "... = card (X2 × X2 - H.bad_pair_set X2 Y (?δ ^ 3 / 128))" using card_Diff_subset
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"
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)
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"
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
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
is_walk_not_empty is_walk_tl last_ConsL last_tl list.expand list.sel list.simps(3)
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
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)"
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)
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}"]
qed
have edges1: "∀ a ∈ A. ∀ b ∈ A. ({(a, 0), (b, 1)} ∈ ?E ⟷ popular_diff (b ⊖ a) c A)"
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
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 ∧ ```