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} [] [] (A : ) (B : ) (C : ) :
(A - C).card * B.card (A - B).card * (B - C).card

Ruzsa's triangle inequality. Subtraction version.

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

Ruzsa's triangle inequality. Division version.

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

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

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

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

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

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

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

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

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

theorem Finset.add_pluennecke_petridis {α : Type u_1} [] [] {A : } {B : } (C : ) (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.mul_pluennecke_petridis {α : Type u_1} [] [] {A : } {B : } (C : ) (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.card_add_mul_card_le_card_add_mul_card_add {α : Type u_1} [] [] (A : ) (B : ) (C : ) :
(A + C).card * B.card (A + B).card * (B + C).card

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

Ruzsa's triangle inequality. Multiplication version.

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

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

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

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

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

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

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

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

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

theorem Finset.card_add_nsmul_le {α : Type u_2} [] [] {A : } {B : } (hAB : A'A, (A + B).card * A'.card (A' + B).card * A.card) (n : ) :
(A + n B).card ((A + B).card / A.card) ^ n * A.card
theorem Finset.card_mul_pow_le {α : Type u_1} [] [] {A : } {B : } (hAB : A'A, (A * B).card * A'.card (A' * B).card * A.card) (n : ) :
(A * B ^ n).card ((A * B).card / A.card) ^ n * A.card
theorem Finset.card_nsmul_sub_nsmul_le {α : Type u_1} [] [] {A : } (hA : A.Nonempty) (B : ) (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.card_pow_div_pow_le {α : Type u_1} [] [] {A : } (hA : A.Nonempty) (B : ) (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.card_nsmul_sub_nsmul_le' {α : Type u_1} [] [] {A : } (hA : A.Nonempty) (B : ) (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.card_pow_div_pow_le' {α : Type u_1} [] [] {A : } (hA : A.Nonempty) (B : ) (m : ) (n : ) :
(B ^ m / B ^ n).card ((A / B).card / A.card) ^ (m + n) * A.card

The Plünnecke-Ruzsa inequality. Subtraction version.

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

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

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

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

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

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

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

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