The Plünnecke-Ruzsa inequality #
This file proves Ruzsa's triangle inequality, the Plünnecke-Petridis lemma, and the Plünnecke-Ruzsa inequality.
Main declarations #
Finset.ruzsa_triangle_inequality_sub_sub_sub
: The Ruzsa triangle inequality, difference version.Finset.ruzsa_triangle_inequality_add_add_add
: The Ruzsa triangle inequality, sum version.Finset.pluennecke_petridis_inequality_add
: The Plünnecke-Petridis inequality.Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add
: The Plünnecke-Ruzsa inequality.
References #
- Giorgis Petridis, The Plünnecke-Ruzsa inequality: an overview
- Terrence Tao, Van Vu, *Additive Combinatorics
See also #
In general non-abelian groups, small doubling doesn't imply small powers anymore, but small tripling
does. See Mathlib.Combinatorics.Additive.SmallTripling
.
Noncommutative Ruzsa triangle inequality #
Plünnecke-Petridis inequality #
Commutative Ruzsa triangle inequality #
Ruzsa's triangle inequality. Addition version.
Ruzsa's triangle inequality. Add-sub-sub version.
Ruzsa's triangle inequality. Sub-add-sub version.
Ruzsa's triangle inequality. Sub-sub-add version.
The Plünnecke-Ruzsa inequality. Multiplication version. Note that this is genuinely harder than the division version because we cannot use a double counting argument.
The Plünnecke-Ruzsa inequality. Addition version. Note that this is genuinely harder than the subtraction version because we cannot use a double counting argument.
The Plünnecke-Ruzsa inequality. Subtraction version.
Special case of the Plünnecke-Ruzsa inequality. Addition version.
Special case of the Plünnecke-Ruzsa inequality. Subtraction version.