### 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

- Mathematics/Combinatorics

### Session Pluennecke_Ruzsa_Inequality

- Pluennecke_Ruzsa_Inequality

### Depends on

- A Case Study in Basic Algebra

### Used by

- Kneser’s Theorem and the Cauchy–Davenport Theorem
- The Balog–Szemerédi–Gowers Theorem
- Khovanskii's Theorem

### Auto-related entries

- The Balog–Szemerédi–Gowers Theorem
- Khovanskii's Theorem
- Hensel’s Lemma for the p-adic Integers
- Banach-Steinhaus Theorem

## Cite

×

Pluennecke_Ruzsa_Inequality-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- May 30, 2022 : Isabelle2021-1