Documentation

Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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 #

References #

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 #

Ruzsa's triangle inequality. Division version.

Ruzsa's triangle inequality. Subtraction version.

Ruzsa's triangle inequality. Mulinv-mulinv-mulinv version.

Ruzsa's triangle inequality. Addneg-addneg-addneg version.

Ruzsa's triangle inequality. Invmul-invmul-invmul version.

Ruzsa's triangle inequality. Negadd-negadd-negadd version.

Ruzsa's triangle inequality. Div-mul-mul version.

Ruzsa's triangle inequality. Sub-add-add version.

Ruzsa's triangle inequality. Mulinv-mul-mul version.

Ruzsa's triangle inequality. Addneg-add-add version.

Ruzsa's triangle inequality. Invmul-mul-mul version.

Ruzsa's triangle inequality. Negadd-add-add version.

Ruzsa's triangle inequality. Mul-div-mul version.

Ruzsa's triangle inequality. Add-sub-add version.

Ruzsa's triangle inequality. Mul-mulinv-mul version.

Ruzsa's triangle inequality. Add-addneg-add version.

Ruzsa's triangle inequality. Mul-mul-invmul version.

Ruzsa's triangle inequality. Add-add-negadd version.

Plünnecke-Petridis inequality #

theorem Finset.pluennecke_petridis_inequality_mul {G : Type u_1} [DecidableEq G] [CommGroup G] {A B : Finset G} (C : Finset G) (hA : A'A, (A * B).card * A'.card (A' * B).card * A.card) :
(A * B * C).card * A.card (A * B).card * (A * C).card
theorem Finset.pluennecke_petridis_inequality_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A B : Finset G} (C : Finset G) (hA : A'A, (A + B).card * A'.card (A' + B).card * A.card) :
(A + B + C).card * A.card (A + B).card * (A + C).card

Commutative Ruzsa triangle inequality #

Ruzsa's triangle inequality. Multiplication version.

Ruzsa's triangle inequality. Addition version.

Ruzsa's triangle inequality. Mul-div-div version.

Ruzsa's triangle inequality. Add-sub-sub version.

Ruzsa's triangle inequality. Div-mul-div version.

Ruzsa's triangle inequality. Sub-add-sub version.

Ruzsa's triangle inequality. Div-div-mul version.

Ruzsa's triangle inequality. Sub-sub-add version.

theorem Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul {G : Type u_1} [DecidableEq G] [CommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (m n : ) :
(B ^ m / B ^ n).card ((A * B).card / A.card) ^ (m + n) * A.card

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.

theorem Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (m n : ) :
(m B - n B).card ((A + B).card / A.card) ^ (m + n) * A.card

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.

theorem Finset.pluennecke_ruzsa_inequality_pow_div_pow_div {G : Type u_1} [DecidableEq G] [CommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (m n : ) :
(B ^ m / B ^ n).card ((A / B).card / A.card) ^ (m + n) * A.card

The Plünnecke-Ruzsa inequality. Division version.

theorem Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (m n : ) :
(m B - n B).card ((A - B).card / A.card) ^ (m + n) * A.card

The Plünnecke-Ruzsa inequality. Subtraction version.

theorem Finset.pluennecke_ruzsa_inequality_pow_mul {G : Type u_1} [DecidableEq G] [CommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (n : ) :
(B ^ n).card ((A * B).card / A.card) ^ n * A.card

Special case of the Plünnecke-Ruzsa inequality. Multiplication version.

theorem Finset.pluennecke_ruzsa_inequality_nsmul_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (n : ) :
(n B).card ((A + B).card / A.card) ^ n * A.card

Special case of the Plünnecke-Ruzsa inequality. Addition version.

theorem Finset.pluennecke_ruzsa_inequality_pow_div {G : Type u_1} [DecidableEq G] [CommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (n : ) :
(B ^ n).card ((A / B).card / A.card) ^ n * A.card

Special case of the Plünnecke-Ruzsa inequality. Division version.

theorem Finset.pluennecke_ruzsa_inequality_nsmul_sub {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A : Finset G} (hA : A.Nonempty) (B : Finset G) (n : ) :
(n B).card ((A - B).card / A.card) ^ n * A.card

Special case of the Plünnecke-Ruzsa inequality. Subtraction version.