The Plünnecke-Ruzsa Inequality

Angeliki Koutsoukou-Argyraki 🌐 📧 and Lawrence C. Paulson

May 26, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We formalise Plünnecke's inequality and the Plünnecke-Ruzsa inequality, following the notes by Timothy Gowers: "Introduction to Additive Combinatorics" (2022) for the University of Cambridge. To this end, we first introduce basic definitions and prove elementary facts on sumsets and difference sets. Then, we show two versions of the Ruzsa triangle inequality. We follow with a proof due to Petridis.

License

BSD License

Topics

Session Pluennecke_Ruzsa_Inequality

Depends on

Used by

Cite

× 
@article{Pluennecke_Ruzsa_Inequality-AFP,
  author  = {Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
  title   = {The Plünnecke-Ruzsa Inequality},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Pluennecke_Ruzsa_Inequality.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: