# The Plünnecke-Ruzsa inequality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

Ruzsa's triangle inequality. Division version.

theorem finset.card_sub_mul_le_card_sub_mul_card_sub {α : Type u_1} [decidable_eq α] (A B C : finset α) :
(A - C).card * B.card (A - B).card * (B - C).card

Ruzsa's triangle inequality. Subtraction version.

theorem finset.card_sub_mul_le_card_add_mul_card_add {α : Type u_1} [decidable_eq α] (A B C : finset α) :
(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} [comm_group α] [decidable_eq α] (A B C : finset α) :
(A / C).card * B.card (A * B).card * (B * C).card

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

theorem finset.card_mul_mul_le_card_div_mul_card_mul {α : Type u_1} [comm_group α] [decidable_eq α] (A B C : finset α) :
(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_sub_mul_card_add {α : Type u_1} [decidable_eq α] (A B C : finset α) :
(A + C).card * B.card (A - B).card * (B + C).card

theorem finset.card_add_mul_le_card_add_mul_card_sub {α : Type u_1} [decidable_eq α] (A B C : finset α) :
(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} [comm_group α] [decidable_eq α] (A B C : finset α) :
(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} [decidable_eq α] {A B : finset α} (C : finset α) (hA : (A' : finset α), 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} [comm_group α] [decidable_eq α] {A B : finset α} (C : finset α) (hA : (A' : finset α), 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_mul_mul_card_le_card_mul_mul_card_mul {α : Type u_1} [comm_group α] [decidable_eq α] (A B C : finset α) :
(A * C).card * B.card (A * B).card * (B * C).card

Ruzsa's triangle inequality. Multiplication version.

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

theorem finset.card_add_nsmul_le {α : Type u_1} [decidable_eq α] {A B : finset α} (hAB : (A' : finset α), 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} [comm_group α] [decidable_eq α] {A B : finset α} (hAB : (A' : finset α), 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_pow_div_pow_le {α : Type u_1} [comm_group α] [decidable_eq α] {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.card_nsmul_sub_nsmul_le {α : Type u_1} [decidable_eq α] {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.card_pow_div_pow_le' {α : Type u_1} [comm_group α] [decidable_eq α] {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. Subtraction version.

theorem finset.card_nsmul_sub_nsmul_le' {α : Type u_1} [decidable_eq α] {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.card_pow_le {α : Type u_1} [comm_group α] [decidable_eq α] {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.card_nsmul_le {α : Type u_1} [decidable_eq α] {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.card_nsmul_le' {α : Type u_1} [decidable_eq α] {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.card_pow_le' {α : Type u_1} [comm_group α] [decidable_eq α] {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.