Roth's Theorem on Arithmetic Progressions

 

Title: Roth's Theorem on Arithmetic Progressions
Authors: Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson
Submission date: 2021-12-28
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├ę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" (revised version here) and W.T. Gowers's Cambridge lecture notes "Topics in Combinatorics". 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".
BibTeX:
@article{Roth_Arithmetic_Progressions-AFP,
  author  = {Chelsea Edmonds and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
  title   = {Roth's Theorem on Arithmetic Progressions},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Roth_Arithmetic_Progressions.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Ergodic_Theory, Girth_Chromatic, Random_Graph_Subgraph_Threshold, Szemeredi_Regularity
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.