Finset.card_mul_mul_card_le_card_mul_mul_card_mul
theorem Finset.card_mul_mul_card_le_card_mul_mul_card_mul :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A * C).card * B.card ≤ (A * B).card * (B * C).card
**Ruzsa's Triangle Inequality** (Multiplication Version): This theorem states that for any type `α` that forms a commutative group and possesses a decidable equality, given three finite sets `A`, `B`, and `C` of type `α`, the cardinals (sizes) of these sets satisfy a certain inequality. Specifically, the product of the cardinal of `A * C` and the cardinal of `B` is less than or equal to the product of the cardinal of `A * B` and the cardinal of `B * C`. Here, `A * B` denotes the set of all elements that can be obtained by multiplying an element of `A` with an element of `B`.
More concisely: For any commutative group type `α` with decidable equality, the cardinal product of sets `A`, `B`, and `C` satisfies `|A ⊤ B| * |B ⊤ C| ≤ |A ⊤ B| * |B ⊤ C|`, where `|.|` denotes the cardinality and `⊤` denotes the cartesian product.
|
Finset.card_add_mul_le_card_add_mul_card_sub
theorem Finset.card_add_mul_le_card_add_mul_card_sub :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A + C).card * B.card ≤ (A + B).card * (B - C).card
**Ruzsa's Triangle Inequality**: In the context of an additive commutative group `α` with decidable equality, for any three finite sets `A`, `B`, and `C` from `α`, the number of elements in the sum-set `(A + C)` times the number of elements in `B` is less than or equal to the number of elements in the sum-set `(A + B)` times the number of elements in `B` that are not in `C` (`(B - C)`). This is the add-add-sub version of the inequality.
More concisely: In an additive commutative group with decidable equality, the size of A + C times the size of B is less than or equal to the size of A + B times the size of B \setminus C.
|
Finset.card_div_mul_le_card_mul_mul_card_div
theorem Finset.card_div_mul_le_card_mul_mul_card_div :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A / C).card * B.card ≤ (A * B).card * (B / C).card
**Ruzsa's triangle inequality theorem (div-mul-div version)**: For any type `α` that forms a commutative group and has decidable equality, and for any finite sets `A`, `B` and `C` of type `α`, the cardinality (or size) of the set obtained by dividing `A` by `C` multiplied by the cardinality of `B` is less than or equal to the cardinality of the set obtained by multiplying `A` and `B` multiplied by the cardinality of the set obtained by dividing `B` by `C`.
More concisely: For any commutative group `α` with decidable equality, and finite sets `A`, `B`, `C` of `α`, |A/C| * |B| ≤ |A * B| * |B/C|, where |X| denotes the cardinality of set X.
|
Finset.card_sub_mul_le_card_add_mul_card_add
theorem Finset.card_sub_mul_le_card_add_mul_card_add :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A - C).card * B.card ≤ (A + B).card * (B + C).card
**Ruzsa's triangle inequality - Sub-add-add version**: For any type `α` belonging to the `AddCommGroup` (an additive commutative group), and which has decidable equality, given any three finite sets `A`, `B`, and `C` of type `α`, the number of elements in the difference set `A - C` multiplied by the number of elements in set `B` is always less than or equal to the number of elements in the sum set `A + B` multiplied by the number of elements in the sum set `B + C`.
More concisely: For any additive commutative group `α` with decidable equality, the size of `(A - C)` times the size of `B` is less than or equal to the size of `(A + B)` times the size of `(B + C)`.
|
Finset.card_div_mul_le_card_div_mul_card_mul
theorem Finset.card_div_mul_le_card_div_mul_card_mul :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A / C).card * B.card ≤ (A / B).card * (B * C).card
The theorem, named as "Ruzsa's triangle inequality", states that for any set type `α` which forms a commutative group and has decidable equality, given three finite sets `A`, `B`, and `C` of this type, the cardinality of the set obtained by dividing `A` by `C`, multiplied by the cardinality of `B`, is less than or equal to the cardinality of the set obtained by dividing `A` by `B`, multiplied by the cardinality of the set obtained by multiplying `B` and `C`. This is the 'div-div-mul' version of the theorem, which provides an inequality constraint between certain operations on sets in a commutative group context.
More concisely: For sets `A`, `B`, and `C` in a commutative group with decidable equality, |A / C| * |B| ≤ |A / B| * |C|, where |X| denotes the cardinality of set X.
|
Finset.card_mul_mul_le_card_div_mul_card_mul
theorem Finset.card_mul_mul_le_card_div_mul_card_mul :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A * C).card * B.card ≤ (A / B).card * (B * C).card
**Ruzsa's Triangle Inequality (Mul-Div-Div Version)**: For any type `α` which forms a commutative group and has a decidable equality, given any three finite sets `A`, `B` and `C` of elements from `α`, the cardinality (i.e., the number of elements) of the product set `A * C` multiplied by the cardinality of `B` is always less than or equal to the product of the cardinality of the set `A / B` and the cardinality of the product set `B * C`.
More concisely: For any commutative group `α` with decidable equality and finite sets `A`, `B`, and `C` from `α`, |A × C| ≤ |B| · |A / B × C|, where |.| denotes cardinality.
|
Finset.card_pow_le
theorem Finset.card_pow_le :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (n : ℕ), ↑(B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
This theorem is a special case of the Plünnecke-Ruzsa inequality, specifically the multiplication version. It states that for any type `α` that is a commutative group with decidable equality, given a nonempty finite set `A` of this type, and any other finite set `B` of the same type and a natural number `n`, the cardinality of `B` raised to the power `n` is less than or equal to the cardinality of the product of `A` and `B` divided by the cardinality of `A`, all raised to the power `n` and multiplied by the cardinality of `A`.
More concisely: For any commutative group with decidable equality `α`, the cardinality of a finite set `B` raised to the power `n` is less than or equal to the product of the cardinalities of sets `A` and `B`, both raised to the power `n`, divided by the cardinality of set `A`. (Plünnecke-Ruzsa inequality, multiplication version)
|
Finset.card_pow_div_pow_le
theorem Finset.card_pow_div_pow_le :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (m n : ℕ), ↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
This is the statement of the Plünnecke-Ruzsa inequality in its multiplication version for finite sets. For any type `α` that forms a commutative group with decidable equality and two finite sets `A` and `B` of this type, given that `A` is nonempty and two natural numbers `m` and `n`, the cardinality of the set resulted from the division of `B` risen to the power `m` by `B` risen to the power `n`, is less than or equal to the cardinality of the set resulted from the multiplication of `A` and `B`, divided by the cardinality of `A`, all risen to the power `m + n`, multiplied by the cardinality of `A`. Note that proving this version of the inequality is more challenging than its division version as we cannot employ a double counting argument.
More concisely: For any commutative group `α` with decidable equality and finite sets `A` and `B` of type `α`, if `A` is nonempty, then $|A|^{-1} |B|^m |B|^n \leq |A \times B| |B|^{-(m+n)}$, where $|X|$ denotes the cardinality of a set `X`. (Plünnecke-Ruzsa inequality, multiplication version for finite sets)
|
Finset.card_add_mul_le_card_sub_mul_card_add
theorem Finset.card_add_mul_le_card_sub_mul_card_add :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A + C).card * B.card ≤ (A - B).card * (B + C).card
This is the statement of **Ruzsa's triangle inequality** in the version of addition-subtraction-subtraction. For any type `α` that forms an additive commutative group and that has decidable equality, and for any finite sets `A`, `B`, and `C` of elements of `α`, the cardinality of the set obtained by adding every element of `A` to every element of `C`, times the cardinality of `B`, is less than or equal to the cardinality of the set obtained by subtracting every element of `B` from every element of `A`, times the cardinality of the set obtained by adding every element of `B` to every element of `C`.
More concisely: For any additive commutative group `α` with decidable equality, and finite sets `A`, `B`, and `C` of elements from `α`, we have |A + C| *|B| ≤ |A + B + C| \* |B|, where |S| denotes the cardinality of set S.
|
Finset.card_nsmul_sub_nsmul_le'
theorem Finset.card_nsmul_sub_nsmul_le' :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
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** theorem in its subtraction variant states that for any type `α` that forms an additive commutative group and has a decidable equality, given two finite sets (or `Finset`s) `A` and `B` of this type with `A` being nonempty, and two natural numbers `m` and `n`, the cardinality of the set `m • B - n • B` (obtained by scalar multiplication and subtraction of sets) is bounded above by the expression `(↑(A - B).card / ↑A.card) ^ (m + n) * ↑A.card`, where `A - B` denotes the set difference, `.card` denotes the cardinality of a set, and `m + n` is the exponent. The theorem is a fundamental result in additive combinatorics that provides bounds on the growth rate of sets under addition and subtraction operations.
More concisely: For any additive commutative group type `α` with decidable equality, the cardinality of `m • (A - B)` for finite nonempty sets `A` and `B` of type `α` is bounded above by `(card A / card (A - B)) ^ (m + n) * card A`, where `m` and `n` are natural numbers.
|
Finset.card_nsmul_sub_nsmul_le
theorem Finset.card_nsmul_sub_nsmul_le :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (m n : ℕ), ↑(m • B - n • B).card ≤ (↑(A + B).card / ↑A.card) ^ (m + n) * ↑A.card
The theorem `Finset.card_nsmul_sub_nsmul_le` represents the **Plünnecke-Ruzsa inequality** in the context of addition. It states that for any type `α` which forms an additive commutative group and has decidable equality, given any nonempty `Finset` `A` of `α`, and another `Finset` `B` of `α` with two natural numbers `m` and `n`, the cardinality of the set obtained by taking the m-fold sum of `B`, subtracting the n-fold sum of `B`, is less than or equal to (the cardinality of the set obtained by adding `A` and `B`, divided by the cardinality of `A`) raised to the power of `m + n` times the cardinality of `A`. This is a more complex version of the inequality compared to the subtraction version due to the inability to apply a double counting argument.
More concisely: For any additive commutative group type `α` with decidable equality, the cardinality of the set obtained by taking `m`-fold sum of a nonempty `Finset` `B` of `α` and subtracting `n`-fold sum of `B`, is less than or equal to the cardinality of `A ∪ B` multiplied by the power of `|A|` raised to `m + n`.
|
Finset.card_mul_mul_le_card_div_mul_card_div
theorem Finset.card_mul_mul_le_card_div_mul_card_div :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A * C).card * B.card ≤ (A / B).card * (B / C).card
**Ruzsa's triangle inequality** is a theorem in the context of a commutative group that asserts the following inequality: For any three finite sets `A`, `B`, and `C` of elements from a commutative group `α` (where `α` has decidable equality), the cardinality (or size) of the set formed by multiplying every element of `A` with every element of `C` (denoted as `A * C`), times the cardinality of `B`, is less than or equal to the cardinality of the set formed by dividing every element of `A` by every element of `B` (denoted as `A / B`), times the cardinality of the set formed by dividing every element of `B` by every element of `C` (denoted as `B / C`).
More concisely: The product of the cardinalities of `A` and `C`, and the cardinality of `B`, is less than or equal to the product of the cardinalities of `A / B` and `B / C`.
|
Finset.card_div_mul_le_card_mul_mul_card_mul
theorem Finset.card_div_mul_le_card_mul_mul_card_mul :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A / C).card * B.card ≤ (A * B).card * (B * C).card
**Ruzsa's triangle inequality** (div-mul-mul version): For any type `α` that forms a commutative group and has decidable equality, and for any three finite sets `A`, `B`, and `C` of this type, the cardinality (or size) of the set resulting from dividing `A` by `C` and then multiplying by the cardinality of `B` is less than or equal to the product of the cardinalities of the sets resulting from multiplying `A` by `B` and `B` by `C`. In mathematical notation, this is saying |A/C| * |B| ≤ |A*B| * |B*C|.
More concisely: The cardinality of the quotient set A / C of a commutative group of type α with decidable equality, formed by dividing set A by set C, is less than or equal to the product of the cardinalities of the sets formed by multiplying A and B, and then multiplying B and C. That is, |A / C| * |B| ≤ |A * B| * |B * C|.
|
Finset.card_div_mul_le_card_div_mul_card_div
theorem Finset.card_div_mul_le_card_div_mul_card_div :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A / C).card * B.card ≤ (A / B).card * (B / C).card
This theorem states Ruzsa's triangle inequality in the context of division. Given any type `α` that forms a commutative group, for which equality is decidable, and three finite sets `A`, `B`, and `C` of elements of this type, the cardinality of the set obtained by dividing `A` by `C` multiplied by the cardinality of `B` is always less than or equal to the product of the cardinality of the set obtained by dividing `A` by `B` and the cardinality of the set obtained by dividing `B` by `C`.
More concisely: For commutative groups `α` with decidable equality, and finite sets `A`, `B`, `C` of `α`, we have |A / C| * |B| ≤ |A / B| * |B / C|.
|
Finset.card_sub_mul_le_card_sub_mul_card_sub
theorem Finset.card_sub_mul_le_card_sub_mul_card_sub :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A - C).card * B.card ≤ (A - B).card * (B - C).card
**Ruzsa's triangle inequality** in its subtraction variant states: Given an additive commutative group `α` along with a decidable equality on `α`, for any three finite sets `A`, `B`, and `C` in `α`, the cardinality of the set difference `A - C` multiplied by the cardinality of `B` is less than or equal to the product of the cardinalities of the set differences `A - B` and `B - C`.
More concisely: For any additive commutative group `α` with decidable equality, and finite sets `A, B, C` in `α`, |A - C| * |B| ≤ |A - B| * |B - C|.
|
Finset.card_pow_le'
theorem Finset.card_pow_le' :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (n : ℕ), ↑(B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ n * ↑A.card
This is a special case of the Plünnecke-Ruzsa inequality, specifically the division version. Given a type `α` which forms a commutative group and for which equality is decidable, if there is a nonempty `Finset` of `α` denoted `A`, then for any `Finset` `B` of `α` and any natural number `n`, the cardinality (size) of `B` raised to the `n`th power is less than or equal to the cardinality of `A` divided by the cardinality of `B`, raised to the `n`th power, all multiplied by the cardinality of `A`. This theorem measures a kind of "growth rate" of sets under the operation of the group, and is used in additive combinatorics.
More concisely: For any commutative group type `α` with decidable equality and nonempty finite sets `A` and `B`, the cardinality of `B^n` (the set of `n`-tuples of elements from `B`) is bounded above by the cardinality of `A` divided by the cardinality of `B` raised to the power of `n`.
|
Finset.card_add_mul_card_le_card_add_mul_card_add
theorem Finset.card_add_mul_card_le_card_add_mul_card_add :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A + C).card * B.card ≤ (A + B).card * (B + C).card
This theorem, known as **Ruzsa's triangle inequality** in its additive form, states that for any type `α` that forms an additive commutative group and has decidable equality, and for any three finite sets `A`, `B`, and `C` of elements of this type, the cardinality of the set `A + C` multiplied by the cardinality of `B` is less than or equal to the product of the cardinalities of `A + B` and `B + C`. In other words, if we perform element-wise addition on the elements of `A` and `C` and `B` and `C` respectively, and calculate the product of the size of these resultant sets with the size of `B`, this product would always be less than or equal to the product of the sizes of the sets obtained by adding `A` and `B` and `B` and `C` respectively.
More concisely: For any additive commutative group `α` with decidable equality, and finite sets `A`, `B`, `C` of elements of `α`, |A + C| * |B| ≤ |A + B| * |B + C|.
|
Finset.card_pow_div_pow_le'
theorem Finset.card_pow_div_pow_le' :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (m n : ℕ), ↑(B ^ m / B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ (m + n) * ↑A.card
This is the **Plünnecke-Ruzsa inequality** in subtraction form. The theorem states that for any type `α` (denoted by `α : Type u_1`) which is a commutative group (`inst : CommGroup α`) and which has decidable equality (`inst_1 : DecidableEq α`), given a nonempty finite set `A` from this type (`A : Finset α`, `A.Nonempty`) and any other finite set `B` from the same type (`B : Finset α`), and for any two natural numbers `m` and `n` (`m, n : ℕ`), the cardinality of the set obtained by raising `B` to the power of `m`, then dividing by `B` raised to the power of `n` (written as `B ^ m / B ^ n`), is less than or equal to the cardinality of the set obtained by dividing `A` by `B`, raised to the power of `m + n`, then multiplied by the cardinality of `A` (written as `(A / B).card ^ (m + n) * A.card`).
More concisely: For any commutative group `α` with decidable equality, the cardinality of `(B ^ m / B ^ n)`, where `B` is a finite subset of `α` and `m` and `n` are natural numbers, is less than or equal to the product of `(A / B).card ^ (m + n)` and `A.card`, where `A` is another finite subset of `α` not empty together with `A`.
|
Finset.card_mul_mul_le_card_mul_mul_card_div
theorem Finset.card_mul_mul_le_card_mul_mul_card_div :
∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (A B C : Finset α),
(A * C).card * B.card ≤ (A * B).card * (B / C).card
This theorem is a statement of Ruzsa's triangle inequality in the context of finite sets of elements from a commutative group. More specifically, for any three finite sets A, B and C of elements from a commutative group with a decidable equality relation, the product of the cardinality of the set resulting from multiplying A with C and the cardinality of B is less than or equal to the product of the cardinality of the set resulting from multiplying A with B and the cardinality of the set resulting from B divided by C.
More concisely: For any commutative group with decidable equality and finite sets A, B, C, |A · C| * |B| ≤ |A · B| * |B∖C|, where |X| denotes the cardinality of set X.
|
Finset.card_nsmul_le'
theorem Finset.card_nsmul_le' :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (n : ℕ), ↑(n • B).card ≤ (↑(A - B).card / ↑A.card) ^ n * ↑A.card
This is a special case of the Plünnecke-Ruzsa inequality, specifically the subtraction version. It states that for any type `α` which forms an additive commutative group and has decidable equality, given a nonempty finite subset 'A' of `α` and any other finite subset 'B' of `α`, along with a natural number 'n', the cardinality of the set gained by n-times of scalar multiplication of 'B' is less than or equal to the cardinality of the difference set 'A - B' divided by the cardinality of 'A', all raised to the power 'n', multiplied by the cardinality of 'A'.
More concisely: For any additive commutative group `α` with decidable equality, the cardinality of `n`-times scalar multiplication of a finite subset `B` of `α` is bounded above by the cardinality of the difference set `A - B` divided by the cardinality of `A`, raised to the power of `n`, times the cardinality of `A`.
|
Finset.card_nsmul_le
theorem Finset.card_nsmul_le :
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] {A : Finset α},
A.Nonempty → ∀ (B : Finset α) (n : ℕ), ↑(n • B).card ≤ (↑(A + B).card / ↑A.card) ^ n * ↑A.card
This theorem is a special case of the Plünnecke-Ruzsa inequality, specifically the version dealing with addition. It states that for any type `α` that forms an additive commutative group and has decidable equality, given a non-empty finite set `A` and any finite set `B` of the same type, and a natural number `n`, the cardinality of the set obtained by scaling `B` by `n` (`n • B`) is less than or equal to the cardinality of the set `A + B`, divided by the cardinality of `A`, all raised to the power `n` and then multiplied by the cardinality of `A`. This is a result in additive combinatorics that provides bounds on the size of set obtained by multiplying `B` by `n` in terms of the sizes of `A`, `B` and the sumset `A + B`.
More concisely: For any finite additive commutative group `α` with decidable equality, the cardinality of `n • B` is bounded above by the quotient of the cardinalities of `A + B` and `A` raised to the power of `n`.
|