Theory Balog_Szemeredi_Gowers_Main_Proof
section‹Towards the proof of the Balog--Szemer\'{e}di--Gowers Theorem›
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")
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)
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
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 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))
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
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)
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)
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
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
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
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"
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}"
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
let ?B = "(λ (a, b). a) ` X'"
let ?C = "(λ (a, b). a) ` Y'"
have hBA: "?B ⊆ A" and hCA: "?C ⊆ A" using Y'sub X'sub by auto
have inj_on_X': "inj_on (λ (a, b). a) X'" using X'sub by (intro inj_onI) (auto)
have inj_on_Y': "inj_on (λ (a, b). a) Y'" using Y'sub by (intro inj_onI) (auto)
have hBX': "card ?B = card X'" and hCY': "card ?C = card Y'"
using card_image inj_on_X' inj_on_Y' by auto
then have cardB: "card ?B ≥ (c^4) * (card A)/16" and cardC: "card ?C ≥ c^2 * (card A)/4"
using cardX' cardY' by auto
have card_ineq1: "⋀ x y. x ∈ ?B ⟹ y ∈ ?C ⟹ card ({(z, w) | z w. z ∈ A ∧ w ∈ A ∧
popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}) ≥
(c^12) * ((card A)^2) / 2^13"
proof-
fix x y assume hx: "x ∈ ?B" and hy: "y ∈ ?C"
have hxA: "x ∈ A" and hyA: "y ∈ A" using hx hy hBA hCA by auto
define f:: "'a × 'a ⇒ ('a × nat) list"
where "f ≡ (λ (z, w). [(x, 0), (z, 1), (w, 0), (y, 1)])"
have f_inj_on: "inj_on f {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" using f_def by (intro inj_onI) (auto)
have f_image: "f ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} =
{p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3}"
proof
show "f ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} ⊆
{p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3}"
proof
fix p assume hp: "p ∈ f ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}"
then obtain z w where hz: "z ∈ A" and hw: "w ∈ A" and hzx: "popular_diff (z ⊖ x) c A" and
hzw: "popular_diff (z ⊖ w) c A" and hyw: "popular_diff (y ⊖ w) c A" and
hp: "p = [(x, 0), (z, 1), (w, 0), (y, 1)]" using f_def hp by fast
then have hcon: "H.connecting_walk (x, 0) (y, 1) p"
unfolding H.connecting_walk_def H.is_walk_def
using hxA hyA H.vert_adj_def H.vert_adj_sym edges1 by simp
thus "p ∈ {p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3}"
using hp H.walk_length_conv by auto
qed
next
show "{p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3} ⊆ f ` {(z, w) |z w.
z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A}"
proof(intro subsetI)
fix p assume hp: "p ∈ {p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3}"
then have len: "length p = 4" using H.walk_length_conv by auto
have hpsub: "set p ⊆ A × {0} ∪ A × {1}" using hp H.connecting_walk_def H.is_walk_def
by auto
then have fst_sub: "fst ` set p ⊆ A" by auto
have h1A: "fst (p!1) ∈ A" and h2A: "fst (p!2) ∈ A" using fst_sub len by auto
have hpnum: "p = [p!0, p!1, p!2, p!3]"
proof (auto simp add: list_eq_iff_nth_eq len)
fix k assume "k < (4:: nat)"
then have "k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3" by auto
thus "p ! k = [p ! 0, p ! Suc 0, p ! 2, p ! 3] ! k" by fastforce
qed
then have "set (H.walk_edges p) = {{p!0, p!1} , {p!1, p!2}, {p!2, p!3}}" using
comp_sgraph.walk_edges.simps(2) comp_sgraph.walk_edges.simps(3)
by (metis empty_set list.simps(15))
then have h1: "{p!0, p!1} ∈ ?E" and h2: "{p!2, p!1} ∈ ?E" and h3: "{p!2, p!3} ∈ ?E"
using hp H.connecting_walk_def H.is_walk_def len by auto
have hxp: "p!0 = (x, 0)" using hp len hd_conv_nth H.connecting_walk_def H.is_walk_def
by fastforce
have hyp: "p!3 = (y,1)" using hp len last_conv_nth H.connecting_walk_def H.is_walk_def
by fastforce
have h1p: "p!1 = (fst (p!1), 1)"
proof-
have "p!1 ∈ A × {0} ∪ A × {1}" using hpnum hpsub
by (metis (no_types, lifting) insertCI list.simps(15) subsetD)
then have hsplit: "snd (p!1) = 0 ∨ snd (p!1) = 1" by auto
then have "snd (p!1) = 1"
proof(cases "snd (p!1) = 0")
case True
then have 1: "{(x, 0), (fst (p!1), 0)} ∈ ?E" using h1 hxp doubleton_eq_iff
by (smt (verit, del_insts) surjective_pairing)
have hY: "(fst (p!1), 0) ∉ ?Y" and hX: "(x, 0) ∈ ?X" using hxA by auto
then have 2: "{(x, 0), (fst (p!1), 0)} ∉ ?E" using H.X_vert_adj_Y H.vert_adj_def by meson
then show ?thesis using 1 2 by blast
next
case False
then show ?thesis using hsplit by auto
qed
thus "(p ! 1) = (fst (p ! 1), 1)"
by (metis (full_types) split_pairs)
qed
have h2p: "p!2 = (fst (p!2), 0)"
proof-
have "p!2 ∈ A × {0} ∪ A × {1}" using hpnum hpsub
by (metis (no_types, lifting) insertCI list.simps(15) subsetD)
then have hsplit: "snd (p!2) = 0 ∨ snd (p!2) = 1" by auto
then have "snd (p!2) = 0"
proof(cases "snd (p!2) = 1")
case True
then have 1: "{(fst (p!2), 1), (y, 1)} ∈ ?E" using h3 hyp doubleton_eq_iff
by (smt (verit, del_insts) surjective_pairing)
have hY: "(y, 1) ∉ ?X" and hX: "(fst (p!2), 1) ∈ ?Y" using hyA h2A by auto
then have 2: "{(fst (p!2), 1), (y, 1)} ∉ ?E" using H.Y_vert_adj_X H.vert_adj_def
by meson
then show ?thesis using 1 2 by blast
next
case False
then show ?thesis using hsplit by auto
qed
thus "(p ! 2) = (fst (p ! 2), 0)"
by (metis (full_types) split_pairs)
qed
have hpop1: "popular_diff ((fst (p!1)) ⊖ x) c A" using edges1 h1 hxp h1p hxA h1A
by (smt (z3))
have hpop2: "popular_diff((fst (p!1)) ⊖ (fst (p!2))) c A" using edges1 h2 h1p h2p h1A h2A
by (smt (z3))
have hpop3: "popular_diff (y ⊖ (fst (p!2))) c A" using edges1 h3 h2p hyp hyA h2A
by (smt (z3))
thus "p ∈ f ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" using f_def hpnum hxp h1p h2p hyp
h1A h2A hpop1 hpop2 hpop3 by force
qed
qed
have hx1: "(x, 0) ∈ X'" and hy2: "(y, 1) ∈ Y'" using hx X'sub hy Y'sub by auto
have "card {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} =
card {p. H.connecting_walk (x, 0) (y, 1) p ∧ H.walk_length p = 3}"
using card_image f_inj_on f_image by fastforce
thus "card {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} ≥ c ^ 12 * ((card A)^2) / 2 ^ 13"
using hx1 hy2 card_walks by auto
qed
have card_ineq2: "⋀ x y z w. x ∈ ?B ⟹ y ∈ ?C ⟹ (z, w) ∈ {(z, w) | z w. z ∈ A ∧ w ∈ A ∧
popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} ⟹
card {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧
p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w} ≥ c^3 * card A^3"
proof (auto)
fix x x2 y y2 z w assume "(x, x2) ∈ X'" and "(y, y2) ∈ Y'" and "z ∈ A" and "w ∈ A" and
1: "popular_diff (z ⊖ x) c A" and 2: "popular_diff (z ⊖ w) c A" and
3: "popular_diff (y ⊖ w) c A"
define f:: "'a × 'a × 'a × 'a × 'a × 'a ⇒ ('a × 'a) × ('a × 'a) × ('a × 'a)" where
"f ≡ (λ (p, q, r, s, t, u). ((p, q), (r, s), (t, u)))"
have f_inj: "inj_on f {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}" using f_def
by (intro inj_onI) (auto)
have f_image: "f ` {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w} =
{(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x} ×
{(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w} ×
{(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = y ⊖ w}" using f_def by force
have "card {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w} = card ({(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x} ×
{(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w} × {(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = y ⊖ w})"
using card_image f_inj f_image by fastforce
moreover have "card ({(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x} ×
{(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w} × {(p, q). p ∈ A ∧ q ∈ A ∧ p ⊖ q = y ⊖ w}) =
card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x} *
card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w} *
card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = y ⊖ w}"
using card_cartesian_product3 by auto
moreover have "c * card A ≤ card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x}"
using 1 popular_diff_def f_diff_def by auto
moreover then have "(c * card A) * (c * card A) ≤ card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x}
* card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w}"
using 2 popular_diff_def f_diff_def mult_mono assms(2) mult_nonneg_nonneg
of_nat_0_le_iff of_nat_mult by fastforce
moreover then have "(c * card A) * (c * card A) * (c * card A) ≤ card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ x}
* card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = z ⊖ w} *
card {(p, q) | p q. p ∈ A ∧ q ∈ A ∧ p ⊖ q = y ⊖ w}"
using 3 popular_diff_def f_diff_def mult_mono assms(2) mult_nonneg_nonneg of_nat_0_le_iff
of_nat_mult by fastforce
moreover have "c ^ 3 * card A ^ 3 = (c * card A) * ((c * card A) * (c * card A))"
by (simp add: power3_eq_cube algebra_simps)
ultimately show "c ^ 3 * real (card A) ^ 3 ≤
(card {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧
p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})" by auto
qed
have card_ineq3: "⋀ x y. x ∈ ?B ⟹ y ∈ ?C ⟹ card (⋃ (z, w) ∈ {(z, w) | z w. z ∈ A ∧ w ∈ A ∧
popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}.
{(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}) ≥
c ^ 15 * ((card A)^5) / 2 ^ 13"
proof-
fix x y assume hx: "x ∈ ?B" and hy: "y ∈ ?C"
have hxG: "x ∈ G" and hyG: "y ∈ G" using hx hy hBA hCA assms(4) by auto
let ?f = "(λ (z, w). {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})"
have h_pairwise_disjnt: "pairwise (λ a b. disjnt (?f a) (?f b))
{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A}"
proof (intro pairwiseI)
fix a b assume "a ∈ {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" "b ∈ {(z, w) |z w. z ∈ A ∧ w ∈ A ∧
popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" and
"a ≠ b"
then obtain a1 a2 b1 b2 where ha: "a = (a1, a2)" and hb: "b = (b1, b2)" and ha1: "a1 ∈ G" and
ha2: "a2 ∈ G" and hb1: "b1 ∈ G" and hb2: "b2 ∈ G" and hne: "(a1, a2) ≠ (b1, b2)"
using assms(4) by blast
have "(∀x. ¬ (x ∈ (?f a) ∧ x ∈ (?f b)))"
proof(intro allI notI)
fix d assume "d ∈ (?f a) ∧ d ∈ (?f b)"
then obtain p q r s t u where "d = (p, q, r, s, t, u)" and hpq1: "p ⊖ q = a1 ⊖ x" and
htu1: "t ⊖ u = y ⊖ a2" and hpq2: "p ⊖ q = b1 ⊖ x" and htu2: "t ⊖ u = y ⊖ b2"
using ha hb by auto
then have "y ⊖ a2 = y ⊖ b2" using htu1 htu2 by auto
then have 2: "a2 = b2" using ha2 hb2 hyG
by (metis additive_abelian_group.inverse_closed additive_abelian_group_axioms
invertible invertible_inverse_inverse invertible_left_cancel)
have 1: "a1 = b1" using hpq1 hpq2 ha1 hb1 hxG by simp
show "False" using 1 2 hne by auto
qed
thus "disjnt (?f a) (?f b)" using disjnt_iff[of "(?f a)" "(?f b)"] by auto
qed
have hfinite_walks: "⋀ B. B ∈ ((λ (z, w). {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}) `
{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A}) ⟹ finite B"
proof-
fix B assume "B ∈ ((λ (z, w). {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}) `
{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A})"
then have "B ⊆ A × A × A × A × A × A" by auto
thus "finite B" using assms(1)
by (auto simp add: finite_subset)
qed
have hdisj: "disjoint ((λ (z, w). {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}) `
{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A})" using h_pairwise_disjnt pairwise_image[of "disjnt" "(λ (z, w). {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})"
"{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A}"] by (simp add: pairwise_def)
have "{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} ⊆ A × A" by auto
then have hwalks_finite: "finite {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" using finite_subset assms(1)
by fastforce
have f_ineq: "∀ a ∈ {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}. c ^ 3 * (card A) ^ 3 ≤
card (?f a)" using card_ineq2 hx hy by auto
have "c ^ 15 * ((card A)^5) / 2 ^ 13 = (c ^ 12 * (card A) ^ 2 / 2 ^ 13) * (c ^ 3 * card A ^ 3)"
by (simp add: algebra_simps)
also have "... ≤ card {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A} * (c ^ 3 * (card A) ^ 3)"
using card_ineq1[of "x" "y"] hx hy mult_le_cancel_right hA by (smt (verit, best) assms(2)
mult_pos_pos of_nat_0_less_iff of_nat_le_0_iff zero_less_power)
also have "... = (∑ a ∈ {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}. (c ^ 3 * (card A) ^ 3))" by auto
also have "... ≤ (∑a∈{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}. card (?f a))"
using sum_mono f_ineq by (smt (verit, del_insts) of_nat_sum)
also have "... = sum card (?f ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A})"
using sum_card_image[of "{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}" "?f"] h_pairwise_disjnt hwalks_finite by auto
also have "... = card (⋃ (z, w)∈{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}. {(p, q, r, s, t, u) |p q r s t u.
p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧
t ⊖ u = y ⊖ w})" using card_Union_disjoint hfinite_walks hdisj by (metis (no_types, lifting))
finally show "c ^ 15 * real (card A ^ 5) / 2 ^ 13 ≤ real (card (⋃(z, w)∈{(z, w) |z w.
z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧
popular_diff (y ⊖ w) c A}. {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}))" by simp
qed
have hdsub: "∀ d ∈ differenceset ?C ?B. ∃ y ∈ ?C. ∃ x ∈ ?B.
(⋃ (z, w) ∈ {(z, w) | z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}.
{(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})
⊆ {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
proof
fix d assume "d ∈ differenceset ?C ?B"
then obtain y x where hy: "y ∈ ?C" and hx: "x ∈ ?B" and hxy: "d = y ⊖ x"
using sumset_def minusset_def hBA hCA assms(4) subset_trans
by (smt (verit, best) minusset.simps sumset.cases)
have hxG: "x ∈ G" and hyG: "y ∈ G" using hx hy hBA hCA assms(4) by auto
have "(⋃(z, w)∈{(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}. {(p, q, r, s, t, u) |p q r s t u.
p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})
⊆ {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧
d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
proof (rule Union_least)
fix X assume "X ∈ (λ(z, w). {(p, q, r, s, t, u) |p q r s t u.
p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧
t ⊖ u = y ⊖ w}) ` {(z, w) |z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}"
then obtain z w where hX: "X = {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}"
and hz: "z ∈ A" and hw: "w ∈ A" by auto
have hzG: "z ∈ G" and hwG: "w ∈ G" using hz hw assms(4) by auto
have "{(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w} ⊆
{(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧
d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
proof
fix e assume "e ∈ {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}"
then obtain p q r s t u where "p ⊖ q = z ⊖ x" and "r ⊖ s = z ⊖ w" and "t ⊖ u = y ⊖ w"
and hp: "p ∈ A" and hq: "q ∈ A" and hr: "r ∈ A" and hs: "s ∈ A" and ht: "t ∈ A"
and hu: "u ∈ A" and he: "e = (p, q, r, s, t, u)" by blast
then have "p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u = (z ⊖ x) ⊖ (z ⊖ w) ⊕ (y ⊖ w)"
by (smt (z3) additive_abelian_group.inverse_closed additive_abelian_group_axioms assms(4)
associative commutative_monoid.commutative commutative_monoid_axioms composition_closed
invertible invertible_inverse_inverse monoid.inverse_composition_commute monoid_axioms subsetD)
also have "... = (w ⊖ x) ⊕ (y ⊖ w)" using hxG hyG hzG hwG associative commutative
inverse_composition_commute invertible_right_inverse2 by auto
also have "... = y ⊖ x" using hxG hwG hyG associative commutative
by (simp add: monoid.invertible_right_inverse2 monoid_axioms)
finally have "p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u = d" using hxy by simp
thus "e ∈ {(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧
u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}" using he hp hq hr hs ht hu by auto
qed
thus "X ⊆ {(p, q, r, s, t, u) |p q r s t u.
p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
using hX by auto
qed
thus "∃y∈(λ(a, b). a) ` Y'. ∃x∈(λ(a, b). a) ` X'. (⋃(z, w)∈{(z, w) |z w. z ∈ A ∧ w ∈ A ∧
popular_diff (z ⊖ x) c A ∧ popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}.
{(p, q, r, s, t, u) |p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧
p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w}) ⊆ {(p, q, r, s, t, u) |p q r s t u.
p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
using hx hy by meson
qed
have pos: "0 < c ^ 15 * real (card A ^ 5) / 2 ^ 13" using hA ‹c>0› by auto
have "(5:: nat) ≤ 6" by auto
then have "(card A ^ 6 / card A ^ 5) = (card A) ^ (6 - 5)"
using hA power_diff by (metis of_nat_eq_0_iff of_nat_power)
then have cardApow: "(card A ^ 6 / card A ^ 5) = card A" using power_one_right by simp
moreover have "∀ d ∈ differenceset ?C ?B. card {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ (d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u)} ≥ c ^ 15 * (card A) ^ 5 / 2 ^13"
proof
fix d assume "d ∈ differenceset ?C ?B"
then obtain x y where hy: "y ∈ ?C" and hx: "x ∈ ?B" and hsub:
"(⋃ (z, w) ∈ {(z, w) | z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}.
{(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})
⊆ {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}" using hdsub by meson
have "{(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u} ⊆ A × A × A × A × A × A" by auto
then have fin: "finite {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
using finite_subset assms(1) finite_cartesian_product by fastforce
have "c ^ 15 * (card A) ^ 5 / 2 ^13 ≤ card (⋃ (z, w) ∈ {(z, w) | z w. z ∈ A ∧ w ∈ A ∧ popular_diff (z ⊖ x) c A ∧
popular_diff (z ⊖ w) c A ∧ popular_diff (y ⊖ w) c A}.
{(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧ s ∈ A ∧
t ∈ A ∧ u ∈ A ∧ p ⊖ q = z ⊖ x ∧ r ⊖ s = z ⊖ w ∧ t ⊖ u = y ⊖ w})"
using card_ineq3 hx hy by auto
also have "... ≤ card {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}"
using hsub card_mono fin by auto
finally show "c ^ 15 * (card A) ^ 5 / 2 ^13 ≤ card {(p, q, r, s, t, u) | p q r s t u. p ∈ A ∧ q ∈ A ∧ r ∈ A ∧
s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u}" by linarith
qed
moreover have "pairwise (λ s t. disjnt ((λ d. {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ (d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u)}) s)
((λ d. {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ (d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u)}) t)) (differenceset ?C ?B)"
unfolding disjnt_def by (intro pairwiseI) (auto)
moreover have "∀ d ∈ differenceset ?C ?B. ((λ d. {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ (d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u)}) d) ⊆ A × A × A × A × A × A"
by blast
ultimately have "card (differenceset ?C ?B) ≤ ((card A) ^ 6) / (c^15 * (card A)^5 /2^13)"
using assms(1) hA finite_cartesian_product card_cartesian_product_6[of "A"]
pos card_le_image_div[of "A × A × A × A × A × A" "(λ d. {(p, q, r, s, t, u)| p q r s t u. p ∈ A ∧ q ∈ A ∧
r ∈ A ∧ s ∈ A ∧ t ∈ A ∧ u ∈ A ∧ (d = p ⊖ q ⊖ r ⊕ s ⊕ t ⊖ u)})" "differenceset ?C ?B"
"(c^15 * (card A)^5 /2^13)"] by auto
also have "... = (card A ^ 6 / card A ^ 5) / (c^15 / 2^13)"
using hA assms(3) field_simps by simp
also have "... = (card A) / (c ^ 15 / 2 ^ 13)"
using cardApow by metis
finally have final: "card (differenceset ?C ?B) ≤ 2 ^ 13 * (1 / c ^ 15) * real (card A)"
by argo
have "0 < c ^ 4 * real (card A) / 16" and "0 < c ^ 2 * real (card A) / 4" using assms(2) hA by auto
then have "?B ≠ {}" and "?C ≠ {}" using cardB cardC by auto
then show ?thesis using hCA hBA cardC cardB final that by auto
qed
text‹We now show the main theorem, which is a direct application of lemma
@{term obtains_subsets_differenceset_card_bound} and the Ruzsa triangle inequality.
(The main theorem corresponds to Corollary 2.19 in Gowers's notes \cite{Gowersnotes}.) ›
theorem Balog_Szemeredi_Gowers: fixes A::"'a set" and c::real
assumes afin: "finite A" and "A ≠ {}" and "c>0" and "additive_energy A = 2 * c" and ass: "A ⊆ G"
obtains A' where "A' ⊆ A" and "card A' ≥ c^2 * card A / 4" and
"card (differenceset A' A') ≤ 2^30 * card A / c^34"
proof-
obtain B and A' where bss: "B ⊆ A" and bne: "B ≠ {}" and bge: "card B ≥ (c^4) * (card A)/16"
and a2ss: "A' ⊆ A" and a2ge: "card A' ≥ (c^2) * (card (A))/4"
and hcardle: "card (differenceset A' B) ≤ 2^13 * card A / c^15"
using assms obtains_subsets_differenceset_card_bound by metis
have Bg0: "(card B :: real) > 0" using bne afin bss infinite_super by fastforce
have "(card B) * card (differenceset A' A') ≤
card (differenceset A' B) * card (differenceset A' B)"
using afin a2ss bss infinite_super ass Ruzsa_triangle_ineq1 card_minusset' differenceset_commute
sumset_subset_carrier subset_trans sumset_commute by (smt (verit, best))
then have "card B * card (differenceset A' A') ≤ (card (differenceset A' B))^2"
using bss bss power2_eq_square by metis
then have "(card (differenceset A' A')) ≤ (card (differenceset A' B))^2/card B"
using Bg0 nonzero_mult_div_cancel_left[of "card B" "card(differenceset A' A')"]
divide_right_mono by (smt (verit) of_nat_0 of_nat_mono of_nat_div_le_of_nat)
moreover have "(card (differenceset A' B))^2 ≤ ((2^13) * (1/c^15)*(card A))^2"
using hcardle by simp
ultimately have "(card (differenceset A' A')) ≤ ((2^13) * (1/c^15)*(card A))^2/(card B)"
using pos_le_divide_eq[OF Bg0] by simp
moreover have "(c^4) * (card A)/16 >0"
using assms card_0_eq by fastforce
moreover have "((2^13) * (1/c^15) * (card A))^2/(card B) =
((2^13)* (1/c^15)*(card A))^2 * (1/(card B))" by simp
moreover have "((2^13)* (1/c^15) * (card A))^2 * (1/(card B)) ≤
((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)"
using bge calculation(2, 3) frac_le less_eq_real_def zero_le_power2 by metis
ultimately have "(card (differenceset A' A')) ≤ ((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)"
by linarith
then have "(card (differenceset A' A')) ≤ (2^30) * (card A)/(c^34)"
using card_0_eq assms by (simp add: power2_eq_square)
then show ?thesis using a2ss a2ge that by blast
qed
text‹The following is an analogous version of the Balog--Szemer\'{e}di--Gowers
Theorem for a sumset instead of a difference set. The proof is similar to that of the original
version, again using @{term obtains_subsets_differenceset_card_bound}, however, instead
of the Ruzsa triangle inequality we will use the alternative triangle inequality for sumsets
@{term triangle_ineq_sumsets}. ›
theorem Balog_Szemeredi_Gowers_sumset: fixes A::"'a set" and c::real
assumes afin: "finite A" and "A ≠ {}" and "c>0" and "additive_energy A = 2 * c" and ass: "A ⊆ G"
obtains A' where "A' ⊆ A" and "card A' ≥ c^2 * card A / 4" and
"card (sumset A' A') ≤ 2^30 * card A / c^34"
proof-
obtain B and A' where bss: "B ⊆ A" and bne: "B ≠ {}" and bge: "card B ≥ (c^4) * (card A)/16"
and a2ss: "A' ⊆ A" and a2ne: "A' ≠ {}" and a2ge: "card A' ≥ (c^2) * (card (A))/4"
and hcardle: "card (differenceset A' B) ≤ 2^13 * card A / c^15"
using assms obtains_subsets_differenceset_card_bound by metis
have finA': "finite A'" and finB: "finite B" using afin a2ss bss using infinite_super by auto
have bg0: "(card B :: real) > 0" using bne afin bss infinite_super by fastforce
have "card (minusset B) * card (sumset A' A') ≤
card (sumset (minusset B) A') * card (sumset (minusset B) A')"
using finA' finB ass a2ss bss triangle_ineq_sumsets
finite_minusset minusset_subset_carrier subset_trans by metis
then have "card B * card (sumset A' A') ≤ (card (differenceset A' B))^2"
using card_minusset bss ass power2_eq_square
by (metis card_minusset' subset_trans sumset_commute)
then have "(card (sumset A' A')) ≤ (card (differenceset A' B))^2/card B"
using bg0 nonzero_mult_div_cancel_left[of "card B" "card(sumset A' A')"]
divide_right_mono by (smt (verit) of_nat_0 of_nat_mono of_nat_div_le_of_nat)
moreover have "(card (differenceset A' B))^2 ≤ ((2^13) * (1/c^15) * (card A))^2"
using hcardle by simp
ultimately have "(card (sumset A' A')) ≤ ((2^13) * (1/c^15) * (card A))^2/(card B)"
using pos_le_divide_eq[OF bg0] by simp
moreover have "(c^4) * (card A)/16 >0"
using assms card_0_eq by fastforce
moreover have "((2^13) * (1/c^15) * (card A))^2/(card B) =
((2^13)* (1/c^15) * (card A))^2 * (1/(card B))" by simp
moreover have "((2^13) * (1/c^15)*(card A))^2 * (1/(card B)) ≤
((2^13) * (1/c^15) * (card A))^2/ ((c^4) * (card A)/16)" using bge frac_le less_eq_real_def
zero_le_power2 calculation(2, 3) by metis
ultimately have "(card (sumset A' A')) ≤ ((2^13) * (1/c^15)*(card A))^2/ ((c^4) * (card A)/16)"
by linarith
then have "(card (sumset A' A')) ≤ (2^30) * (card A)/(c^34)"
using card_0_eq assms by (simp add: power2_eq_square)
then show ?thesis using a2ss a2ne a2ge that by blast
qed
end
end