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][petridis2014]
• [Terrence Tao, Van Vu, *Additive Combinatorics][tao-vu]

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

Ruzsa's triangle inequality. Subtraction version.

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

Ruzsa's triangle inequality. Division version.

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.pluennecke_petridis_inequality_add {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (C : Finset α) (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_mul {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (C : Finset α) (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

Sum triangle inequality

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

Ruzsa's triangle inequality. Addition version.

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

Ruzsa's triangle inequality. Multiplication version.

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_mul {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_sub {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_div_pow_div {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_add {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_mul {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (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_sub {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : A.Nonempty) (B : Finset α) (n : ℕ) : ↑(n • B).card ≤ (↑(A - B).card / ↑A.card) ^ n * ↑A.card

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

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

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