diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,648 +1,649 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CoCon CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras CoSMed CoSMeDis Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree +Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn Szemeredi_Regularity TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weighted_Path_Order Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Roth_Arithmetic_Progressions/ROOT b/thys/Roth_Arithmetic_Progressions/ROOT new file mode 100644 --- /dev/null +++ b/thys/Roth_Arithmetic_Progressions/ROOT @@ -0,0 +1,11 @@ +chapter AFP + +session Roth_Arithmetic_Progressions (AFP) = "HOL-Probability" + + options [timeout = 600] + sessions + Girth_Chromatic Szemeredi_Regularity Random_Graph_Subgraph_Threshold Ergodic_Theory + theories + Roth_Arithmetic_Progressions + document_files + "root.tex" + diff --git a/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy new file mode 100644 --- /dev/null +++ b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy @@ -0,0 +1,1862 @@ +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 \For the Library\ + +declare prod_encode_eq [simp] +declare prod_decode_eq [simp] + +lemma mult_mod_cancel_right: + fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}" + assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n" + shows "a mod m = b mod m" +proof - + have "m dvd (a*n - b*n)" + using eq mod_eq_dvd_iff by blast + then have "m dvd a-b" + by (metis \coprime m n\ coprime_dvd_mult_left_iff left_diff_distrib') + then show ?thesis + using mod_eq_dvd_iff by blast +qed + +lemma mult_mod_cancel_left: + fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}" + assumes "(n * a) mod m = (n * b) mod m" and "coprime m n" + shows "a mod m = b mod m" + by (metis assms mult.commute mult_mod_cancel_right) + +(*Stronger than the one in Szemeredi [now installed in AFP_devel] *) +lemma edge_density_le1: "edge_density X Y G \ 1" +proof (cases "finite X \ finite Y") + case True + then show ?thesis + using of_nat_mono [OF max_all_edges_between, of X Y] + by (fastforce simp add: edge_density_def divide_simps) +qed (auto simp: edge_density_def) + +lemma card_3_iff: "card S = 3 \ (\x y z. S = {x,y,z} \ x \ y \ y \ z \ x \ z)" + by (fastforce simp: card_Suc_eq numeral_eq_Suc) + +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 min_card_fin_X_elem: "finite X \ x \ X \ card X \ 1" + using card.remove by fastforce + +lemma card_or_filter_max: + assumes "finite A" + shows "card {a \ A . P a \ Q a} \ card {a \ A . P a} + card {a \ A . Q a}" +proof - + have fin: "finite {a \ A . P a}" "finite {a \ A . Q a}" + by(simp_all add: assms) + have equiv: "{a \ A . P a \ Q a} = {a \ A . P a} \ {a \ A . Q a}" by auto + then have "card {a \ A . P a} + card {a \ A . Q a} = card ({a \ A . P a} \ {a \ A . Q a}) + card ({a \ A . P a} \ {a \ A . Q a})" + using card_Un_Int fin by auto + thus ?thesis using equiv + by presburger +qed + +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_Union1: + "all_edges_between (Union \) Y G = (\X\\. all_edges_between X Y G)" + by (auto simp: all_edges_between_def) + +lemma all_edges_between_Union2: + "all_edges_between X (Union \) G = (\Y\\. all_edges_between X Y G)" + by (auto simp: all_edges_between_def) + +lemma all_edges_between_disjoint1: + assumes "disjoint R" + shows "disjoint ((\X. all_edges_between X Y G) ` R)" + using assms by (auto simp: all_edges_between_def disjoint_def) + +lemma all_edges_between_disjoint2: + assumes "disjoint R" + shows "disjoint ((\Y. all_edges_between X Y G) ` R)" + using assms by (auto simp: all_edges_between_def disjoint_def) + +lemma all_edges_between_disjoint_family_on1: + assumes "disjoint R" + shows "disjoint_family_on (\X. all_edges_between X Y G) R" + by (metis (no_types, lifting) all_edges_between_disjnt1 assms disjnt_def disjoint_family_on_def pairwiseD) + +lemma all_edges_between_disjoint_family_on2: + assumes "disjoint R" + shows "disjoint_family_on (\Y. all_edges_between X Y G) R" + by (metis (no_types, lifting) all_edges_between_disjnt2 assms disjnt_def disjoint_family_on_def pairwiseD) + +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 inj_on_mk_uedge: "X \ Y = {} \ inj_on mk_uedge (all_edges_between X Y G)" + by (auto simp: inj_on_def doubleton_eq_iff all_edges_between_def) + +lemma uwellformed_alt: + assumes "uwellformed G" "{x, y} \ uedges G" + shows "{x, y} \ uverts G" + using uwellformed_def assms by auto + +lemma uwellformed_alt_fst: + assumes "uwellformed G" "{x, y} \ uedges G" + shows "x \ uverts G" + using uwellformed_alt assms by simp + +lemma uwellformed_alt_snd: + assumes "uwellformed G" "{x, y} \ uedges G" + shows "y \ uverts G" + using uwellformed_alt 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 card_all_edges_between: + assumes "finite Y" "finite (uverts G)" "uwellformed G" + shows "card (all_edges_between X Y G) = (\y\Y. card (all_edges_between X {y} G))" +proof - + have "all_edges_between X Y G = (\y\Y. all_edges_between X {y} G)" + by (auto simp: all_edges_between_def) + moreover have "disjoint_family_on (\y. all_edges_between X {y} G) Y" + unfolding disjoint_family_on_def + by (auto simp: disjoint_family_on_def all_edges_between_def) + ultimately show ?thesis + by (simp add: card_UN_disjoint' assms finite_all_edges_between') +qed + +lemma max_edges_graph: + assumes "uwellformed G" "finite (uverts G)" + shows "card (uedges G) \ (card (uverts G))^2" +proof - + have "card (uedges G) \ card (uverts G) choose 2" + by (metis all_edges_finite assms card_all_edges card_mono wellformed_all_edges) + thus ?thesis + by (metis binomial_le_pow le0 neq0_conv order.trans zero_less_binomial_iff) +qed + +lemma all_edges_between_ss_uedges: "mk_uedge ` (all_edges_between X Y G) \ uedges G" + by (auto simp: all_edges_between_def) + +lemma all_edges_betw_D1: "(x, y) \ all_edges_between X Y G \ x \ X" + by (simp add: all_edges_between_def) + +lemma all_edges_betw_D2: "(x, y) \ all_edges_between X Y G \ y \ Y" + by (simp add: all_edges_between_def) + +lemma all_edges_betw_D3: "(x, y) \ all_edges_between X Y G \ {x, y} \ uedges G" + by (simp add: all_edges_between_def) + +lemma all_edges_betw_I: "x \ X \ y \ Y \ {x, y} \ uedges G \ (x, y) \ all_edges_between X Y G" + by (simp add: all_edges_between_def) + +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_betw_prod_def: "all_edges_between X Y G = {(x, y) \ X \ Y . {x, y} \ uedges G}" + by (simp add: all_edges_between_def) + +thm in_mk_uedge_img +lemma in_mk_uedge_img_iff: "{a,b} \ mk_uedge ` A \ (a,b) \ A \ (b,a) \ A" + by (auto simp: doubleton_eq_iff intro: rev_image_eqI) + +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_prod_def_neighbors: "uwellformed G \ + all_edges_between X Y G = {(x, y) \ X \ Y . neighbor_in_graph x y G}" + by (auto simp: neighbor_in_graph_def uwellformed_alt_fst uwellformed_alt_snd all_edges_between_def) + +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 card_triangle_triples_rotate: "card (triangle_triples X Y Z G) = card (triangle_triples Y Z X G)" +proof - + have "triangle_triples Y Z X G = (\(x,y,z). (y,z,x)) ` triangle_triples X Y Z G" + by (auto simp: triangle_triples_def case_prod_unfold image_iff insert_commute triangle_in_graph_def) + moreover have "inj_on (\(x, y, z). (y, z, x)) (triangle_triples X Y Z G)" + by (auto simp: inj_on_def) + ultimately show ?thesis + by (simp add: card_image) +qed + +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_vertices_distinct3: + assumes "uwellformed G" "triangle_in_graph x y z G" + shows "z \ x" + 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 edge_btw_vertices_not_equal: + assumes "uwellformed G" "(x, y) \ all_edges_between X Y G" + shows "x \ y" + using edge_vertices_not_equal all_edges_between_def + by (metis all_edges_betw_D3 assms) + +lemma mk_triangle_from_ss_edges: +assumes "(x, y) \ all_edges_between X Y G" and "(x, z) \ all_edges_between X Z G" and "(y, z) \ all_edges_between Y Z G" +shows "(triangle_in_graph x y z G)" + by (meson all_edges_betw_D3 assms triangle_in_graph_def) + +lemma triangle_in_graph_verts: + assumes "uwellformed G" + assumes "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 convert_triangle_rep_ss: + fixes G :: "ugraph" + assumes "X \ uverts G" and "Y \ uverts G" and "Z \ uverts G" + shows "mk_triangle_set ` {(x, y, z) \ X \ Y \ Z . (triangle_in_graph x y z G)} \ triangle_set G" + by (auto simp add: subsetI triangle_set_def) (auto) + +lemma finite_triangle_set: + fixes G :: "ugraph" + assumes fin: "finite (uverts G)" and wf: "uwellformed G" + shows "finite (triangle_set G)" +proof - + have "triangle_set G \ Pow (uverts G)" + using insert_iff 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: + fixes G :: "ugraph" + 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_set_finite: + assumes "finite (uverts G)" + assumes "uwellformed G" + shows "finite (triangle_set G)" + using triangle_set_power_set_ss assms + by (meson finite_Pow_iff rev_finite_subset) + +lemma triangle_in_graph_ss: + fixes G :: "ugraph" and Gnew :: "ugraph" + assumes "uedges Gnew \ uedges G" + assumes "triangle_in_graph x y z Gnew" + shows "triangle_in_graph x y z G" +proof - + have "{x, y} \ uedges G" using assms triangle_in_graph_def by auto + have "{y, z} \ uedges G" using assms triangle_in_graph_def by auto + have "{x, z} \ uedges G" using assms triangle_in_graph_def by auto + thus ?thesis + by (simp add: \{x, y} \ uedges G\ \{y, z} \ uedges G\ triangle_in_graph_def) +qed + +lemma triangle_set_graph_edge_ss: + fixes G :: "ugraph" and Gnew :: "ugraph" + assumes "uwellformed G" + assumes "uedges Gnew \ uedges G" + assumes "uverts Gnew = uverts G" + shows "(triangle_set Gnew) \ (triangle_set G)" +proof (intro subsetI) + fix t assume "t \ triangle_set Gnew" + then obtain x y z where "t = {x,y,z}" and "triangle_in_graph x y z Gnew" + using triangle_set_def assms mem_Collect_eq by auto + then have "triangle_in_graph x y z G" using assms triangle_in_graph_ss by simp + thus "t \ triangle_set G" using triangle_set_def assms + using \t = {x,y,z}\ by auto +qed + +lemma triangle_set_graph_edge_ss_bound: + fixes G :: "ugraph" and Gnew :: "ugraph" + assumes "uwellformed G" + assumes "finite (uverts G)" + assumes "uedges Gnew \ uedges G" + assumes "uverts Gnew = uverts G" + shows "card (triangle_set G) \ card (triangle_set Gnew)" + using triangle_set_graph_edge_ss triangle_set_finite + by (simp add: assms card_mono) + + +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_pairI: + fixes \ :: real and G :: "ugraph" and X :: "uvert set" and Y ::"uvert set" + assumes "\ > 0" and "regular_pair X Y G \" and xss: "X' \ X" and yss: "Y' \ Y" and "card X' \ \ * card X" and "(card Y' \ \ * card Y)" + shows "\ edge_density X' Y' G - edge_density X Y G \ \ \" + using regular_pair_def assms by meson + +lemma edge_density_zero: "Y = {} \ edge_density X Y G = 0" + by (simp add: edge_density_def) + +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*\" + shows "card{x \ X. card (neighbors_ss x Y G) < (edge_density X Y G - \)* card (Y)} < \ * card X" + (is "card (?X') < \ * _") +proof (cases "?X' = {}") + case True + then show ?thesis + by (simp add: True \card X > 0\ eg0) + next + case False + 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 by simp + have "\ x. x \ ?X'\ (card (neighbors_ss x Y G)) < (edge_density X Y G - \) * (card Y)" + 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 + 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 sumge0: "(\x\?X'. card (neighbors_ss x Y G)) \ 0" + by blast + have xge0: "card X > 0" + using fin(1) False by fastforce + have yge0: "card Y > 0" + using False by fastforce + then have xyge0: "card X * card Y > 0" using xge0 by simp + then have xyne0: "card X * card Y \ 0" by simp + have fracg0:"(1/(card ?X' * card Y)) > 0" + using card_0_eq finx False yge0 by fastforce + then have upper2: "(1/(card ?X' * card Y)) * (\x\?X'. card (neighbors_ss x Y G)) < (1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y))" + using upper mult_less_cancel_left_pos[of "(1/(card ?X' * card Y))" "(\x\?X'. card (neighbors_ss x Y G))" "(card ?X')* ((edge_density X Y G - \)* (card Y))"] + by linarith + have minuse: "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y)) = (edge_density X Y G - \)" + proof - + have "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y)) = (1/(card ?X' * card Y)) * ((card ?X')* (card Y))*(edge_density X Y G - \)" + by (smt (z3) divide_divide_eq_right of_nat_mult times_divide_eq_left) + also have "\ = ((card ?X'* card Y)/(card ?X' * card Y)) * (edge_density X Y G - \)" by simp + also have "\ = 1 * (edge_density X Y G - \)" + using divide_eq_1_iff[of "(card ?X'* card Y)" "(card ?X'* card Y)"] xyne0 + using finx False by force + finally have "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y)) = (edge_density X Y G - \)" by simp + thus ?thesis by simp + qed + then have edlt1: "(1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y)) < edge_density X Y G" + using eg0 + by linarith + then have edlt2: "(1/(card ?X' * card Y))* (\x\?X'. card (neighbors_ss x Y G)) < edge_density X Y G" + using upper2 by linarith + then have "\edge_density X Y G - (1/(card ?X' * card Y))* (\x\?X'. card (neighbors_ss x Y G))\ = edge_density X Y G - (1/(card ?X' * card Y))* (\x\?X'. card (neighbors_ss x Y G))" + by linarith + have "(edge_density X Y G - (1/(card ?X' * card Y))* (\x\?X'. card (neighbors_ss x Y G))) > (edge_density X Y G - (1/(card ?X' * card Y)) * (card ?X')* ((edge_density X Y G - \)* (card Y)))" + using edlt1 edlt2 upper2 + by linarith + then have "edge_density X Y G - (1/(card ?X' * card Y)) * (\x\?X'. card (neighbors_ss x Y G)) > edge_density X Y G - (edge_density X Y G - \)" + using minuse by linarith + then have con: "edge_density X Y G - (1/(card ?X' * card Y)) * (\x\?X'. card (neighbors_ss x Y G)) > \" by simp + have ye: "card Y \ \ * (card Y)" using ebound by (simp add: yge0) + have xe': "card ?X' \ \ * (card X)" using a by fastforce + have "?X' \ X" by simp + then have "\ edge_density ?X' Y G - edge_density X Y G \ \ \" + using regular_pairI[of "\" "X" "Y" "G" "?X'" "Y"] assms ye xe' by simp + then have "\ (card (all_edges_between ?X' Y G))/ (card ?X' * card Y) - edge_density X Y G \ \ \" + by (simp add: edge_density_def) + then have "\ (1/(card ?X' * card Y)) * (card (all_edges_between ?X' Y G)) - edge_density X Y G \ \ \" + by simp + then have "\(1/(card ?X' * card Y)) * (\x\?X'. card (neighbors_ss x Y G)) - edge_density X Y G \ \ \" + using card_all_edges_betw_neighbor fin wf by simp + then have lt: "\edge_density X Y G - (1/(card ?X' * card Y)) * (\x\?X'. card (neighbors_ss x Y G)) \ \ \" + by simp + thus False using lt con by linarith + qed (* Following Gowers's proof - more in depth with reasoning on contradiction *) +qed + +lemma neighbor_set_meets_e_reg_cond: + fixes \::real + assumes "X \ uverts G" and "Y \ uverts G" and enot0: "\ > 0" + and fin: "finite X" "finite Y" and "uwellformed G" + and rp1: "regular_pair X Y G \" + and ed1: "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)" +proof - + have "card (neighbors_ss x Y G) \ (edge_density X Y G - \) * card Y" using assms by simp + thus ?thesis + by (smt (verit, ccfv_SIG) mult_right_mono of_nat_less_0_iff ed1 enot0) +qed + + +lemma all_edges_btwn_neighbour_sets_lower_bound: + fixes \::real + assumes "X \ uverts G" and "Y \ uverts G" and "Z \ uverts G" and "\ > 0" + and finG: "finite (uverts G)" + and wf: "uwellformed G" and fin: "finite X" "finite Y" "finite Z" + 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*\" + 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" + and "x \ X" + 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 neighbor_set_meets_e_reg_cond cond1 assms fin by meson + have min_sizeZ: "card ?Z' \ \ * card Z" using neighbor_set_meets_e_reg_cond cond2 assms fin by meson + then have "\ edge_density ?Y' ?Z' G - edge_density Y Z G \ \ \" + using min_sizeY regular_pairI[of "\" "Y" "Z" "G" "?Y'" "?Z'"] yss' zss' assms by simp + then have "-\ \ ( edge_density ?Y' ?Z' G - edge_density Y Z G)" + by linarith + then have "edge_density Y Z G - \ \ edge_density ?Y' ?Z' G" by linarith + 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 (metis abs_of_nat division_ring_divide_zero le_divide_eq mult_of_nat_commute of_nat_0_le_iff times_divide_eq_right zero_less_abs_iff) + then show ?thesis + by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) mult_of_nat_commute of_nat_mult) +qed + + +lemma edge_density_implies_edge_exists: + fixes \::real + assumes "X \ uverts G" and "Y \ uverts G" and "\ > 0" and "uwellformed G" + assumes "edge_density X Y G \ \" + obtains e where "e \ all_edges_between X Y G" +proof - + have "edge_density X Y G = card (all_edges_between X Y G) / (card X * card Y)" by (simp add: edge_density_def) + then have "card (all_edges_between X Y G) \ 0" + using assms divide_eq_0_iff by fastforce + thus ?thesis + by (metis card.empty empty_subsetI subsetI subset_antisym that) +qed + +text\We are now ready to show the Triangle Counting Lemma (Theorem 3.13 in Zhao's notes):\ + +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)}" + define XF where "XF \ \Y. {x \ X. card(neighbors_ss x Y G) < ((edge_density X Y G) - \) * card Y}" + have fin: "finite X" "finite Y" "finite Z" using finG rev_finite_subset xss yss zss by auto + have "card X > 0" + using card_0_eq ed1 edge_density_def en0 fin(1) by fastforce + have ebound: "\ \ 1/2" + using ed1 edge_density_le1 fin + by (metis le_divide_eq_numeral1(1) mult.commute order_trans) + then have ebound2: "1 - 2*\ \ 0" + by linarith + + 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" + by (simp add: X2_def) + have finx2: "finite X2" + by (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 minx2help: "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) + have edmultbound: "((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z) \ 0" + using ed3 ed1 ed2 assms(4) by auto + + text \Reasoning on the minimum number of edges between neighborhoods of @{term X} in @{term Y} +and @{term Z}.\ + + have edyzgt0: "((edge_density Y Z G) - \) > 0" + and edxygt0: "((edge_density X Y G) - \) > 0" using ed1 ed3 \\ > 0\ by linarith+ + have cardnzgt0: "card (neighbors_ss x Z G) \ 0" and cardnygt0: "card (neighbors_ss x Y G) \ 0" + if "x \ X2" for x + by auto + have card_y_bound: "\x. x \ X2 \ (card (neighbors_ss x Y G)) \ (edge_density X Y G - \) * (card Y)" + by (auto simp: XF_def X2_def) + have card_z_bound: "\x. x \ X2 \ (card (neighbors_ss x Z G)) \ (edge_density X Z G - \) * (card Z)" + by (auto simp: XF_def X2_def) + have card_y_bound': + "(\x\ X2. ((edge_density Y Z G) - \) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) \ + (\x\ X2 . ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (card (neighbors_ss x Z G)))" + by (rule sum_mono) (smt (verit, best) Groups.mult_ac(3) card_y_bound edyzgt0 mult.commute mult_right_mono of_nat_0_le_iff) + have x2_card: "\x. x \ X2 \ ((edge_density Y Z G) - \) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G)) + \ card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)" + by (meson all_edges_btwn_neighbour_sets_lower_bound assms(1) card_y_bound card_z_bound ed1 ed2 ed3 en0 fin finG local.wf rp1 rp2 rp3 subsetD xss yss zss) + have card_z_bound': + "(\x\ X2. ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (card (neighbors_ss x Z G))) \ + (\x\ X2. ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z))" + using card_z_bound mult_left_mono edxygt0 edyzgt0 by (fastforce intro!: sum_mono) + have eq_set: "\ x. 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 } = +card {(y, z) . y \ (neighbors_ss x Y G) \ z \ (neighbors_ss x Z G) \ {y, z} \ uedges G }" + by (metis (no_types, lifting) mem_Collect_eq 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 \ 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 {(y, z). y \ Y \ z \ Z \ {y, z} \ uedges G \ neighbor_in_graph x y G \ neighbor_in_graph x z G })" + by simp + finally have "card ?T_all = (\x\ X . card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))" + using eq_set by (auto simp: all_edges_between_def) + then 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 . ((edge_density Y Z G) - \) * (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)))" + by (meson x2_card finx2 sum_mono) + then have "card ?T_all \ (\x\ X2 . ((edge_density Y Z G) - \) * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G)))" + using l of_nat_le_iff [symmetric, where 'a=real] by force + then have "card ?T_all \ (\x\ X2 . ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (card (neighbors_ss x Z G)))" + using card_y_bound' by simp + then have tall_gt: "card ?T_all \ (\x\ X2 . ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z))" + using card_z_bound' by simp + have "(\x\ X2 . ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z)) = + card X2 * ((edge_density Y Z G) - \) * (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z)" + by simp + then have "of_real (card ?T_all) \ card X2 * ((edge_density Y Z G) - \) * (edge_density X Y G - \)* + (card Y) * (edge_density X Z G - \)* (card Z)" + using tall_gt + by force + then have "of_real (card ?T_all) \ ((1 - 2 * \) * card X) * ((edge_density Y Z G) - \) * + (edge_density X Y G - \)* (card Y) * (edge_density X Z G - \)* (card Z)" + using minx2 edmultbound dual_order.trans mult.commute ordered_comm_semiring_class.comm_mult_left_mono + by (smt (verit, ccfv_SIG) assms(4) ed1 ed2 mult_cancel_right mult_less_cancel_right +mult_pos_neg2 of_nat_0_eq_iff of_nat_le_0_iff) + then show ?thesis by (simp add: triangle_triples_def mult.commute mult.left_commute) +qed + +definition regular_graph :: "uvert set set \ ugraph \ real \ bool" + 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 = {} \ (real (card X) \ \ \ real (card Y) \ \)" + +definition decent_graph :: "uvert set set \ ugraph \ real \ bool" + where "decent_graph P G \ \ \R S. R\P \ S\P \ decent R S G \" for \::real + +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. This is mentioned briefly on pg 57 of +Zhao's notes towards the end of the proof.\ + +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) list.simps(15) 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)" + proof (clarsimp simp: triangle_set_def) + fix u v w + assume t: "triangle_in_graph u v w G" + then have "(u, v, w) \ tofl ` permutations_of_set {u,v,w}" + by (metis in_tofl local.wf triangle_commu1 triangle_vertices_distinct1 triangle_vertices_distinct2) + with t show "\t. (\x y z. t = {x, y, z} \ triangle_in_graph x y z G) \ (u, v, w) \ tofl ` permutations_of_set t" + by blast + qed + 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)" + apply (rule sum_mono) + by (metis card.infinite card_permutations_of_set card_triangle_3 eq_refl local.wf nat.simps(3) 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 "card {(x, y, z) \ X \ Y \ Z . (triangle_in_graph x y z G)} \ t" + 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 *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 3.15 in Zhao's notes).\ + +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 \ + (\Gnew. triangle_free_graph Gnew \ uverts Gnew = uverts G \ (uedges Gnew \ uedges G) \ + card (uedges G - uedges Gnew) \ \ * (card (uverts G))\<^sup>2)" + (is "\\::real > 0. \G. _ \ _ \ _ \ (\Gnew. ?\ G Gnew)") +proof (cases "\ < 1") + case False + define Gnew where "Gnew \ \G. ((uverts G), {}::uedge set)" + show ?thesis + proof (intro exI conjI strip) + fix G + assume G: "uwellformed G" "card(uverts G) > 0" + then show "triangle_free_graph (Gnew G)" "uverts (Gnew G) = uverts G" "uedges (Gnew G) \ uedges G" + by (auto simp: Gnew_def triangle_free_graph_empty) + have "real (card (uedges G)) \ (card (uverts G))\<^sup>2" + by (meson G card_gt_0_iff max_edges_graph of_nat_le_iff) + also have "\ \ \ * (card (uverts G))\<^sup>2" + using False mult_le_cancel_right1 by fastforce + finally show "real (card (uedges G - uedges (Gnew G))) \ \ * real ((card (uverts G))\<^sup>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) + (* a reminder: as it is implied we have: *) + 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 + using fin fin_part finite_graph_partition_le that by meson + 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$. + We call the graph obtained after this process @{term Gnew}. \ + + 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 \ irregular_pair R S G (\/4)}" + 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" \\Count the edge bound for @{term Ea}\ + 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 \ irregular_pair R S G (\/4)}. 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)" \\Count the edge bound for @{term Eb}.\ + proof - + 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)" + apply (rule sum_mono) + apply(auto simp add: divide_simps card_P_gt0 low_density_pairs_def edge_density_def + edge_dense_def) + by (smt (verit, best) card_edge_le_card of_nat_le_iff mult.assoc) + 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)" \\Count the edge bound for @{term Ec}.\ + 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\<^sup>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\<^sup>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 + \\total count\ + 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 allij: "\R S. edge R S \ uedges G" + using all_edges_between_ss_uedges edge_def by presburger + then have eae: "Ea \ uedges G" by (auto simp: Ea_def) + have eab: "Eb \ uedges G" using allij by (auto simp: Eb_def) + have "Ec \ uedges G" using allij by (auto simp: Ec_def) + then have diffedges: "(Ea \ Eb \ Ec) \ uedges G" + using eae eab by auto + 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: "regular_pair R S Gnew (\/4)" 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: "regular_graph P Gnew (\/4)" + 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 where xinp: "x \ R" and ilt: "R\P" + using graph_partition_new finite_graph_partition_obtain xin by metis + then obtain S where yinp: "y \ S" and jlt: "S\P" + using graph_partition_new finite_graph_partition_obtain yin by metis + then obtain T where zinp: "z \ T" and klt: "T\P" + using graph_partition_new finite_graph_partition_obtain zin by metis + have finitesubsets: "finite R" "finite S" "finite T" + using ilt jlt klt 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 subsets ilt jlt klt xinp yinp zinp unfolding dense_graph_def edge_dense_def + by (metis all_edges_betw_I equals0D triangle_in_graph_def trig_ex)+ + 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)*(?e4M * ?n) * (?e4M * ?n)" + by (metis (no_types) of_nat_0_le_iff of_nat_mult min_sizes mult_mono) + then have "(card R)*(card S)* (card T) \ (?e4M* ?n)^3" + by (simp add: power3_eq_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))\<^sup>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. +This is Corollary 3.18 in Zhao's notes:\ + +corollary corollary_triangle_removal: + fixes \ :: real + assumes "0 < \" + shows "\N>0. \G. card(uverts G) > N \ uwellformed G \ unique_triangles G \ + card (uedges G) \ \ * (card (uverts G))\<^sup>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\ \ + (\Gnew. triangle_free_graph Gnew \ uverts Gnew = uverts G \ (uedges Gnew \ uedges G) \ + card (uedges G - uedges Gnew) \ \/3 * (card (uverts G))\<^sup>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 + 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 + let ?TWO = "(\t. [t]\<^bsup>2\<^esup>)" + have tri_nsets_2: "[{x,y,z}]\<^bsup>2\<^esup> = {{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]\<^bsup>3\<^esup>" 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]\<^bsup>3\<^esup>" + 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]\<^bsup>2\<^esup>" 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]\<^bsup>2\<^esup>)" 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 triangle_set_finite) + have "card ([i]\<^bsup>2\<^esup>) = 3" if "i \ triangle_set G" for i + using that wf + unfolding triangle_set_def triangle_in_graph_def uwellformed_def + by (smt (z3) image_subset_iff mem_Collect_eq nsets_def sub that) + then show "(\i\triangle_set G. card ([i]\<^bsup>2\<^esup>)) = 3 * card (triangle_set G)" + by simp + qed + ultimately have A: "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 "\ = card (uverts G) choose 2" + by (metis G_ne card_all_edges card_eq_0_iff not_less0) + also have "\ = card (uverts G) * (card (uverts G) - 1) div 2" + by (meson n_choose_2_nat) + also have "\ < (card (uverts G))\<^sup>2" + by (simp add: G_ne less_imp_diff_less less_mult_imp_div_less power2_eq_square) + finally have B: "card (uedges G) < (card (uverts G))\<^sup>2" . + + have "card (triangle_set G) \ (card (uverts G))\<^sup>2 / 3" + using A B by linarith + also have "\ \ \ * card(uverts G) ^ 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\<^sup>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.\ + + 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\<^sup>2" + using A 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 \{... + +lemma RothArithmeticProgressions_aux: + fixes \::real + assumes "\ > 0" + obtains X where "\N \ X. \A \ {..k d. d>0 \ progression3 k d \ A) \ card A < \ * real N" +proof - + obtain X where "X>0" + and X: "\G. \card(uverts G) > X; uwellformed G; unique_triangles G\ + \ card (uedges G) \ \/12 * (card (uverts G))\<^sup>2" + by (metis assms corollary_triangle_removal less_divide_eq_numeral1(1) mult_eq_0_iff) + show thesis + proof (intro strip that) + fix N A + assume "X \ N" and A: "A \ {..k d. 0 < d \ progression3 k d \ A" + then have "N > 0" using \0 < X\ 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 {..k d. d > 0 \ progression3 k d \ int ` A" + by (metis p3_int_iff non pos_int_cases zero_le_imp_eq_int imageE insert_subset of_nat_0_le_iff +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)) ` {.. \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 \ i0 < 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) {.. 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 have "int y = int (x+a) mod int M" + unfolding diff_def by (smt (verit, ccfv_SIG) 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) {..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) > X" + using M_def \X \ 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: "\id\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 "a1a1 \ 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 "ix \ ?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 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 by blast + with \a \ A\ \j 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) + 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' 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 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 by blast + with \a \ A\ \k 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 + by (force simp add: XY_def Edges_def 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' 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 = i'" + by (metis Nat.add_diff_assoc2 \a' < M\ \i' < M\ add.left_commute add_implies_diff +less_imp_le_nat mod_add_right_eq mod_add_self2 mod_less) + 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 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 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 \k 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' 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))\<^sup>2" + using X \X < card (uverts G)\ \unique_triangles G\ \uwellformed G\ by blast + + have diff_cancel: "\j A" for i a + proof - + have "int a < int M" + using A M_def that by auto + then have "(int ((i + a) mod M) - int i) mod int M = int a" + by (simp add: mod_diff_left_eq of_nat_mod) + then show ?thesis + using \0 < M\ diff_def mod_less_divisor by blast + qed + have diff2_cancel: "\j A" "i = 2 * int a * (1 + int N) mod int M" + by (smt (verit) mod_diff_left_eq mod_mult_eq mod_mult_right_eq) + also have "\ = int a mod int M" + proof - + have "(2 * int a * (1 + int N) - int a) = M * a" + by (simp add: M_def algebra_simps) + then have "M dvd (2 * int a * (1 + int N) - int a)" + by simp + then show ?thesis + using mod_eq_dvd_iff by blast + qed + also have "\ = a" by (simp add: \a < M\) + finally show ?thesis + by (metis \0 < M\ diff2_def mod_less_divisor of_nat_Suc) + qed + + have card_Edges: "card (Edges (part_of \) (part_of \) df) = M * card A" (is "card ?E = _") + if "\ \ \" and df_cancel: "\a\A. \ija. inj_on (\x. df x a) {.. \ 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 ({.. 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) + then have "y = y'" + using part_of_def u'(3) u(3) by fastforce + ultimately show "u = u'" + using u'(1) u(1) by force + next + have "f \ (part_of \) df ` ?E \ {.. 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 "{.. A \ f \ (part_of \) df ` ?E" + proof clarsimp + fix i a assume "a \ A" and "i < M" + then obtain j where "j (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 = {.. 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_edges: "card (uedges G) = 3 * M * card A" + by (simp add: G_def card_Un_disjnt) + have "card A \ \ * (real M / 4)" + using * \0 < M\ by (simp add: cardG card_edges 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 X where X: "\N \ X. \A' \ {..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 \ X. card (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 + + + diff --git a/thys/Roth_Arithmetic_Progressions/document/root.tex b/thys/Roth_Arithmetic_Progressions/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Roth_Arithmetic_Progressions/document/root.tex @@ -0,0 +1,48 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amssymb} +\usepackage{isabelle,isabellesym} +\usepackage[english]{babel} % for guillemots + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Roth's Theorem on Arithmetic Progressions} +\author{Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson\\ +Computer Laboratory, University of Cambridge CB3 0FD\\ +\texttt{\{cle47,ak2110,lp15\}@cam.ac.uk}} + +\maketitle + +\begin{abstract} +We formalise a proof of Roth's Theorem on Arithmetic Progressions, a major result in additive +combinatorics on the existence of 3-term arithmetic progressions in subsets of natural numbers. +To this end, we follow a proof using graph regularity. We employ our recent formalisation of Szemer\'{e}di's +Regularity Lemma, a major result in extremal graph theory, which we use here to prove +the Triangle Counting Lemma and the Triangle Removal Lemma. +Our sources are Yufei Zhao's MIT lecture notes ``Graph Theory and Additive Combinatorics''% +\footnote{\url{https://ocw.mit.edu/courses/mathematics/18-217-graph-theory-and-additive-combinatorics-fall-2019/lecture-notes/MIT18_217F19_ch3.pdf} and \url{https://yufeizhao.com/gtac/gtac17.pdf}} +and W.T. Gowers's Cambridge lecture notes ``Topics in Combinatorics''.% +\footnote{\url{https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf}} +We also refer to the University of Georgia notes by Stephanie Bell and Will Grodzicki +``Using Szemerédi's Regularity Lemma to Prove Roth's Theorem''.% +\footnote{\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.432.327}} +\end{abstract} + +\tableofcontents + +\subsection*{Acknowledgements} +The authors were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council. + +\newpage + +% include generated text of all theories +\input{session} + +\end{document}