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.

source

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

(A - C).card * B.card ≤ (A - B).card * (B - C).card

Ruzsa's triangle inequality. Subtraction version.

source

theorem finset.card_sub_mul_le_card_add_mul_card_add {α : Type u_1} [add_comm_group α] [decidable_eq α] (A B C : finset α) :

(A - C).card * B.card ≤ (A + B).card * (B + C).card

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

source

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.

source

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.

source

theorem finset.card_add_mul_le_card_sub_mul_card_add {α : Type u_1} [add_comm_group α] [decidable_eq α] (A B C : finset α) :

(A + C).card * B.card ≤ (A - B).card * (B + C).card

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

source

theorem finset.card_add_mul_le_card_add_mul_card_sub {α : Type u_1} [add_comm_group α] [decidable_eq α] (A B C : finset α) :

(A + C).card * B.card ≤ (A + B).card * (B - C).card

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

source

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.

source

theorem finset.add_pluennecke_petridis {α : Type u_1} [add_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

source

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 #

source

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.

source

theorem finset.card_add_mul_card_le_card_add_mul_card_add {α : Type u_1} [add_comm_group α] [decidable_eq α] (A B C : finset α) :

(A + C).card * B.card ≤ (A + B).card * (B + C).card

Ruzsa's triangle inequality. Addition version.

source

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

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

source

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

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

source

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

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

source

theorem finset.card_add_nsmul_le {α : Type u_1} [add_comm_group α] [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)

source

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)

source

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.

source

theorem finset.card_nsmul_sub_nsmul_le {α : Type u_1} [add_comm_group α] [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.

source

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.

source

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

source

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.

source

theorem finset.card_nsmul_le {α : Type u_1} [add_comm_group α] [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.

source

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

source

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.