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 #

Noncommutative Ruzsa triangle inequality #

source
theorem Finset.ruzsa_triangle_inequality_div_div_div {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A / C).card * B.card ≤ (A / B).card * (C / B).card

Ruzsa's triangle inequality. Division version.

source
theorem Finset.ruzsa_triangle_inequality_sub_sub_sub {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A - C).card * B.card ≤ (A - B).card * (C - B).card

Ruzsa's triangle inequality. Subtraction version.

source
theorem Finset.ruzsa_triangle_inequality_mulInv_mulInv_mulInv {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A * C⁻¹).card * B.card ≤ (A * B⁻¹).card * (C * B⁻¹).card

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

source
theorem Finset.ruzsa_triangle_inequality_addNeg_addNeg_addNeg {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A + -C).card * B.card ≤ (A + -B).card * (C + -B).card

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

source
theorem Finset.ruzsa_triangle_inequality_invMul_invMul_invMul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A⁻¹ * C).card ≤ (B⁻¹ * A).card * (B⁻¹ * C).card

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

source
theorem Finset.ruzsa_triangle_inequality_negAdd_negAdd_negAdd {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (-A + C).card ≤ (-B + A).card * (-B + C).card

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

source
theorem Finset.ruzsa_triangle_inequality_div_mul_mul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A / C).card * B.card ≤ (A * B).card * (C * B).card

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

source
theorem Finset.ruzsa_triangle_inequality_sub_add_add {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A - C).card * B.card ≤ (A + B).card * (C + B).card

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

source
theorem Finset.ruzsa_triangle_inequality_mulInv_mul_mul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A * C⁻¹).card * B.card ≤ (A * B).card * (C * B).card

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

source
theorem Finset.ruzsa_triangle_inequality_addNeg_add_add {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A + -C).card * B.card ≤ (A + B).card * (C + B).card

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

source
theorem Finset.ruzsa_triangle_inequality_invMul_mul_mul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A⁻¹ * C).card ≤ (B * A).card * (B * C).card

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

source
theorem Finset.ruzsa_triangle_inequality_negAdd_add_add {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (-A + C).card ≤ (B + A).card * (B + C).card

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

source
theorem Finset.ruzsa_triangle_inequality_mul_div_mul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A * C).card ≤ (B / A).card * (B * C).card

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

source
theorem Finset.ruzsa_triangle_inequality_add_sub_add {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A + C).card ≤ (B - A).card * (B + C).card

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

source
theorem Finset.ruzsa_triangle_inequality_mul_mulInv_mul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A * C).card ≤ (B * A⁻¹).card * (B * C).card

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

source
theorem Finset.ruzsa_triangle_inequality_add_addNeg_add {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
B.card * (A + C).card ≤ (B + -A).card * (B + C).card

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

source
theorem Finset.ruzsa_triangle_inequality_mul_mul_invMul {G : Type u_1} [DecidableEq G] [Group G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A * C).card * B.card ≤ (A * B).card * (C⁻¹ * B).card

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

source
theorem Finset.ruzsa_triangle_inequality_add_add_negAdd {G : Type u_1} [DecidableEq G] [AddGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A + C).card * B.card ≤ (A + B).card * (-C + B).card

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

Plünnecke-Petridis inequality #

source
theorem Finset.pluennecke_petridis_inequality_mul {G : Type u_1} [DecidableEq G] [CommGroup G] {A : Finset G} {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
source
theorem Finset.pluennecke_petridis_inequality_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] {A : Finset G} {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 #

source
theorem Finset.ruzsa_triangle_inequality_mul_mul_mul {G : Type u_1} [DecidableEq G] [CommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A * C).card * B.card ≤ (A * B).card * (B * C).card

Ruzsa's triangle inequality. Multiplication version.

source
theorem Finset.ruzsa_triangle_inequality_add_add_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A + C).card * B.card ≤ (A + B).card * (B + C).card

Ruzsa's triangle inequality. Addition version.

source
theorem Finset.ruzsa_triangle_inequality_mul_div_div {G : Type u_1} [DecidableEq G] [CommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A * C).card * B.card ≤ (A / B).card * (B / C).card

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

source
theorem Finset.ruzsa_triangle_inequality_add_sub_sub {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A + C).card * B.card ≤ (A - B).card * (B - C).card

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

source
theorem Finset.ruzsa_triangle_inequality_div_mul_div {G : Type u_1} [DecidableEq G] [CommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A / C).card * B.card ≤ (A * B).card * (B / C).card

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

source
theorem Finset.ruzsa_triangle_inequality_sub_add_sub {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A - C).card * B.card ≤ (A + B).card * (B - C).card

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

source
theorem Finset.card_div_mul_le_card_div_mul_card_mul {G : Type u_1} [DecidableEq G] [CommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A / C).card * B.card ≤ (A / B).card * (B * C).card

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

source
theorem Finset.card_sub_add_le_card_sub_add_card_add {G : Type u_1} [DecidableEq G] [AddCommGroup G] (A : Finset G) (B : Finset G) (C : Finset G) :
(A - C).card * B.card ≤ (A - B).card * (B + C).card

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

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.