Theory Roth_Arithmetic_Progressions
section‹Roth's Theorem on Arithmetic Progressions›
theory Roth_Arithmetic_Progressions
imports Szemeredi_Regularity.Szemeredi
"Random_Graph_Subgraph_Threshold.Subgraph_Threshold"
"Ergodic_Theory.Asymptotic_Density"
"HOL-Library.Ramsey" "HOL-Library.Nat_Bijection"
begin
subsection ‹Miscellaneous Preliminaries›
lemma sum_prod_le_prod_sum:
fixes a :: "'a ⇒ 'b::linordered_idom"
assumes "⋀i. i ∈ I ⟹ a i ≥ 0 ∧ b i ≥ 0"
shows "(∑i∈I. ∑j∈I. a i * b j) ≤ (∑i∈I. a i) * (∑i∈I. b i)"
using assms
by (induction I rule: infinite_finite_induct) (auto simp add: algebra_simps sum.distrib sum_distrib_left)
lemma real_mult_gt_cube: "A ≥ (X ::real) ⟹ B ≥ X ⟹ C ≥ X ⟹ X ≥ 0 ⟹ A * B * C ≥ X^3"
by (simp add: mult_mono' power3_eq_cube)
lemma triple_sigma_rewrite_card:
assumes "finite X" "finite Y" "finite Z"
shows "card {(x,y,z) . x ∈ X ∧ (y,z) ∈ Y × Z ∧ P x y z} = (∑x∈ X . card {(y,z) ∈ Y × Z. P x y z})"
proof -
define W where "W ≡ λx. {(y,z) ∈ Y × Z. P x y z}"
have "W x ⊆ Y × Z" for x
by (auto simp: W_def)
then have [simp]: "finite (W x)" for x
by (meson assms finite_SigmaI infinite_super)
have eq: "{(x,y,z) . x ∈ X ∧ (y,z) ∈ Y × Z ∧ P x y z} = (⋃x∈X. ⋃(y,z)∈W x. {(x,y,z)})"
by (auto simp: W_def)
show ?thesis
unfolding eq by (simp add: disjoint_iff assms card_UN_disjoint) (simp add: W_def)
qed
lemma all_edges_between_mono1:
"Y ⊆ Z ⟹ all_edges_between Y X G ⊆ all_edges_between Z X G"
by (auto simp: all_edges_between_def)
lemma all_edges_between_mono2:
"Y ⊆ Z ⟹ all_edges_between X Y G ⊆ all_edges_between X Z G"
by (auto simp: all_edges_between_def)
lemma uwellformed_alt_fst:
assumes "uwellformed G" "{x, y} ∈ uedges G"
shows "x ∈ uverts G"
using uwellformed_def assms by simp
lemma uwellformed_alt_snd:
assumes "uwellformed G" "{x, y} ∈ uedges G"
shows "y ∈ uverts G"
using uwellformed_def assms by simp
lemma all_edges_between_subset_times: "all_edges_between X Y G ⊆ (X ∩ ⋃(uedges G)) × (Y ∩ ⋃(uedges G))"
by (auto simp: all_edges_between_def)
lemma finite_all_edges_between':
assumes "finite (uverts G)" "uwellformed G"
shows "finite (all_edges_between X Y G)"
proof -
have "finite (⋃(uedges G))"
by (meson Pow_iff all_edges_subset_Pow assms finite_Sup subsetD wellformed_all_edges)
with all_edges_between_subset_times show ?thesis
by (metis finite_Int finite_SigmaI finite_subset)
qed
lemma all_edges_between_E_diff:
"all_edges_between X Y (V,E-E') = all_edges_between X Y (V,E) - all_edges_between X Y (V,E')"
by (auto simp: all_edges_between_def)
lemma all_edges_between_E_Un:
"all_edges_between X Y (V,E∪E') = all_edges_between X Y (V,E) ∪ all_edges_between X Y (V,E')"
by (auto simp: all_edges_between_def)
lemma all_edges_between_E_UN:
"all_edges_between X Y (V, ⋃i∈I. E i) = (⋃i∈I. all_edges_between X Y (V,E i))"
by (auto simp: all_edges_between_def)
lemma all_edges_preserved: "⟦all_edges_between A B G' = all_edges_between A B G; X ⊆ A; Y ⊆ B⟧
⟹ all_edges_between X Y G' = all_edges_between X Y G"
by (auto simp: all_edges_between_def)
lemma subgraph_edge_wf:
assumes "uwellformed G" "uverts H = uverts G" "uedges H ⊆ uedges G"
shows "uwellformed H"
by (metis assms subsetD uwellformed_def)
subsection ‹Preliminaries on Neighbors in Graphs›
definition neighbor_in_graph:: " uvert ⇒ uvert ⇒ ugraph ⇒ bool"
where "neighbor_in_graph x y G ≡ (x ∈ (uverts G) ∧ y ∈ (uverts G) ∧ {x,y} ∈ (uedges G))"
definition neighbors :: "uvert ⇒ ugraph ⇒ uvert set" where
"neighbors x G ≡ {y ∈ uverts G . neighbor_in_graph x y G}"
definition neighbors_ss:: "uvert ⇒ uvert set ⇒ ugraph ⇒ uvert set" where
"neighbors_ss x Y G ≡ {y ∈ Y . neighbor_in_graph x y G}"
lemma all_edges_betw_sigma_neighbor:
"uwellformed G ⟹ all_edges_between X Y G = (SIGMA x:X. neighbors_ss x Y G)"
by (auto simp add: all_edges_between_def neighbors_ss_def neighbor_in_graph_def
uwellformed_alt_fst uwellformed_alt_snd)
lemma card_all_edges_betw_neighbor:
assumes "finite X" "finite Y" "uwellformed G"
shows "card (all_edges_between X Y G) = (∑x∈X. card (neighbors_ss x Y G))"
using all_edges_betw_sigma_neighbor assms by (simp add: neighbors_ss_def)
subsection ‹Preliminaries on Triangles in Graphs›
definition triangle_in_graph:: "uvert ⇒ uvert ⇒ uvert ⇒ ugraph ⇒ bool"
where "triangle_in_graph x y z G
≡ ({x,y} ∈ uedges G) ∧ ({y,z} ∈ uedges G) ∧ ({x,z} ∈ uedges G)"
definition triangle_triples
where "triangle_triples X Y Z G ≡ {(x,y,z) ∈ X × Y × Z. triangle_in_graph x y z G}"
lemma triangle_commu1:
assumes "triangle_in_graph x y z G"
shows "triangle_in_graph y x z G"
using assms triangle_in_graph_def by (auto simp add: insert_commute)
lemma triangle_vertices_distinct1:
assumes wf: "uwellformed G"
assumes tri: "triangle_in_graph x y z G"
shows "x ≠ y"
proof (rule ccontr)
assume a: "¬ x ≠ y"
have "card {x, y} = 2" using tri wf triangle_in_graph_def
using uwellformed_def by blast
thus False using a by simp
qed
lemma triangle_vertices_distinct2:
assumes "uwellformed G" "triangle_in_graph x y z G"
shows "y ≠ z"
by (metis assms triangle_vertices_distinct1 triangle_in_graph_def)
lemma triangle_in_graph_edge_point:
assumes "uwellformed G"
shows "triangle_in_graph x y z G ⟷ {y, z} ∈ uedges G ∧ neighbor_in_graph x y G ∧ neighbor_in_graph x z G"
by (auto simp add: triangle_in_graph_def neighbor_in_graph_def assms uwellformed_alt_fst uwellformed_alt_snd)
definition
"unique_triangles G
≡ ∀e ∈ uedges G. ∃!T. ∃x y z. T = {x,y,z} ∧ triangle_in_graph x y z G ∧ e ⊆ T"
definition triangle_free_graph:: "ugraph ⇒ bool"
where "triangle_free_graph G ≡ ¬(∃ x y z. triangle_in_graph x y z G )"
lemma triangle_free_graph_empty: "uedges G = {} ⟹ triangle_free_graph G"
by (simp add: triangle_free_graph_def triangle_in_graph_def)
lemma edge_vertices_not_equal:
assumes "uwellformed G" "{x,y} ∈ uedges G"
shows "x ≠ y"
using assms triangle_in_graph_def triangle_vertices_distinct1 by blast
lemma triangle_in_graph_verts:
assumes "uwellformed G" "triangle_in_graph x y z G"
shows "x ∈ uverts G" "y ∈ uverts G" "z∈ uverts G"
proof -
have 1: "{x, y} ∈ uedges G" using triangle_in_graph_def
using assms(2) by auto
then show "x ∈ uverts G" using uwellformed_alt_fst assms by blast
then show "y ∈ uverts G" using 1 uwellformed_alt_snd assms by blast
have "{x, z} ∈ uedges G" using triangle_in_graph_def assms(2) by auto
then show "z ∈ uverts G" using uwellformed_alt_snd assms by blast
qed
definition triangle_set :: "ugraph ⇒ uvert set set"
where "triangle_set G ≡ { {x,y,z} | x y z. triangle_in_graph x y z G}"
fun mk_triangle_set :: "(uvert × uvert × uvert) ⇒ uvert set"
where "mk_triangle_set (x,y,z) = {x,y,z}"
lemma finite_triangle_set:
assumes fin: "finite (uverts G)" and wf: "uwellformed G"
shows "finite (triangle_set G)"
proof -
have "triangle_set G ⊆ Pow (uverts G)"
using PowI local.wf triangle_in_graph_def triangle_set_def uwellformed_def by auto
then show ?thesis
by (meson fin finite_Pow_iff infinite_super)
qed
lemma card_triangle_3:
assumes "t ∈ triangle_set G" "uwellformed G"
shows "card t = 3"
using assms by (auto simp: triangle_set_def edge_vertices_not_equal triangle_in_graph_def)
lemma triangle_set_power_set_ss: "uwellformed G ⟹ triangle_set G ⊆ Pow (uverts G)"
by (auto simp add: triangle_set_def triangle_in_graph_def uwellformed_alt_fst uwellformed_alt_snd)
lemma triangle_in_graph_ss:
assumes "uedges Gnew ⊆ uedges G"
assumes "triangle_in_graph x y z Gnew"
shows "triangle_in_graph x y z G"
using assms triangle_in_graph_def by auto
lemma triangle_set_graph_edge_ss:
assumes "uedges Gnew ⊆ uedges G"
assumes "uverts Gnew = uverts G"
shows "triangle_set Gnew ⊆ triangle_set G"
using assms unfolding triangle_set_def by (blast intro: triangle_in_graph_ss)
lemma triangle_set_graph_edge_ss_bound:
fixes G :: "ugraph" and Gnew :: "ugraph"
assumes "uwellformed G" "finite (uverts G)" "uedges Gnew ⊆ uedges G" "uverts Gnew = uverts G"
shows "card (triangle_set G) ≥ card (triangle_set Gnew)"
by (simp add: assms card_mono finite_triangle_set triangle_set_graph_edge_ss)
subsection ‹The Triangle Counting Lemma and the Triangle Removal Lemma›
text‹We begin with some more auxiliary material to be used in the main lemmas.›
lemma regular_pair_neighbor_bound:
fixes ε::real
assumes finG: "finite (uverts G)"
assumes xss: "X ⊆ uverts G" and yss: "Y ⊆ uverts G" and "card X > 0"
and wf: "uwellformed G"
and eg0: "ε > 0" and "ε-regular_pair X Y G" and ed: "edge_density X Y G ≥ 2*ε"
defines "X' ≡ {x ∈ X. card (neighbors_ss x Y G) < (edge_density X Y G - ε) * card (Y)}"
shows "card X' < ε * card X"
(is "card (?X') < ε * _")
proof (cases "?X' = {}")
case False
let ?rxy = "1/(card X' * card Y)"
show ?thesis
proof (rule ccontr)
assume "¬ (card (X') < ε * card X) "
then have a: "(card(X') ≥ ε * card X) " by simp
have fin: "finite X" "finite Y" using assms finite_subset by auto
have ebound: "ε ≤ 1/2"
by (metis ed edge_density_le1 le_divide_eq_numeral1(1) mult.commute order_trans)
have finx: "finite X'" using fin X'_def by simp
have "⋀ x. x ∈ X'⟹ (card (neighbors_ss x Y G)) < (edge_density X Y G - ε) * (card Y)"
unfolding X'_def by blast
then have "(∑x∈X'. card (neighbors_ss x Y G)) < (∑x∈X'. ((edge_density X Y G - ε) * (card Y)))"
using False sum_strict_mono X'_def
by (smt (verit, del_insts) finx of_nat_sum)
then have upper: "(∑x∈X'. card (neighbors_ss x Y G)) < (card X') * ((edge_density X Y G - ε) * (card Y))"
by (simp add: sum_bounded_above)
have yge0: "card Y > 0"
by (metis gr0I mult_eq_0_iff of_nat_0 of_nat_less_0_iff upper)
have "?rxy > 0"
using card_0_eq finx False yge0 X'_def by fastforce
then have upper2: "?rxy * (∑x∈X'. card (neighbors_ss x Y G)) < ?rxy * (card X') * ((edge_density X Y G - ε) * (card Y))"
by (smt (verit) mult.assoc mult_le_cancel_left upper)
have "?rxy * (card X') * ((edge_density X Y G - ε) * (card Y)) = edge_density X Y G - ε"
using False X'_def finx by force
with ‹ε > 0› upper2 have con: "edge_density X Y G - ?rxy * (∑x∈X'. card (neighbors_ss x Y G)) > ε"
by linarith
have "¦edge_density X Y G - ?rxy * (∑x∈X'. card (neighbors_ss x Y G))¦
= ¦?rxy * (card (all_edges_between X' Y G)) - edge_density X Y G¦"
using card_all_edges_betw_neighbor fin wf by (simp add: X'_def)
also have "... = ¦edge_density X' Y G - edge_density X Y G¦"
by (simp add: edge_density_def)
also have "... ≤ ε"
using assms ebound yge0 a by (force simp add: X'_def regular_pair_def)
finally show False using con by linarith
qed
qed (simp add: ‹card X > 0› eg0)
lemma neighbor_set_meets_e_reg_cond:
fixes ε::real
assumes "edge_density X Y G ≥ 2*ε"
and "card (neighbors_ss x Y G) ≥ (edge_density X Y G - ε) * card Y"
shows "card (neighbors_ss x Y G) ≥ ε * card (Y)"
by (smt (verit) assms mult_right_mono of_nat_0_le_iff)
lemma all_edges_btwn_neighbor_sets_lower_bound:
fixes ε::real
assumes rp2: "ε-regular_pair Y Z G"
and ed1: "edge_density X Y G ≥ 2*ε" and ed2: "edge_density X Z G ≥ 2*ε"
and cond1: "card (neighbors_ss x Y G) ≥ (edge_density X Y G - ε) * card Y"
and cond2: "card (neighbors_ss x Z G) ≥ (edge_density X Z G - ε) * card Z"
shows "card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)
≥ (edge_density Y Z G - ε) * card (neighbors_ss x Y G) * card (neighbors_ss x Z G)"
(is "card (all_edges_between ?Y' ?Z' G) ≥ (edge_density Y Z G - ε) * card ?Y' * card ?Z'")
proof -
have yss': "?Y' ⊆ Y" using neighbors_ss_def by simp
have zss': "?Z' ⊆ Z" using neighbors_ss_def by simp
have min_sizeY: "card ?Y' ≥ ε * card Y"
using cond1 ed1 neighbor_set_meets_e_reg_cond by blast
have min_sizeZ: "card ?Z' ≥ ε * card Z"
using cond2 ed2 neighbor_set_meets_e_reg_cond by blast
then have "¦ edge_density ?Y' ?Z' G - edge_density Y Z G ¦ ≤ ε"
using min_sizeY yss' zss' assms by (force simp add: regular_pair_def)
then have "edge_density Y Z G - ε ≤ (card (all_edges_between ?Y' ?Z' G)/(card ?Y' * card ?Z'))"
using edge_density_def by simp
then have "(card ?Y' * card ?Z') * (edge_density Y Z G - ε) ≤ (card (all_edges_between ?Y' ?Z' G))"
by (fastforce simp: divide_simps mult.commute simp flip: of_nat_mult split: if_split_asm)
then show ?thesis
by (metis (no_types, lifting) mult.assoc mult_of_nat_commute of_nat_mult)
qed
text‹We are now ready to show the Triangle Counting Lemma:›
theorem triangle_counting_lemma:
fixes ε::real
assumes xss: "X ⊆ uverts G" and yss: "Y ⊆ uverts G" and zss: "Z ⊆ uverts G" and en0: "ε > 0"
and finG: "finite (uverts G)" and wf: "uwellformed G"
and rp1: "ε-regular_pair X Y G" and rp2: "ε-regular_pair Y Z G" and rp3: "ε-regular_pair X Z G"
and ed1: "edge_density X Y G ≥ 2*ε" and ed2: "edge_density X Z G ≥ 2*ε" and ed3: "edge_density Y Z G ≥ 2*ε"
shows "card (triangle_triples X Y Z G)
≥ (1-2*ε) * (edge_density X Y G - ε) * (edge_density X Z G - ε) * (edge_density Y Z G - ε)*
card X * card Y * card Z"
proof -
let ?T_all = "{(x,y,z) ∈ X × Y × Z. (triangle_in_graph x y z G)}"
let ?ediff = "λX Y. edge_density X Y G - ε"
define XF where "XF ≡ λY. {x ∈ X. card(neighbors_ss x Y G) < ?ediff X Y * card Y}"
have fin: "finite X" "finite Y" "finite Z" using finG rev_finite_subset xss yss zss by auto
then have "card X > 0"
using card_0_eq ed1 edge_density_def en0 by fastforce
text‹ Obtain a subset of @{term X} where all elements meet minimum numbers for neighborhood size
in @{term Y} and @{term Z}.›
define X2 where "X2 ≡ X - (XF Y ∪ XF Z)"
have xss: "X2 ⊆ X" and finx2: "finite X2"
by (auto simp add: X2_def fin)
text ‹Reasoning on the minimum size of @{term X2}:›
have part1: "(XF Y ∪ XF Z) ∪ X2 = X"
by (auto simp: XF_def X2_def)
have card_XFY: "card (XF Y) < ε * card X"
using regular_pair_neighbor_bound assms ‹card X > 0› by (simp add: XF_def)
text‹ We now repeat the same argument as above to the regular pair @{term X} @{term Z} in @{term G}.›
have card_XFZ: "card (XF Z) < ε * card X"
using regular_pair_neighbor_bound assms ‹card X > 0› by (simp add: XF_def)
have "card (XF Y ∪ XF Z) ≤ 2 * ε * (card X)"
by (smt (verit) card_XFY card_XFZ card_Un_le comm_semiring_class.distrib of_nat_add of_nat_mono)
then have "card X2 ≥ card X - 2 * ε * card X"
using part1 by (smt (verit, del_insts) card_Un_le of_nat_add of_nat_mono)
then have minx2: "card X2 ≥ (1 - 2 * ε) * card X"
by (metis mult.commute mult_cancel_left2 right_diff_distrib)
text ‹Reasoning on the minimum number of edges between neighborhoods of @{term X} in @{term Y}
and @{term Z}.›
have edyzgt0: "?ediff Y Z > 0" and edxygt0: "?ediff X Y > 0"
using ed1 ed3 ‹ε > 0› by linarith+
have card_y_bound: "card (neighbors_ss x Y G) ≥ ?ediff X Y * card Y"
and card_z_bound: "card (neighbors_ss x Z G) ≥ ?ediff X Z * card Z"
if "x ∈ X2" for x
using that by (auto simp: XF_def X2_def)
have card_y_bound':
"(∑x∈ X2. ?ediff Y Z * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) ≥
(∑x∈ X2. ?ediff Y Z * ?ediff X Y * (card Y) * (card (neighbors_ss x Z G)))"
by (rule sum_mono) (smt (verit, best) mult.left_commute card_y_bound edyzgt0 mult.commute mult_right_mono of_nat_0_le_iff)
have card_z_bound':
"(∑x∈ X2. ?ediff Y Z * ?ediff X Y * (card Y) * (card (neighbors_ss x Z G))) ≥
(∑x∈ X2. ?ediff Y Z * ?ediff X Y * (card Y) * ?ediff X Z * (card Z))"
using card_z_bound mult_left_mono edxygt0 edyzgt0 by (fastforce intro!: sum_mono)
have eq_set: "⋀x. {(y,z). y ∈ Y ∧ z ∈ Z ∧ {y, z} ∈ uedges G ∧ neighbor_in_graph x y G ∧ neighbor_in_graph x z G } =
{(y,z). y ∈ (neighbors_ss x Y G) ∧ z ∈ (neighbors_ss x Z G) ∧ {y, z} ∈ uedges G }"
by (auto simp: neighbors_ss_def)
have "card ?T_all = (∑x∈ X . card {(y,z) ∈ Y × Z. triangle_in_graph x y z G})"
using triple_sigma_rewrite_card fin by force
also have "… = (∑x∈ X . card {(y,z). y ∈ Y ∧ z ∈ Z ∧ {y, z} ∈ uedges G ∧ neighbor_in_graph x y G ∧ neighbor_in_graph x z G })"
using triangle_in_graph_edge_point assms by auto
also have "... = (∑x ∈ X. card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))"
using all_edges_between_def eq_set by presburger
finally have l: "card ?T_all ≥ (∑x∈ X2 . card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))"
by (simp add: fin xss sum_mono2)
have "(∑x∈ X2. ?ediff Y Z * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) ≤
(∑x∈ X2. real (card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)))"
(is "sum ?F _ ≤ sum ?G _")
proof (rule sum_mono)
show "⋀x. x ∈ X2 ⟹ ?F x ≤ ?G x"
using all_edges_btwn_neighbor_sets_lower_bound card_y_bound card_z_bound ed1 ed2 rp2 by blast
qed
then have "card ?T_all ≥ card X2 * ?ediff Y Z * ?ediff X Y * card Y * ?ediff X Z * card Z"
using card_z_bound' card_y_bound' l of_nat_le_iff [symmetric, where 'a=real] by force
then have "real (card ?T_all) ≥ ((1 - 2 * ε) * card X) * ?ediff Y Z *
?ediff X Y * (card Y) * ?ediff X Z * (card Z)"
by (smt (verit, best) ed2 edxygt0 edyzgt0 en0 minx2 mult_right_mono of_nat_0_le_iff)
then show ?thesis by (simp add: triangle_triples_def mult.commute mult.left_commute)
qed
definition regular_graph :: "real ⇒ uvert set set ⇒ ugraph ⇒ bool"
(‹_-regular'_graph› [999]1000)
where "ε-regular_graph P G ≡ ∀R S. R∈P ⟶ S∈P ⟶ ε-regular_pair R S G" for ε::real
text ‹A minimum density, but empty edge sets are excluded.›
definition edge_dense :: "nat set ⇒ nat set ⇒ ugraph ⇒ real ⇒ bool"
where "edge_dense X Y G ε ≡ all_edges_between X Y G = {} ∨ edge_density X Y G ≥ ε"
definition dense_graph :: "uvert set set ⇒ ugraph ⇒ real ⇒ bool"
where "dense_graph P G ε ≡ ∀R S. R∈P ⟶ S∈P ⟶ edge_dense R S G ε" for ε::real
definition decent :: "nat set ⇒ nat set ⇒ ugraph ⇒ real ⇒ bool"
where "decent X Y G η ≡ all_edges_between X Y G = {} ∨ (card X ≥ η ∧ card Y ≥ η)" for η::real
definition decent_graph :: "uvert set set ⇒ ugraph ⇒ real ⇒ bool"
where "decent_graph P G η ≡ ∀R S. R∈P ⟶ S∈P ⟶ decent R S G η"
text ‹The proof of the triangle counting lemma requires ordered triples. For each unordered triple
there are six permutations, hence the factor of $1/6$ here.›
lemma card_convert_triangle_rep:
fixes G :: "ugraph"
assumes "X ⊆ uverts G" and "Y ⊆ uverts G" and "Z ⊆ uverts G" and fin: "finite (uverts G)"
and wf: "uwellformed G"
shows "card (triangle_set G) ≥ 1/6 * card {(x,y,z) ∈ X × Y × Z . (triangle_in_graph x y z G)}"
(is "_ ≥ 1/6 * card ?TT")
proof -
define tofl where "tofl ≡ λl::nat list. (hd l, hd(tl l), hd(tl(tl l)))"
have in_tofl: "(x,y,z) ∈ tofl ` permutations_of_set {x,y,z}" if "x≠y" "y≠z" "x≠z" for x y z
proof -
have "distinct[x,y,z]"
using that by simp
then show ?thesis
unfolding tofl_def image_iff
by (smt (verit, best) list.sel(1) list.sel(3) set_simps permutations_of_setI set_empty)
qed
have "?TT ⊆ {(x,y,z). (triangle_in_graph x y z G)}"
by auto
also have "… ⊆ (⋃t ∈ triangle_set G. tofl ` permutations_of_set t)"
using edge_vertices_not_equal [OF wf] in_tofl
by (clarsimp simp add: triangle_set_def triangle_in_graph_def) metis
finally have "?TT ⊆ (⋃t ∈ triangle_set G. tofl ` permutations_of_set t)" .
then have "card ?TT ≤ card(⋃t ∈ triangle_set G. tofl ` permutations_of_set t)"
by (intro card_mono finite_UN_I finite_triangle_set) (auto simp: assms)
also have "… ≤ (∑t ∈ triangle_set G. card (tofl ` permutations_of_set t))"
using card_UN_le fin finite_triangle_set local.wf by blast
also have "… ≤ (∑t ∈ triangle_set G. card (permutations_of_set t))"
by (meson card_image_le finite_permutations_of_set sum_mono)
also have "… ≤ (∑t ∈ triangle_set G. fact 3)"
by (rule sum_mono) (metis card.infinite card_permutations_of_set card_triangle_3 eq_refl local.wf nat.case numeral_3_eq_3)
also have "… = 6 * card (triangle_set G)"
by (simp add: eval_nat_numeral)
finally have "card ?TT ≤ 6 * card (triangle_set G)" .
then show ?thesis
by (simp add: divide_simps)
qed
lemma card_convert_triangle_rep_bound:
fixes G :: "ugraph" and t :: real
assumes "X ⊆ uverts G" and "Y ⊆ uverts G" and "Z ⊆ uverts G" and fin: "finite (uverts G)"
and wf: "uwellformed G"
assumes "card {(x,y,z) ∈ X × Y × Z . (triangle_in_graph x y z G)} ≥ t"
shows "card (triangle_set G) ≥ 1/6 *t"
proof -
define t' where "t' ≡ card {(x,y,z) ∈ X × Y × Z . (triangle_in_graph x y z G)}"
have "t' ≥ t" using assms t'_def by simp
then have tgt: "1/6 * t' ≥ 1/6 * t" by simp
have "card (triangle_set G) ≥ 1/6 *t'" using t'_def card_convert_triangle_rep assms by simp
thus ?thesis using tgt by linarith
qed
lemma edge_density_eq0:
assumes "all_edges_between A B G = {}" and "X ⊆ A" "Y ⊆ B"
shows "edge_density X Y G = 0"
proof -
have "all_edges_between X Y G = {}"
by (metis all_edges_between_mono1 all_edges_between_mono2 assms subset_empty)
then show ?thesis
by (auto simp: edge_density_def)
qed
text‹The following is the Triangle Removal Lemma.›
theorem triangle_removal_lemma:
fixes ε :: real
assumes egt: "ε > 0"
shows "∃δ::real > 0. ∀G. card(uverts G) > 0 ⟶ uwellformed G ⟶
card (triangle_set G) ≤ δ * card(uverts G) ^ 3 ⟶
(∃G'. triangle_free_graph G' ∧ uverts G' = uverts G ∧ uedges G' ⊆ uedges G ∧
card (uedges G - uedges G') ≤ ε * (card (uverts G))⇧2)"
(is "∃δ::real > 0. ∀G. _ ⟶ _ ⟶ _ ⟶ (∃Gnew. ?Φ G Gnew)")
proof (cases "ε < 1")
case False
show ?thesis
proof (intro exI conjI strip)
fix G
define Gnew where "Gnew ≡ ((uverts G), {}::uedge set)"
assume G: "uwellformed G" "card(uverts G) > 0"
then show "triangle_free_graph Gnew" "uverts Gnew = uverts G" "uedges Gnew ⊆ uedges G"
by (auto simp: Gnew_def triangle_free_graph_empty)
have "real (card (uedges G)) ≤ (card (uverts G))⇧2"
by (meson G card_gt_0_iff max_edges_graph of_nat_le_iff)
also have "… ≤ ε * (card (uverts G))⇧2"
using False mult_le_cancel_right1 by fastforce
finally show "real (card (uedges G - uedges Gnew)) ≤ ε * ((card (uverts G))⇧2)"
by (simp add: Gnew_def)
qed (rule zero_less_one)
next
case True
have e4gt: "ε/4 > 0" using ‹ε > 0› by auto
then obtain M0 where
M0: "⋀G. card (uverts G) > 0 ⟹ ∃P. regular_partition (ε/4) G P ∧ card P ≤ M0"
and "M0>0"
by (metis Szemeredi_Regularity_Lemma le0 neq0_conv not_le not_numeral_le_zero)
define D0 where "D0 ≡ 1/6 *(1-(ε/2))*((ε/4)^3)*((ε /(4*M0))^3)"
have "D0 > 0"
using ‹0 < ε› ‹ε < 1› ‹M0 > 0› by (simp add: D0_def zero_less_mult_iff)
then obtain δ:: "real" where δ: "0 < δ" "δ < D0"
by (meson dense)
show ?thesis
proof (rule exI, intro conjI strip)
fix G
assume "card(uverts G) > 0" and wf: "uwellformed G"
then have fin: "finite (uverts G)"
by (simp add: card_gt_0_iff)
text‹Assume that, for a yet to be determined $\delta$, we have:›
assume ineq: "real (card (triangle_set G)) ≤ δ * card (uverts G) ^ 3"
text‹Step 1: Partition: Using Szemer\'{e}di's Regularity Lemma, we get an $\epsilon/4$ partition. ›
let ?n = "card (uverts G)"
have vne: "uverts G ≠ {}"
using ‹0 < card (uverts G)› by force
then have ngt0: "?n > 0"
by (simp add: fin card_gt_0_iff)
with M0 obtain P where M: "regular_partition (ε/4) G P" and "card P ≤ M0"
by blast
define M where "M ≡ card P"
have "finite P"
by (meson M fin finite_elements regular_partition_def)
with M0 have "M > 0"
unfolding M_def
by (metis M card_gt_0_iff partition_onD1 partition_on_empty regular_partition_def vne)
let ?e4M = "ε / (4 * real M)"
define D where "D ≡ 1/6 *(1-(ε/2)) * ((ε/4)^3) * ?e4M^3"
have "D > 0"
using ‹0 < ε› ‹ε < 1› ‹M > 0› by (simp add: D_def zero_less_mult_iff)
have "D0 ≤ D"
unfolding D0_def D_def using ‹0 < ε› ‹ε < 1› ‹card P ≤ M0› ‹M > 0›
by (intro mult_mono) (auto simp: frac_le M_def)
have fin_part: "finite_graph_partition (uverts G) P M"
using M unfolding regular_partition_def finite_graph_partition_def
by (metis M_def ‹0 < M› card_gt_0_iff)
then have fin_P: "finite R" and card_P_gt0: "card R > 0" if "R∈P" for R
using fin finite_graph_partition_finite finite_graph_partition_gt0 that by auto
have card_P_le: "card R ≤ ?n" if "R∈P" for R
by (meson card_mono fin fin_part finite_graph_partition_subset that)
have P_disjnt: "⋀R S. ⟦R ≠ S; R ∈ P; S ∈ P⟧ ⟹ R ∩ S = {}"
using fin_part
by (metis disjnt_def finite_graph_partition_def insert_absorb pairwise_insert partition_on_def)
have sum_card_P: "(∑R∈P. card R) = ?n"
using card_finite_graph_partition fin fin_part by meson
text‹Step 2. Cleaning. For each ordered pair of parts $(P_i,P_j)$, remove all edges between
$P_i$ and $P_j$ if (a) it is an irregular pair, (b) its edge density ${} < \epsilon/2$,
(c) either $P_i$ or $P_j$ is small (${}\le(\epsilon/4M)n$)
Process (a) removes at most $(\epsilon/4)n^2$ edges.
Process (b) removes at most $(\epsilon/2)n^2$ edges.
Process (c) removes at most $(\epsilon/4)n^2$ edges.
The remaining graph is triangle-free for some choice of $\delta$. ›
define edge where "edge ≡ λR S. mk_uedge ` (all_edges_between R S G)"
have edge_commute: "edge R S = edge S R" for R S
by (force simp add: edge_def all_edges_between_swap [of S] split: prod.split)
have card_edge_le_card: "card (edge R S) ≤ card (all_edges_between R S G)" for R S
by (simp add: card_image_le edge_def fin finite_all_edges_between' local.wf)
have card_edge_le: "card (edge R S) ≤ card R * card S" if "R∈P" "S∈P" for R S
by (meson card_edge_le_card fin_P le_trans max_all_edges_between that)
text ‹Obtain the set of edges meeting condition (a).›
define irreg_pairs where "irreg_pairs ≡ {(R,S). R ∈ P ∧ S ∈ P ∧ ¬ (ε/4)-regular_pair R S G}"
define Ea where "Ea ≡ (⋃(R,S) ∈ irreg_pairs. edge R S)"
text ‹Obtain the set of edges meeting condition (b).›
define low_density_pairs
where "low_density_pairs ≡ {(R,S). R ∈ P ∧ S ∈ P ∧ ¬ edge_dense R S G (ε/2)}"
define Eb where "Eb ≡ (⋃(i,j) ∈ low_density_pairs. edge i j)"
text ‹Obtain the set of edges meeting condition (c).›
define small where "small ≡ λR. R ∈ P ∧ card R ≤ ?e4M * ?n"
let ?SMALL = "Collect small"
define small_pairs where "small_pairs ≡ {(R,S). R ∈ P ∧ S ∈ P ∧ (small R ∨ small S)}"
define Ec where "Ec ≡ (⋃R ∈ ?SMALL. ⋃S ∈ P. edge R S)"
have Ec_def': "Ec = (⋃(i,j) ∈ small_pairs. edge i j)"
by (force simp: edge_commute small_pairs_def small_def Ec_def)
have eabound: "card Ea ≤ (ε/4) * ?n^2"
proof -
have §: "⋀R S. ⟦R ∈ P; S ∈ P⟧ ⟹ card (edge R S) ≤ card R * card S"
unfolding edge_def
by (meson card_image_le fin_P finite_all_edges_between max_all_edges_between order_trans)
have "irreg_pairs ⊆ P × P"
by (auto simp: irreg_pairs_def)
then have "finite irreg_pairs"
by (meson ‹finite P› finite_SigmaI finite_subset)
have "card Ea ≤ (∑(R,S)∈irreg_pairs. card (edge R S))"
by (simp add: Ea_def card_UN_le [OF ‹finite irreg_pairs›] case_prod_unfold)
also have "… ≤ (∑(R,S) ∈ {(R,S). R∈P ∧ S∈P ∧ ¬ (ε/4)-regular_pair R S G}. card R * card S)"
unfolding irreg_pairs_def using § by (force intro: sum_mono)
also have "… = (∑(R,S) ∈ irregular_set (ε/4) G P. card R * card S)"
by (simp add: irregular_set_def)
finally have "card Ea ≤ (∑(R,S) ∈ irregular_set (ε/4) G P. card R * card S)" .
with M show ?thesis
unfolding regular_partition_def by linarith
qed
have ebbound: "card Eb ≤ (ε/2) * (?n^2)"
proof -
have §: "⋀R S. ⟦R ∈ P; S ∈ P; ¬ edge_dense R S G (ε / 2)⟧
⟹ real (card (edge R S)) * 2 ≤ ε * real (card R) * real (card S)"
by (simp add: divide_simps edge_dense_def edge_density_def card_P_gt0)
(smt (verit, best) card_edge_le_card of_nat_le_iff mult.assoc)
have subs: "low_density_pairs ⊆ P × P"
by (auto simp: low_density_pairs_def)
then have "finite low_density_pairs"
by (metis ‹finite P› finite_SigmaI finite_subset)
have "real (card Eb) ≤ (∑(i,j)∈low_density_pairs. real (card (edge i j)))"
unfolding Eb_def
by (smt (verit, ccfv_SIG) ‹finite low_density_pairs› card_UN_le of_nat_mono of_nat_sum
case_prod_unfold sum_mono)
also have "… ≤ (∑(R,S)∈low_density_pairs. ε/2 * card R * card S)"
unfolding low_density_pairs_def by (force intro: sum_mono §)
also have "… ≤ (∑(R,S)∈P × P. ε/2 * card R * card S)"
using subs ‹ε > 0› by (intro sum_mono2) (auto simp: ‹finite P›)
also have "… = ε/2 * (∑(R,S)∈P × P. card R * card S)"
by (simp add: sum_distrib_left case_prod_unfold mult_ac)
also have "… ≤ (ε/2) * (?n^2)"
using ‹ε>0› sum_prod_le_prod_sum
by (simp add: power2_eq_square sum_product flip: sum.cartesian_product sum_card_P)
finally show ?thesis .
qed
have ecbound: "card Ec ≤ (ε/4) * (?n^2)"
proof -
have edge_bound: "(card (edge R S)) ≤ ?e4M * ?n^2"
if "S ∈ P" "small R" for R S
proof -
have "real (card R) ≤ ε * ?n / (4 * real M)"
using that by (simp add: small_def)
with card_P_le [OF ‹S∈P›]
have *: "real (card R) * real (card S) ≤ ε * card (uverts G) / (4 * real M) * ?n"
by (meson mult_mono of_nat_0_le_iff of_nat_mono order.trans)
also have "… = ?e4M * ?n^2"
by (simp add: power2_eq_square)
finally show ?thesis
by (smt (verit) card_edge_le of_nat_mono of_nat_mult small_def that)
qed
have subs: "?SMALL ⊆ P"
by (auto simp: small_def)
then obtain card_sp: "card (?SMALL) ≤ M" and "finite ?SMALL"
using M_def ‹finite P› card_mono by (metis finite_subset)
have "real (card Ec) ≤ (∑R ∈ ?SMALL. real (card (⋃S ∈ P. edge R S)))"
unfolding Ec_def
by (smt (verit, ccfv_SIG) ‹finite ?SMALL› card_UN_le of_nat_mono of_nat_sum case_prod_unfold sum_mono)
also have "… ≤ (∑R ∈ ?SMALL. ?e4M * ?n^2)"
proof (intro sum_mono)
fix R assume i: "R ∈ Collect small"
then have "R∈P" and card_Pi: "card R ≤ ?e4M * ?n"
by (auto simp: small_def)
let ?UE = "⋃(edge R ` (P))"
have *: "real (card ?UE) ≤ real (card R * ?n)"
proof -
have "?UE ⊆ mk_uedge ` (all_edges_between R (uverts G) G)"
apply (simp add: edge_def UN_subset_iff Ball_def)
by (meson all_edges_between_mono2 fin_part finite_graph_partition_subset image_mono)
then have "card ?UE ≤ card (all_edges_between R (uverts G) G)"
by (meson card_image_le card_mono fin finite_all_edges_between' finite_imageI wf le_trans)
then show ?thesis
by (meson of_nat_mono fin fin_P max_all_edges_between order.trans ‹R∈P›)
qed
also have "… ≤ ?e4M * real (?n⇧2)"
using card_Pi ‹M > 0› ‹?n > 0› by (force simp add: divide_simps power2_eq_square)
finally show "real (card ?UE) ≤ ?e4M * real (?n⇧2)" .
qed
also have "… ≤ card ?SMALL * (?e4M * ?n^2)"
by simp
also have "… ≤ M * (?e4M * ?n^2)"
using egt by (intro mult_right_mono) (auto simp add: card_sp)
also have "… ≤ (ε/4) * (?n^2)"
using ‹M > 0› by simp
finally show ?thesis .
qed
have prev1: "card (Ea ∪ Eb ∪ Ec) ≤ card (Ea ∪ Eb) + card Ec" by (simp add: card_Un_le)
also have "… ≤ card Ea + card Eb + card Ec" by (simp add: card_Un_le)
also have prev: "… ≤ (ε/4)*(?n^2) + (ε/2)*(?n^2) + (ε/4)*(?n^2)"
using eabound ebbound ecbound by linarith
finally have cutedgesbound: "card (Ea ∪ Eb ∪ Ec) ≤ ε * (?n^2)" by simp
define Gnew where "Gnew ≡ (uverts G, uedges G - (Ea ∪ Eb ∪ Ec))"
show "∃Gnew. ?Φ G Gnew"
proof (intro exI conjI)
show verts: "uverts Gnew = uverts G" by (simp add: Gnew_def)
have diffedges: "(Ea ∪ Eb ∪ Ec) ⊆ uedges G"
by (auto simp: Ea_def Eb_def Ec_def all_edges_between_def edge_def)
then show edges: "uedges Gnew ⊆ uedges G"
by (simp add: Gnew_def)
then have "uedges G - (uedges Gnew) = uedges G ∩ (Ea ∪ Eb ∪ Ec) "
by (simp add: Gnew_def Diff_Diff_Int)
then have "uedges G - (uedges Gnew) = (Ea ∪ Eb ∪ Ec)" using diffedges
by (simp add: Int_absorb1)
then have cardbound: "card (uedges G - uedges Gnew) ≤ ε * (?n^2)"
using cutedgesbound by simp
have graph_partition_new: "finite_graph_partition (uverts Gnew) P M" using verts
by (simp add: fin_part)
have new_wf: "uwellformed Gnew" using subgraph_edge_wf verts edges wf by simp
have new_fin: "finite (uverts Gnew)" using verts fin by simp
text‹ The notes by Bell and Grodzicki are quite useful for understanding the lines below.
See pg 4 in the middle after the summary of the min edge counts.›
have irreg_pairs_swap: "(R,S) ∈ irreg_pairs ⟷ (S, R) ∈ irreg_pairs" for R S
by (auto simp: irreg_pairs_def regular_pair_commute)
have low_density_pairs_swap: "(R,S) ∈ low_density_pairs ⟷ (S,R) ∈ low_density_pairs" for R S
by (simp add: low_density_pairs_def edge_density_commute edge_dense_def)
(use all_edges_between_swap in blast)
have small_pairs_swap: "(R,S) ∈ small_pairs ⟷ (S,R) ∈ small_pairs" for R S
by (auto simp: small_pairs_def)
have all_edges_if:
"all_edges_between R S Gnew
= (if (R,S) ∈ irreg_pairs ∪ low_density_pairs ∪ small_pairs then {}
else all_edges_between R S G)"
(is "?lhs = ?rhs")
if ij: "R ∈ P" "S ∈ P" for R S
proof
show "?lhs ⊆ ?rhs"
using that fin_part unfolding Gnew_def Ea_def Eb_def Ec_def'
apply (simp add: all_edges_between_E_diff all_edges_between_E_Un all_edges_between_E_UN)
apply (auto simp: edge_def in_mk_uedge_img_iff all_edges_between_def)
done
next
have Ea: "all_edges_between R S (V, Ea) = {}"
if "(R,S) ∉ irreg_pairs" for V
using ij that P_disjnt
by (auto simp: Ea_def doubleton_eq_iff edge_def all_edges_between_def irreg_pairs_def;
metis regular_pair_commute disjoint_iff_not_equal)
have Eb: "all_edges_between R S (V, Eb) = {}"
if "(R,S) ∉ low_density_pairs" for V
using ij that
apply (auto simp: Eb_def edge_def all_edges_between_def low_density_pairs_def edge_dense_def)
apply metis
by (metis IntI P_disjnt doubleton_eq_iff edge_density_commute equals0D)
have Ec: "all_edges_between R S (V, Ec) = {}"
if "(R,S) ∉ small_pairs" for V
using ij that
by (auto simp: Ec_def' doubleton_eq_iff edge_def all_edges_between_def small_pairs_def;
metis P_disjnt disjoint_iff)
show "?rhs ⊆ ?lhs"
by (auto simp add: Gnew_def Ea Eb Ec all_edges_between_E_diff all_edges_between_E_Un)
qed
have rp: "(ε/4)-regular_pair R S Gnew" if ij: "R ∈ P" "S ∈ P" for R S
proof (cases "(R,S) ∈ irreg_pairs")
case False
have ed: "edge_density X Y Gnew =
(if (R,S) ∈ irreg_pairs ∪ low_density_pairs ∪ small_pairs then 0
else edge_density X Y G)"
if "X ⊆ R" "Y ⊆ S" for X Y
using all_edges_if that ij False
by (smt (verit) all_edges_preserved edge_density_eq0 edge_density_def)
show ?thesis
using that False ‹ε > 0›
by (auto simp add: irreg_pairs_def regular_pair_def less_le ed)
next
case True
then have ed: "edge_density X Y Gnew = 0" if "X ⊆ R" "Y ⊆ S" for X Y
by (meson edge_density_eq0 all_edges_if that ‹R ∈ P› ‹S ∈ P› UnCI)
with egt that show ?thesis
by (auto simp: regular_pair_def ed)
qed
then have reg_pairs: "(ε/4)-regular_graph P Gnew"
by (meson regular_graph_def)
have "edge_dense R S Gnew (ε/2)"
if "R ∈ P" "S ∈ P" for R S
proof (cases "(R,S) ∈ low_density_pairs")
case False
have ed: "edge_density R S Gnew =
(if (R,S) ∈ irreg_pairs ∪ low_density_pairs ∪ small_pairs then 0
else edge_density R S G)"
using all_edges_if that that by (simp add: edge_density_def)
with that ‹ε > 0› False show ?thesis
by (auto simp: low_density_pairs_def edge_dense_def all_edges_if)
next
case True
then have "edge_density R S Gnew = 0"
by (simp add: all_edges_if edge_density_def that)
with ‹ε > 0› that show ?thesis
by (simp add: True all_edges_if edge_dense_def)
qed
then have density_bound: "dense_graph P Gnew (ε/2)"
by (meson dense_graph_def)
have min_subset_size: "decent_graph P Gnew (?e4M * ?n)"
using ‹ε > 0›
by (auto simp: decent_graph_def small_pairs_def small_def decent_def all_edges_if)
show "triangle_free_graph Gnew"
proof (rule ccontr)
assume non: "¬?thesis"
then obtain x y z where trig_ex: "triangle_in_graph x y z Gnew"
using triangle_free_graph_def non by auto
then have xin: "x ∈ (uverts Gnew)" and yin: "y ∈ (uverts Gnew)" and zin: "z ∈ (uverts Gnew)"
using triangle_in_graph_verts new_wf by auto
then obtain R S T where xinp: "x ∈ R" and ilt: "R∈P" and yinp: "y ∈ S" and jlt: "S∈P"
and zinp: "z ∈ T" and klt: "T∈P"
by (metis graph_partition_new xin Union_iff finite_graph_partition_equals)
then have finitesubsets: "finite R" "finite S" "finite T"
using new_fin fin_part finite_graph_partition_finite fin by auto
have subsets: "R ⊆ uverts Gnew" "S ⊆ uverts Gnew" "T ⊆ uverts Gnew"
using finite_graph_partition_subset ilt jlt klt graph_partition_new by auto
have min_sizes: "card R ≥ ?e4M*?n" "card S ≥ ?e4M*?n" "card T ≥ ?e4M*?n"
using trig_ex min_subset_size xinp yinp zinp ilt jlt klt
by (auto simp: triangle_in_graph_def decent_graph_def decent_def all_edges_between_def)
have min_dens: "edge_density R S Gnew ≥ ε/2" "edge_density R T Gnew ≥ ε/2" "edge_density S T Gnew ≥ ε/2"
using density_bound ilt jlt klt xinp yinp zinp trig_ex
by (auto simp: dense_graph_def edge_dense_def all_edges_between_def triangle_in_graph_def)
then have min_dens_diff:
"edge_density R S Gnew - ε/4 ≥ ε/4" "edge_density R T Gnew - ε/4 ≥ ε/4" "edge_density S T Gnew - ε/4 ≥ ε/4"
by auto
have mincard0: "(card R) * (card S) * (card T) ≥ 0" by simp
have gtcube: "((edge_density R S Gnew) - ε/4)*((edge_density R T Gnew) - ε/4) *((edge_density S T Gnew) - ε/4) ≥ (ε/4)^3"
using min_dens_diff e4gt real_mult_gt_cube by auto
then have c1: "((edge_density R S Gnew) - ε/4)*((edge_density R T Gnew) - ε/4) *((edge_density S T Gnew) - ε/4) ≥ 0"
by (smt (verit) e4gt zero_less_power)
have "?e4M * ?n ≥ 0"
using egt by force
then have "card R * card S * card T ≥ (?e4M * ?n)^3"
by (metis min_sizes of_nat_mult real_mult_gt_cube)
then have cardgtbound:"card R * card S * card T ≥ ?e4M^ 3 * ?n^3"
by (metis of_nat_power power_mult_distrib)
have "(1-ε/2) * (ε/4)^3 * (ε/(4*M))^3 * ?n^3 ≤ (1-ε/2) * (ε/4)^3 * card R * card S * card T"
using cardgtbound ordered_comm_semiring_class.comm_mult_left_mono True e4gt by fastforce
also have "... ≤ (1-2*(ε/4)) * (edge_density R S Gnew - ε/4) * (edge_density R T Gnew - ε/4)
* (edge_density S T Gnew - ε/4) * card R * card S * card T"
using gtcube c1 ‹ε < 1› mincard0 by (simp add: mult.commute mult.left_commute mult_left_mono)
also have "... ≤ card (triangle_triples R S T Gnew)"
by (smt (verit, best) e4gt ilt jlt klt min_dens_diff new_fin new_wf rp subsets triangle_counting_lemma)
finally have "card (triangle_set Gnew) ≥ D * ?n^3"
using card_convert_triangle_rep_bound new_wf new_fin subsets
by (auto simp: triangle_triples_def D_def)
then have g_tset_bound: "card (triangle_set G) ≥ D * ?n^3"
using triangle_set_graph_edge_ss_bound by (smt (verit) edges fin local.wf of_nat_mono verts)
have "card (triangle_set G) > δ * ?n^3"
proof -
have "?n^3 > 0"
by (simp add: ‹uverts G ≠ {}› card_gt_0_iff fin)
with δ ‹D0 ≤ D› have "D * ?n^3 > δ * ?n^3"
by force
thus "card (triangle_set G) > δ * ?n ^3"
using g_tset_bound unfolding D_def by linarith
qed
thus False
using ineq by linarith
qed
show "real (card (uedges G - uedges Gnew)) ≤ ε * real ((card (uverts G))⇧2)"
using cardbound edges verts by blast
qed
qed (rule ‹0 < δ›)
qed
subsection ‹Roth's Theorem›
text‹We will first need the following corollary of the Triangle Removal Lemma.›
text ‹See 🌐‹https://en.wikipedia.org/wiki/Ruzsa--Szemerédi_problem›.
Suggested by Yaël Dillies
›
corollary Diamond_free:
fixes ε :: real
assumes "0 < ε"
shows "∃N>0. ∀G. card(uverts G) > N ⟶ uwellformed G ⟶ unique_triangles G ⟶
card (uedges G) ≤ ε * (card (uverts G))⇧2"
proof -
have "ε/3 > 0"
using assms by auto
then obtain δ::real where "δ > 0"
and δ: "⋀G. ⟦card(uverts G) > 0; uwellformed G; card (triangle_set G) ≤ δ * card(uverts G) ^ 3⟧
⟹ ∃G'. triangle_free_graph G' ∧ uverts G' = uverts G ∧ (uedges G' ⊆ uedges G) ∧
card (uedges G - uedges G') ≤ ε/3 * (card (uverts G))⇧2"
using triangle_removal_lemma by metis
obtain N::nat where N: "real N ≥ 1 / (3*δ)"
by (meson real_arch_simple)
show ?thesis
proof (intro exI conjI strip)
show "N > 0"
using N ‹0 < δ› zero_less_iff_neq_zero by fastforce
fix G
let ?n = "card (uverts G)"
assume G_gt_N: "N < ?n"
and wf: "uwellformed G"
and uniq: "unique_triangles G"
have G_ne: "?n > 0"
using G_gt_N by linarith
let ?TWO = "(λt. [t]⇗2⇖)"
have tri_nsets_2: "[{x,y,z}]⇗2⇖ = {{x,y},{y,z},{x,z}}" if "triangle_in_graph x y z G" for x y z
using that unfolding nsets_def triangle_in_graph_def card_2_iff doubleton_eq_iff
by (blast dest!: edge_vertices_not_equal [OF wf])
have tri_nsets_3: "{{x,y},{y,z},{x,z}} ∈ [uedges G]⇗3⇖" if "triangle_in_graph x y z G" for x y z
using that by (simp add: nsets_def card_3_iff triangle_in_graph_def)
(metis doubleton_eq_iff edge_vertices_not_equal [OF wf])
have sub: "?TWO ` triangle_set G ⊆ [uedges G]⇗3⇖"
using tri_nsets_2 tri_nsets_3 triangle_set_def by auto
have "⋀i. i ∈ triangle_set G ⟹ ?TWO i ≠ {}"
using tri_nsets_2 triangle_set_def by auto
moreover have dfam: "disjoint_family_on ?TWO (triangle_set G)"
using sub [unfolded image_subset_iff] uniq
unfolding disjoint_family_on_def triangle_set_def nsets_def unique_triangles_def
by (smt (verit) disjoint_iff_not_equal insert_subset mem_Collect_eq mk_disjoint_insert )
ultimately have inj: "inj_on ?TWO (triangle_set G)"
by (simp add: disjoint_family_on_iff_disjoint_image)
have §: "∃T∈triangle_set G. e ∈ [T]⇗2⇖" if "e ∈ uedges G" for e
using uniq [unfolded unique_triangles_def] that local.wf
apply (simp add: triangle_set_def triangle_in_graph_def nsets_def uwellformed_def)
by (metis (mono_tags, lifting) finite.emptyI finite.insertI finite_subset)
with sub have "⋃(?TWO ` triangle_set G) = uedges G"
by (auto simp: image_subset_iff nsets_def)
then have "card (⋃(?TWO ` triangle_set G)) = card (uedges G)"
by simp
moreover have "card (⋃(?TWO ` triangle_set G)) = 3 * card (triangle_set G)"
proof (subst card_UN_disjoint' [OF dfam])
show "finite ([i]⇗2⇖)" if "i ∈ triangle_set G" for i
using that tri_nsets_2 triangle_set_def by fastforce
show "finite (triangle_set G)"
by (meson G_ne card_gt_0_iff local.wf finite_triangle_set)
have "card ([i]⇗2⇖) = 3" if "i ∈ triangle_set G" for i
using that wf tri_nsets_2 tri_nsets_3 by (force simp add: nsets_def triangle_set_def)
then show "(∑i∈triangle_set G. card ([i]⇗2⇖)) = 3 * card (triangle_set G)"
by simp
qed
ultimately have 3: "3 * card (triangle_set G) = card (uedges G)"
by auto
have "card (uedges G) ≤ card (all_edges(uverts G))"
by (meson G_ne all_edges_finite card_gt_0_iff card_mono local.wf wellformed_all_edges)
also have "… = ?n choose 2"
by (metis G_ne card_all_edges card_eq_0_iff not_less0)
also have "… ≤ ?n⇧2"
by (metis binomial_eq_0_iff binomial_le_pow linorder_not_le zero_le)
finally have "card (uedges G) ≤ ?n⇧2" .
with 3 have "card (triangle_set G) ≤ ?n⇧2 / 3" by linarith
also have "… ≤ δ * ?n ^ 3"
proof -
have "1 ≤ 3 * δ * N"
using N ‹δ > 0› by (simp add: field_simps)
also have "… ≤ 3 * δ * ?n"
using G_gt_N ‹0 < δ› by force
finally have "1 * ?n^2 ≤ (3 * δ * ?n) * ?n^2"
by (simp add: G_ne)
then show ?thesis
by (simp add: eval_nat_numeral mult_ac)
qed
finally have "card (triangle_set G) ≤ δ * ?n ^ 3" .
then obtain Gnew where Gnew: "triangle_free_graph Gnew" "uverts Gnew = uverts G"
"uedges Gnew ⊆ uedges G" and card_edge_diff: "card (uedges G - uedges Gnew) ≤ ε/3 * ?n⇧2"
using G_ne δ local.wf by meson
text‹Deleting an edge removes at most one triangle from the graph by assumption,
so the number of edges removed in this process is at least the number of triangles.›
obtain TF where TF: "⋀e. e ∈ uedges G ⟹ ∃x y z. TF e = {x,y,z} ∧ triangle_in_graph x y z G ∧ e ⊆ TF e"
using uniq unfolding unique_triangles_def by metis
have False
if non: "⋀e. e ∈ uedges G - uedges Gnew ⟹ {x,y,z} ≠ TF e"
and tri: "triangle_in_graph x y z G" for x y z
proof -
have "¬ triangle_in_graph x y z Gnew"
using Gnew triangle_free_graph_def by blast
with tri obtain e where eG: "e ∈ uedges G - uedges Gnew" and esub: "e ⊆ {x,y,z}"
using insert_commute triangle_in_graph_def by auto
then show False
by (metis DiffD1 TF tri uniq unique_triangles_def non [OF eG])
qed
then have "triangle_set G ⊆ TF ` (uedges G - uedges Gnew)"
unfolding triangle_set_def by blast
moreover have "finite (uedges G - uedges Gnew)"
by (meson G_ne card_gt_0_iff finite_Diff finite_graph_def wf wellformed_finite)
ultimately have "card (triangle_set G) ≤ card (uedges G - uedges Gnew)"
by (meson surj_card_le)
then show "card (uedges G) ≤ ε * ?n⇧2"
using 3 card_edge_diff by linarith
qed
qed
text‹We are now ready to proceed to the proof of Roth's Theorem for Arithmetic Progressions. ›
definition progression3 :: "'a::comm_monoid_add ⇒ 'a ⇒ 'a set"
where "progression3 k d ≡ {k, k+d, k+d+d}"
lemma p3_int_iff: "progression3 (int k) (int d) ⊆ int ` A ⟷ progression3 k d ⊆ A"
apply (simp add: progression3_def image_iff)
by (smt (verit, best) int_plus of_nat_eq_iff)
text‹We assume that a set of naturals $A \subseteq \{...<N \}$ does not have any arithmetic progression.
We will then show that @{term A} is of cardinality $o(N)$.›
lemma RothArithmeticProgressions_aux:
fixes ε::real
assumes "ε > 0"
obtains M where "∀N ≥ M. ∀A ⊆ {..<N}. (∄k d. d>0 ∧ progression3 k d ⊆ A) ⟶ card A < ε * real N"
proof -
obtain L where "L>0"
and L: "⋀G. ⟦card(uverts G) > L; uwellformed G; unique_triangles G⟧
⟹ card (uedges G) ≤ ε/12 * (card (uverts G))⇧2"
by (metis assms Diamond_free less_divide_eq_numeral1(1) mult_eq_0_iff)
show thesis
proof (intro strip that)
fix N A
assume "L ≤ N" and A: "A ⊆ {..<N}"
and non: "∄k d. 0 < d ∧ progression3 k d ⊆ A"
then have "N > 0" using ‹0 < L› by linarith
define M where "M ≡ Suc (2*N)"
have M_mod_bound[simp]: "x mod M < M" for x
by (simp add: M_def)
have "odd M" "M>0" "N<M" by (auto simp: M_def)
have "coprime M (Suc N)"
unfolding M_def
by (metis add_2_eq_Suc coprime_Suc_right_nat coprime_mult_right_iff mult_Suc_right)
then have cop: "coprime M (1 + int N)"
by (metis coprime_int_iff of_nat_Suc)
have A_sub_M: "int ` A ⊆ {..<M}"
using A by (force simp: M_def)
have non_img_A: "∄k d. d > 0 ∧ progression3 k d ⊆ int ` A"
by (metis imageE insert_subset non p3_int_iff pos_int_cases progression3_def)
text‹Construct a tripartite graph @{term G} whose three parts are copies of @{text"ℤ/Mℤ"}.›
define part_of where "part_of ≡ λξ. (λi. prod_encode (ξ,i)) ` {..<M}"
define label_of_part where "label_of_part ≡ λp. fst (prod_decode p)"
define from_part where "from_part ≡ λp. snd (prod_decode p)"
have enc_iff [simp]: "prod_encode (a,i) ∈ part_of a' ⟷ a'=a ∧ i<M" for a a' i
using ‹0 < M› by (clarsimp simp: part_of_def image_iff Bex_def) presburger
have part_of_M: "p ∈ part_of a ⟹ from_part p < M" for a p
using from_part_def part_of_def by fastforce
have disjnt_part_of: "a ≠ b ⟹ disjnt (part_of a) (part_of b)" for a b
by (auto simp: part_of_def disjnt_iff)
have from_enc [simp]: "from_part (prod_encode (a,i)) = i" for a i
by (simp add: from_part_def)
have finpart [iff]: "finite (part_of a)" for a
by (simp add: part_of_def ‹0 < M›)
have cardpart [simp]: "card (part_of a) = M" for a
using ‹0 < M›
by (simp add: part_of_def eq_nat_nat_iff inj_on_def card_image)
let ?X = "part_of 0"
let ?Y = "part_of (Suc 0)"
let ?Z = "part_of (Suc (Suc 0))"
define diff where "diff ≡ λa b. (int a - int b) mod (int M)"
have inj_on_diff: "inj_on (λx. diff x a) {..<M}" for a
apply (clarsimp simp: diff_def inj_on_def)
by (metis diff_add_cancel mod_add_left_eq mod_less nat_int of_nat_mod)
have eq_mod_M: "(x - y) mod int M = (x' - y) mod int M ⟹ x mod int M = x' mod int M" for x x' y
by (simp add: mod_eq_dvd_iff)
have diff_invert: "diff y x = int a ⟷ y = (x + a) mod M" if "y < M" "a∈A" for x y a
proof -
have "a < M"
using A ‹N < M› that by auto
show ?thesis
proof
assume "diff y x = int a"
with that ‹a<M› have "int y = int (x+a) mod int M"
by (smt (verit) diff_def eq_mod_M mod_less of_nat_add zmod_int)
with that show "y = (x + a) mod M"
by (metis nat_int zmod_int)
qed (simp add: ‹a < M› diff_def mod_diff_left_eq zmod_int)
qed
define diff2 where "diff2 ≡ λa b. ((int a - int b) * int(Suc N)) mod (int M)"
have inj_on_diff2: "inj_on (λx. diff2 x a) {..<M}" for a
apply (clarsimp simp: diff2_def inj_on_def)
by (metis eq_mod_M mult_mod_cancel_right [OF _ cop] int_int_eq mod_less zmod_int)
have [simp]: "(1 + int N) mod int M = 1 + int N"
using M_def ‹0 < N› by auto
have diff2_by2: "(diff2 a b * 2) mod M = diff a b" for a b
proof -
have "int M dvd ((int a - int b) * int M)"
by simp
then have "int M dvd ((int a - int b) * int (Suc N) * 2 - (int a - int b))"
by (auto simp: M_def algebra_simps)
then show ?thesis
by (metis diff2_def diff_def mod_eq_dvd_iff mod_mult_left_eq)
qed
have diff2_invert: "diff2 (((x + a) mod M + a) mod M) x = int a" if "a∈A" for x a
proof -
have 1: "((x + a) mod M + a) mod M = (x + 2*a) mod M"
by (metis group_cancel.add1 mod_add_left_eq mult_2)
have "(int ((x + 2*a) mod M) - int x) * (1 + int N) mod int M
= (int (x + 2*a) - int x) * (1 + int N) mod int M"
by (metis mod_diff_left_eq mod_mult_cong of_nat_mod)
also have "… = int (a * (Suc M)) mod int M"
by (simp add: algebra_simps M_def)
also have "… = int a mod int M"
by simp
also have "… = int a"
using A M_def subsetD that by auto
finally show ?thesis
using that by (auto simp: 1 diff2_def)
qed
define Edges where "Edges ≡ λX Y df. {{x,y}| x y. x ∈ X ∧ y ∈ Y ∧ df(from_part y) (from_part x) ∈ int ` A}"
have Edges_subset: "Edges X Y df ⊆ Pow (X ∪ Y)" for X Y df
by (auto simp: Edges_def)
define XY where "XY ≡ Edges ?X ?Y diff"
define YZ where "YZ ≡ Edges ?Y ?Z diff"
define XZ where "XZ ≡ Edges ?X ?Z diff2"
obtain [simp]: "finite XY" "finite YZ" "finite XZ"
using Edges_subset unfolding XY_def YZ_def XZ_def
by (metis finite_Pow_iff finite_UnI finite_subset finpart)
define G where "G ≡ (?X ∪ ?Y ∪ ?Z, XY ∪ YZ ∪ XZ)"
have finG: "finite (uverts G)" and cardG: "card (uverts G) = 3*M"
by (simp_all add: G_def card_Un_disjnt disjnt_part_of)
then have "card(uverts G) > L"
using M_def ‹L ≤ N› by linarith
have "uwellformed G"
by (fastforce simp: card_insert_if part_of_def G_def XY_def YZ_def XZ_def Edges_def uwellformed_def)
have [simp]: "{prod_encode (ξ,x), prod_encode (ξ,y)} ∉ XY"
"{prod_encode (ξ,x), prod_encode (ξ,y)} ∉ YZ"
"{prod_encode (ξ,x), prod_encode (ξ,y)} ∉ XZ" for x y ξ
by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff)
have label_ne_XY [simp]: "label_of_part p ≠ label_of_part q" if "{p,q} ∈ XY" for p q
using that by (auto simp add: XY_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
then have [simp]: "{p} ∉ XY" for p
by (metis insert_absorb2)
have label_ne_YZ [simp]: "label_of_part p ≠ label_of_part q" if "{p,q} ∈ YZ" for p q
using that by (auto simp add: YZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
then have [simp]: "{p} ∉ YZ" for p
by (metis insert_absorb2)
have label_ne_XZ [simp]: "label_of_part p ≠ label_of_part q" if "{p,q} ∈ XZ" for p q
using that by (auto simp add: XZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def)
then have [simp]: "{p} ∉ XZ" for p
by (metis insert_absorb2)
have label012: "label_of_part v < 3" if "v ∈ uverts G" for v
using that by (auto simp add: G_def eval_nat_numeral part_of_def label_of_part_def)
have Edges_distinct: "⋀p q r ξ ζ γ β df df'. ⟦{p,q} ∈ Edges (part_of ξ) (part_of ζ) df;
{q,r} ∈ Edges (part_of ξ) (part_of ζ) df;
{p,r} ∈ Edges (part_of γ) (part_of β) df'; ξ ≠ ζ; γ ≠ β⟧ ⟹ False"
apply (auto simp: disjnt_iff Edges_def doubleton_eq_iff conj_disj_distribR ex_disj_distrib)
apply (metis disjnt_iff disjnt_part_of)+
done
have uniq: "∃i<M. ∃d∈A. ∃x ∈ {p,q,r}. ∃y ∈ {p,q,r}. ∃z ∈ {p,q,r}.
x = prod_encode(0, i)
∧ y = prod_encode(1, (i+d) mod M)
∧ z = prod_encode(2, (i+d+d) mod M)"
if T: "triangle_in_graph p q r G" for p q r
proof -
obtain x y z where xy: "{x,y} ∈ XY" and yz: "{y,z} ∈ YZ" and xz: "{x,z} ∈ XZ"
and x: "x ∈ {p,q,r}" and y: "y ∈ {p,q,r}" and z: "z ∈ {p,q,r}"
using T apply (simp add: triangle_in_graph_def G_def XY_def YZ_def XZ_def)
by (smt (verit, ccfv_SIG) Edges_distinct Zero_not_Suc insert_commute n_not_Suc_n)
then have "x ∈ ?X" "y ∈ ?Y" "z ∈ ?Z"
by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff; metis disjnt_iff disjnt_part_of)+
then obtain i j k where i: "x = prod_encode(0,i)" and j: "y = prod_encode(1,j)"
and k: "z = prod_encode(2,k)"
by (metis One_nat_def Suc_1 enc_iff prod_decode_aux.cases prod_decode_inverse)
obtain a1 where "a1 ∈ A" and a1: "(int j - int i) mod int M = int a1"
using xy ‹x ∈ ?X› i j by (auto simp add: XY_def Edges_def doubleton_eq_iff diff_def)
obtain a3 where "a3 ∈ A" and a3: "(int k - int j) mod int M = int a3"
using yz ‹x ∈ ?X› j k by (auto simp add: YZ_def Edges_def doubleton_eq_iff diff_def)
obtain a2 where "a2 ∈ A" and a2: "(int k - int i) mod int M = int (a2 * 2) mod int M"
using xz ‹x ∈ ?X› i k apply (auto simp add: XZ_def Edges_def doubleton_eq_iff)
by (metis diff2_by2 diff_def int_plus mult_2_right)
obtain "a1<N" "a2<N" "a3<N"
using A ‹a1 ∈ A› ‹a2 ∈ A› ‹a3 ∈ A› by blast
then obtain "a1+a3 < M" "a2 * 2 < M"
by (simp add: M_def)
then have "int (a2 * 2) = int (a2 * 2) mod M"
by force
also have "… = int (a1 + a3) mod int M"
using a1 a2 a3 by (smt (verit, del_insts) int_plus mod_add_eq)
also have "… = int (a1+a3)"
using ‹a1 + a3 < M› by force
finally have "a2*2 = a1+a3"
by presburger
then obtain equal: "a3 - a2 = a2 - a1" "a2 - a3 = a1 - a2"
by (metis Nat.diff_cancel diff_cancel2 mult_2_right)
with ‹a1 ∈ A› ‹a2 ∈ A› ‹a3 ∈ A› have "progression3 a1 (a2 - a1) ⊆ A"
apply (clarsimp simp: progression3_def)
by (metis diff_is_0_eq' le_add_diff_inverse nle_le)
with non equal have "a2 = a1"
unfolding progression3_def
by (metis ‹a2 ∈ A› ‹a3 ∈ A› add.right_neutral diff_is_0_eq insert_subset
le_add_diff_inverse not_gr_zero)
then have "a3 = a2"
using ‹a2 * 2 = a1 + a3› by force
have k_minus_j: "(int k - int j) mod int M = int a1"
by (simp add: ‹a2 = a1› ‹a3 = a2› a3)
have i_to_j: "j mod M = (i+a1) mod M"
by (metis a1 add_diff_cancel_left' add_diff_eq mod_add_right_eq nat_int of_nat_add of_nat_mod)
have j_to_k: "k mod M = (j+a1) mod M"
by (metis ‹a2 = a1› ‹a3 = a2› a3 add_diff_cancel_left' add_diff_eq mod_add_right_eq
nat_int of_nat_add of_nat_mod)
have "i<M"
using ‹x ∈ ?X› i by simp
then show ?thesis
using i j k x y z ‹a1 ∈ A›
by (metis ‹y ∈ ?Y› ‹z ∈?Z› enc_iff i_to_j j_to_k mod_add_left_eq mod_less)
qed
text‹Every edge of the graph G lies in exactly one triangle.›
have "unique_triangles G"
unfolding unique_triangles_def
proof (intro strip)
fix e
assume "e ∈ uedges G"
then consider "e ∈ XY" | "e ∈ YZ" | "e ∈ XZ"
using G_def by fastforce
then show "∃!T. ∃x y z. T = {x, y, z} ∧ triangle_in_graph x y z G ∧ e ⊆ T"
proof cases
case 1
then obtain i j a where eeq: "e = {prod_encode(0,i), prod_encode(1,j)}"
and "i<M" and "j<M"
and df: "diff j i = int a" and "a ∈ A"
by (auto simp: XY_def Edges_def part_of_def)
let ?x = "prod_encode (0, i)"
let ?y = "prod_encode (1, j)"
let ?z = "prod_encode (2, (j+a) mod M)"
have yeq: "j = (i+a) mod M"
using diff_invert using ‹a ∈ A› df ‹j<M› by blast
with ‹a ∈ A› ‹j<M› have "{?y,?z} ∈ YZ"
by (fastforce simp: YZ_def Edges_def image_iff diff_invert)
moreover have "{?x,?z} ∈ XZ"
using ‹a ∈ A› by (fastforce simp: XZ_def Edges_def yeq diff2_invert ‹i<M›)
ultimately have T: "triangle_in_graph ?x ?y ?z G"
using ‹e ∈ uedges G› by (force simp add: G_def eeq triangle_in_graph_def)
show ?thesis
proof (intro ex1I)
show "∃x y z. {?x,?y,?z} = {x, y, z} ∧ triangle_in_graph x y z G ∧ e ⊆ {?x,?y,?z}"
using T eeq by blast
fix T
assume "∃p q r. T = {p, q, r} ∧ triangle_in_graph p q r G ∧ e ⊆ T"
then obtain p q r where Teq: "T = {p,q,r}"
and tri: "triangle_in_graph p q r G" and "e ⊆ T"
by blast
with uniq
obtain i' a' x y z where "i'<M" "a' ∈ A"
and x: "x ∈ {p,q,r}" and y: "y ∈ {p,q,r}" and z: "z ∈ {p,q,r}"
and xeq: "x = prod_encode(0, i')"
and yeq: "y = prod_encode(1, (i'+a') mod M)"
and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
by metis
then have sets_eq: "{x,y,z} = {p,q,r}" by auto
with Teq ‹e ⊆ T› have esub': "e ⊆ {x,y,z}" by blast
have "a' < M"
using A ‹N < M› ‹a' ∈ A› by auto
obtain "?x ∈ e" "?y ∈ e" using eeq by force
then have "x = ?x"
using esub' eeq yeq zeq by simp
then have "y = ?y"
using esub' eeq zeq by simp
obtain eq': "i' = i" "(i'+a') mod M = j"
using ‹x = ?x› xeq using ‹y =?y› yeq by auto
then have "diff (i'+a') i' = int a'"
by (simp add: diff_def ‹a' < M›)
then have "a' = a"
by (metis eq' df diff_def mod_diff_left_eq nat_int zmod_int)
then have "z = ?z"
by (metis ‹y = ?y› mod_add_left_eq prod_encode_eq snd_conv yeq zeq)
then show "T = {?x,?y,?z}"
using Teq ‹x = ?x› ‹y = ?y› sets_eq by presburger
qed
next
case 2
then obtain j k a where eeq: "e = {prod_encode(1,j), prod_encode(2,k)}"
and "j<M" "k<M"
and df: "diff k j = int a" and "a ∈ A"
by (auto simp: YZ_def Edges_def part_of_def numeral_2_eq_2)
let ?x = "prod_encode (0, (M+j-a) mod M)"
let ?y = "prod_encode (1, j)"
let ?z = "prod_encode (2, k)"
have zeq: "k = (j+a) mod M"
using diff_invert using ‹a ∈ A› df ‹k<M› by blast
with ‹a ∈ A› ‹k<M› have "{?x,?z} ∈ XZ"
unfolding XZ_def Edges_def image_iff
apply (clarsimp simp: mod_add_left_eq doubleton_eq_iff conj_disj_distribR ex_disj_distrib)
apply (smt (verit, ccfv_threshold) A ‹N < M› diff2_invert le_add_diff_inverse2 lessThan_iff
linorder_not_less mod_add_left_eq mod_add_self1 not_add_less1 order.strict_trans subsetD)
done
moreover
have "a < N" using A ‹a ∈ A› by blast
with ‹N < M› have "((M + j - a) mod M + a) mod M = j mod M"
by (simp add: mod_add_left_eq)
then have "{?x,?y} ∈ XY"
using ‹a ∈ A› ‹j<M› unfolding XY_def Edges_def
by (force simp add: zeq image_iff diff_invert doubleton_eq_iff ex_disj_distrib)
ultimately have T: "triangle_in_graph ?x ?y ?z G"
using ‹e ∈ uedges G› by (auto simp: G_def eeq triangle_in_graph_def)
show ?thesis
proof (intro ex1I)
show "∃x y z. {?x,?y,?z} = {x, y, z} ∧ triangle_in_graph x y z G ∧ e ⊆ {?x,?y,?z}"
using T eeq by blast
fix T
assume "∃p q r. T = {p, q, r} ∧ triangle_in_graph p q r G ∧ e ⊆ T"
then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e ⊆ T"
by blast
with uniq
obtain i' a' x y z where "i'<M" "a' ∈ A"
and x: "x ∈ {p,q,r}" and y: "y ∈ {p,q,r}" and z: "z ∈ {p,q,r}"
and xeq: "x = prod_encode(0, i')"
and yeq: "y = prod_encode(1, (i'+a') mod M)"
and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
by metis
then have sets_eq: "{x,y,z} = {p,q,r}" by auto
with Teq ‹e ⊆ T› have esub': "e ⊆ {x,y,z}" by blast
have "a' < M"
using A ‹N < M› ‹a' ∈ A› by auto
obtain "?y ∈ e" "?z ∈ e"
using eeq by force
then have "y = ?y"
using esub' eeq xeq zeq by simp
then have "z = ?z"
using esub' eeq xeq by simp
obtain eq': "(i'+a') mod M = j" "(i'+a'+a') mod M = k"
using ‹y = ?y› yeq using ‹z =?z› zeq by auto
then have "diff (i'+a'+a') (i'+a') = int a'"
by (simp add: diff_def ‹a' < M›)
then have "a' = a"
by (metis M_mod_bound ‹a' ∈ A› df diff_invert eq' mod_add_eq mod_if of_nat_eq_iff)
have "(M + ((i'+a') mod M) - a') mod M = (M + (i' + a') - a') mod M"
by (metis Nat.add_diff_assoc2 ‹a' < M› less_imp_le_nat mod_add_right_eq)
with ‹i' < M› have "(M + ((i'+a') mod M) - a') mod M = i'"
by force
with ‹a' = a› eq' have "(M + j - a) mod M = i'"
by force
with xeq have "x = ?x" by blast
then show "T = {?x,?y,?z}"
using Teq ‹z = ?z› ‹y = ?y› sets_eq by presburger
qed
next
case 3
then obtain i k a where eeq: "e = {prod_encode(0,i), prod_encode(2,k)}"
and "i<M" and "k<M"
and df: "diff2 k i = int a" and "a ∈ A"
by (auto simp: XZ_def Edges_def part_of_def eval_nat_numeral)
let ?x = "prod_encode (0, i)"
let ?y = "prod_encode (1, (i+a) mod M)"
let ?z = "prod_encode (2, k)"
have keq: "k = (i+a+a) mod M"
using diff2_invert [OF ‹a ∈ A›, of i] df ‹k<M› using inj_on_diff2 [of i]
by (simp add: inj_on_def Ball_def mod_add_left_eq)
with ‹a ∈ A› have "{?x,?y} ∈ XY"
using ‹a ∈ A› ‹i<M› ‹k<M› apply (auto simp: XY_def Edges_def)
by (metis M_mod_bound diff_invert enc_iff from_enc imageI)
moreover have "{?y,?z} ∈ YZ"
apply (auto simp: YZ_def Edges_def image_iff eval_nat_numeral)
by (metis M_mod_bound ‹a ∈ A› diff_invert enc_iff from_enc mod_add_left_eq keq)
ultimately have T: "triangle_in_graph ?x ?y ?z G"
using ‹e ∈ uedges G› by (force simp add: G_def eeq triangle_in_graph_def)
show ?thesis
proof (intro ex1I)
show "∃x y z. {?x,?y,?z} = {x, y, z} ∧ triangle_in_graph x y z G ∧ e ⊆ {?x,?y,?z}"
using T eeq by blast
fix T
assume "∃p q r. T = {p, q, r} ∧ triangle_in_graph p q r G ∧ e ⊆ T"
then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e ⊆ T"
by blast
with uniq obtain i' a' x y z where "i'<M" "a' ∈ A"
and x: "x ∈ {p,q,r}" and y: "y ∈ {p,q,r}" and z: "z ∈ {p,q,r}"
and xeq: "x = prod_encode(0, i')"
and yeq: "y = prod_encode(1, (i'+a') mod M)"
and zeq: "z = prod_encode(2, (i'+a'+a') mod M)"
by metis
then have sets_eq: "{x,y,z} = {p,q,r}" by auto
with Teq ‹e ⊆ T› have esub': "e ⊆ {x,y,z}" by blast
have "a' < M"
using A ‹N < M› ‹a' ∈ A› by auto
obtain "?x ∈ e" "?z ∈ e" using eeq by force
then have "x = ?x"
using esub' eeq yeq zeq by simp
then have "z = ?z"
using esub' eeq yeq by simp
obtain eq': "i' = i" "(i'+a'+a') mod M = k"
using ‹x = ?x› xeq using ‹z =?z› zeq by auto
then have "diff (i'+a') i' = int a'"
by (simp add: diff_def ‹a' < M›)
then have "a' = a"
by (metis ‹a' ∈ A› add.commute df diff2_invert eq' mod_add_right_eq nat_int)
then have "y = ?y"
by (metis ‹x = ?x› prod_encode_eq snd_conv yeq xeq)
then show "T = {?x,?y,?z}"
using Teq ‹x = ?x› ‹z = ?z› sets_eq by presburger
qed
qed
qed
have *: "card (uedges G) ≤ ε/12 * (card (uverts G))⇧2"
using L ‹L < card (uverts G)› ‹unique_triangles G› ‹uwellformed G› by blast
have diff_cancel: "∃j<M. diff j i = int a" if "a ∈ A" for i a
using M_mod_bound diff_invert that by blast
have diff2_cancel: "∃j<M. diff2 j i = int a" if "a ∈ A" for i a
using M_mod_bound diff2_invert that by blast
have card_Edges: "card (Edges (part_of ξ) (part_of ζ) df) = M * card A" (is "card ?E = _")
if "ξ ≠ ζ" and df_cancel: "∀a∈A. ∀i<M. ∃j<M. df j i = int a"
and df_inj: "∀a. inj_on (λx. df x a) {..<M}" for ξ ζ df
proof -
define R where "R ≡ λξ Y df u p. ∃x y i a. u = {x,y} ∧ p = (i,a) ∧ x = prod_encode (ξ,i)
∧ y ∈ Y ∧ a ∈ A ∧ df(from_part y) (from_part x) = int a"
have R_uniq: "⟦R ξ (part_of ζ) df u p; R ξ (part_of ζ) df u p'; ξ ≠ ζ⟧ ⟹ p' = p" for u p p' ξ ζ df
by (auto simp add: R_def doubleton_eq_iff)
define f where "f ≡ λξ Y df u. @p. R ξ Y df u p"
have f_if_R: "f ξ (part_of ζ) df u = p" if "R ξ (part_of ζ) df u p" "ξ ≠ ζ" for u p ξ ζ df
using R_uniq f_def that by blast
have "bij_betw (f ξ (part_of ζ) df) ?E ({..<M} × A)"
unfolding bij_betw_def inj_on_def
proof (intro conjI strip)
fix u u'
assume "u ∈ ?E" and "u' ∈ ?E"
and eq: "f ξ (part_of ζ) df u = f ξ (part_of ζ) df u'"
obtain x y a where u: "u = {x,y}" "x ∈ part_of ξ" "y ∈ part_of ζ" "a ∈ A"
and df: "df (from_part y) (from_part x) = int a"
using ‹u ∈ ?E› by (force simp add: Edges_def image_iff)
then obtain i where i: "x = prod_encode (ξ,i)"
using part_of_def by blast
with u df R_def f_if_R that have fu: "f ξ (part_of ζ) df u = (i,a)"
by blast
obtain x' y' a' where u': "u' = {x',y'}" "x' ∈ part_of ξ" "y' ∈ part_of ζ" "a'∈A"
and df': "df (from_part y') (from_part x') = int a'"
using ‹u' ∈ ?E› by (force simp add: Edges_def image_iff)
then obtain i' where i': "x' = prod_encode (ξ,i')"
using part_of_def by blast
with u' df' R_def f_if_R that have fu': "f ξ (part_of ζ) df u' = (i',a')"
by blast
have "i'=i" "a' = a"
using fu fu' eq by auto
with i i' have "x = x'"
by meson
moreover have "from_part y = from_part y'"
using df df' ‹x = x'› ‹a' = a› df_inj u'(3) u(3)
by (clarsimp simp add: inj_on_def) (metis part_of_M lessThan_iff)
ultimately show "u = u'"
using u u' by (metis enc_iff from_part_def prod.collapse prod_decode_inverse)
next
have "f ξ (part_of ζ) df ` ?E ⊆ {..<M} × A"
proof (clarsimp simp: Edges_def)
fix i a x y b
assume "x ∈ part_of ξ" "y ∈ part_of ζ" "df (from_part y) (from_part x) = int b"
"b ∈ A" and feq: "(i, a) = f ξ (part_of ζ) df {x, y}"
then have "R ξ (part_of ζ) df {x,y} (from_part x, b)"
by (auto simp: R_def doubleton_eq_iff part_of_def)
then have "(from_part x, b) = (i, a)"
by (simp add: f_if_R feq from_part_def that)
then show "i < M ∧ a ∈ A"
using ‹x ∈ part_of ξ› ‹b ∈ A› part_of_M by fastforce
qed
moreover have "{..<M} × A ⊆ f ξ (part_of ζ) df ` ?E"
proof clarsimp
fix i a assume "a ∈ A" and "i < M"
then obtain j where "j<M" and j: "df j i = int a"
using df_cancel by metis
then have fj: "f ξ (part_of ζ) df {prod_encode (ξ, i), prod_encode (ζ, j)} = (i,a)"
by (metis R_def ‹a ∈ A› enc_iff f_if_R from_enc ‹ξ ≠ ζ›)
then have "{prod_encode (ξ,i), prod_encode (ζ, j mod M)} ∈ Edges (part_of ξ) (part_of ζ) df"
apply (clarsimp simp: Edges_def doubleton_eq_iff)
by (metis ‹a ∈ A› ‹i < M› ‹j < M› enc_iff from_enc image_eqI j mod_if)
then show "(i,a) ∈ f ξ (part_of ζ) df ` Edges (part_of ξ) (part_of ζ) df"
using ‹j < M› fj image_iff by fastforce
qed
ultimately show "f ξ (part_of ζ) df ` ?E = {..<M} × A" by blast
qed
then show ?thesis
by (simp add: bij_betw_same_card card_cartesian_product)
qed
have [simp]: "disjnt XY YZ" "disjnt XY XZ" "disjnt YZ XZ"
using disjnt_part_of unfolding XY_def YZ_def XZ_def Edges_def disjnt_def
by (clarsimp simp add: disjoint_iff doubleton_eq_iff, meson disjnt_iff n_not_Suc_n nat.discI)+
have [simp]: "card XY = M * card A" "card YZ = M * card A"
by (simp_all add: XY_def YZ_def card_Edges diff_cancel inj_on_diff)
have [simp]: "card XZ = M * card A"
by (simp_all add: XZ_def card_Edges diff2_cancel inj_on_diff2)
have "card (uedges G) = 3 * M * card A"
by (simp add: G_def card_Un_disjnt)
then have "card A ≤ ε * (real M / 4)"
using * ‹0 < M› by (simp add: cardG power2_eq_square)
also have "… < ε * N"
using ‹N>0› by (simp add: M_def assms)
finally show "card A < ε * N" .
qed
qed
text‹We finally present the main statement formulated using the upper asymptotic density condition.›
theorem RothArithmeticProgressions:
assumes "upper_asymptotic_density A > 0"
shows "∃k d. d>0 ∧ progression3 k d ⊆ A"
proof (rule ccontr)
assume non: "∄k d. 0 < d ∧ progression3 k d ⊆ A"
obtain M where X: "∀N ≥ M. ∀A' ⊆ {..<N}. (∄k d. d>0 ∧ progression3 k d ⊆ A')
⟶ card A' < upper_asymptotic_density A / 2 * real N"
by (metis half_gt_zero RothArithmeticProgressions_aux assms)
then have "∀N ≥ M. card (A ∩ {..<N}) < upper_asymptotic_density A / 2 * N"
by (meson order_trans inf_le1 inf_le2 non)
then have "upper_asymptotic_density A ≤ upper_asymptotic_density A / 2"
by (force simp add: eventually_sequentially less_eq_real_def intro!: upper_asymptotic_densityI)
with assms show False by linarith
qed
end