Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Plünnecke-Ruzsa Inequality


view this post on Zulip Email Gateway (May 30 2022 at 07:27):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce the following new AFP entry:

The Plünnecke-Ruzsa Inequality
by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

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.

https://www.isa-afp.org/entries/Pluennecke_Ruzsa_Inequality.html

Enjoy,
René


Last updated: Jul 15 2022 at 23:21 UTC