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

Noncommutative Ruzsa triangle inequality

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

Ruzsa's triangle inequality. Division version.

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

Ruzsa's triangle inequality. Subtraction version.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.ruzsa_triangle_inequality_add_add_negAdd {G : Type u_1} [DecidableEq G] [AddGroup G] (A B 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

theorem Finset.pluennecke_petridis_inequality_mul {G : Type u_1} [DecidableEq G] [Group G] {A B : Finset G} (C : Finset G) (hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card) : (C * A * B).card * A.card ≤ (A * B).card * (C * A).card

theorem Finset.pluennecke_petridis_inequality_add {G : Type u_1} [DecidableEq G] [AddGroup G] {A B : Finset G} (C : Finset G) (hA : ∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card) : (C + A + B).card * A.card ≤ (A + B).card * (C + A).card

Commutative Ruzsa triangle inequality

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

Ruzsa's triangle inequality. Multiplication version.

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

Ruzsa's triangle inequality. Addition version.

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

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

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

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

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

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

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

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

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

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

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

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.