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.card_sub_mul_le_card_sub_mul_card_sub: Ruzsa's triangle inequality, difference version.
• Finset.card_add_mul_le_card_add_mul_card_add: Ruzsa's triangle inequality, sum version.
• Finset.pluennecke_petridis: The Plünnecke-Petridis lemma.
• Finset.card_smul_div_smul_le: 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.card_sub_mul_le_card_sub_mul_card_sub {α : Type u_1} [AddCommGroup α] [DecidableEq α] (A : Finset α) (B : Finset α) (C : Finset α) : Finset.card (A - C) * Finset.card B ≤ Finset.card (A - B) * Finset.card (B - C)

Ruzsa's triangle inequality. Subtraction version.

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

Ruzsa's triangle inequality. Division version.

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

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

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

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

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

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

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

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

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

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

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

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

theorem Finset.add_pluennecke_petridis {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (C : Finset α) (hA : ∀ (A' : Finset α), A' ⊆ A → Finset.card (A + B) * Finset.card A' ≤ Finset.card (A' + B) * Finset.card A) : Finset.card (A + B + C) * Finset.card A ≤ Finset.card (A + B) * Finset.card (A + C)

theorem Finset.mul_pluennecke_petridis {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (C : Finset α) (hA : ∀ (A' : Finset α), A' ⊆ A → Finset.card (A * B) * Finset.card A' ≤ Finset.card (A' * B) * Finset.card A) : Finset.card (A * B * C) * Finset.card A ≤ Finset.card (A * B) * Finset.card (A * C)

Sum triangle inequality

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

Ruzsa's triangle inequality. Addition version.

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

Ruzsa's triangle inequality. Multiplication version.

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

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

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

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

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

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

theorem Finset.card_add_nsmul_le {α : Type u_2} [AddCommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (hAB : ∀ (A' : Finset α), A' ⊆ A → Finset.card (A + B) * Finset.card A' ≤ Finset.card (A' + B) * Finset.card A) (n : ℕ) : ↑(Finset.card (A + n • B)) ≤ (↑(Finset.card (A + B)) / ↑(Finset.card A)) ^ n * ↑(Finset.card A)

theorem Finset.card_mul_pow_le {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} {B : Finset α} (hAB : ∀ (A' : Finset α), A' ⊆ A → Finset.card (A * B) * Finset.card A' ≤ Finset.card (A' * B) * Finset.card A) (n : ℕ) : ↑(Finset.card (A * B ^ n)) ≤ (↑(Finset.card (A * B)) / ↑(Finset.card A)) ^ n * ↑(Finset.card A)

theorem Finset.card_nsmul_sub_nsmul_le {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : Finset.Nonempty A) (B : Finset α) (m : ℕ) (n : ℕ) : ↑(Finset.card (m • B - n • B)) ≤ (↑(Finset.card (A + B)) / ↑(Finset.card A)) ^ (m + n) * ↑(Finset.card A)

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.card_pow_div_pow_le {α : Type u_1} [CommGroup α] [DecidableEq α] {A : Finset α} (hA : Finset.Nonempty A) (B : Finset α) (m : ℕ) (n : ℕ) : ↑(Finset.card (B ^ m / B ^ n)) ≤ (↑(Finset.card (A * B)) / ↑(Finset.card A)) ^ (m + n) * ↑(Finset.card A)

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.card_nsmul_sub_nsmul_le' {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : Finset.Nonempty A) (B : Finset α) (m : ℕ) (n : ℕ) : ↑(Finset.card (m • B - n • B)) ≤ (↑(Finset.card (A - B)) / ↑(Finset.card A)) ^ (m + n) * ↑(Finset.card A)

The Plünnecke-Ruzsa inequality. Subtraction version.

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

The Plünnecke-Ruzsa inequality. Subtraction version.

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

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

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

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

theorem Finset.card_nsmul_le' {α : Type u_1} [AddCommGroup α] [DecidableEq α] {A : Finset α} (hA : Finset.Nonempty A) (B : Finset α) (n : ℕ) : ↑(Finset.card (n • B)) ≤ (↑(Finset.card (A - B)) / ↑(Finset.card A)) ^ n * ↑(Finset.card A)

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

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

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