Finset.sum_card_slice_div_choose_le_one
theorem Finset.sum_card_slice_div_choose_le_one :
∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] {𝒜 : Finset (Finset α)} [inst_1 : Fintype α],
IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜 →
((Finset.range (Fintype.card α + 1)).sum fun r => ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r)) ≤ 1
The **Lubell-Yamamoto-Meshalkin inequality** states that for any given antichain `𝒜` from a finset of finsets, where an antichain is a set such that no two distinct elements are related, the sum of the proportions of elements it takes from each layer is less than or equal to `1`. Here, each layer is identified by the range of the cardinality of the Fintype `α` + `1`, and the proportion of elements from each layer is calculated as the cardinality of the slice of `𝒜` at `r` divided by the binomial coefficient of the cardinality of the Fintype `α` and `r`. The inequality holds for any linearly ordered field `𝕜` and any Fintype `α`.
More concisely: For any antichain of finsets, the sum of the proportions of elements from each layer (identified by the cardinality of the Fintype `α` + 1) is less than or equal to 1, where the proportion of elements from layer `r` is the size of the slice divided by the binomial coefficient of `α` and `r`, in any linearly ordered field.
|
Finset.IsAntichain.sperner
theorem Finset.IsAntichain.sperner :
∀ {α : Type u_2} [inst : Fintype α] {𝒜 : Finset (Finset α)},
IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜 → 𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)
**Sperner's Theorem**. This theorem states that for any given finite type 'α', and a set '𝒜' of finite sets of elements of 'α', if '𝒜' is an antichain (meaning no two distinct elements in '𝒜' are related by the subset relation), then the size (number of elements) of '𝒜' is bounded by the binomial coefficient "choose" function of the size of 'α' taken two at a time. This essentially means that the finite set 'α' exhibits a Sperner order.
More concisely: For any finite type 'α' and an antichain '𝒜' of finite subsets of 'α', the size of '𝒜' is bounded by the binomial coefficient of the size of 'α' taken two at a time.
|
Finset.card_div_choose_le_card_shadow_div_choose
theorem Finset.card_div_choose_le_card_shadow_div_choose :
∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : DecidableEq α] [inst_2 : Fintype α]
{𝒜 : Finset (Finset α)} {r : ℕ},
r ≠ 0 →
Set.Sized r ↑𝒜 → ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.card α).choose (r - 1))
This theorem, referred to as the downward local LYM inequality, states that for any types `𝕜` and `α` where `𝕜` is a linear ordered field and `α` has decidable equality and is a fintype, and for any Finset `𝒜` of `α` and any natural number `r` not equal to 0, if every finset in `𝒜` has size `r` (i.e., `𝒜` is `r`-sized), then the ratio of the cardinality of `𝒜` to the number of ways to choose `r` objects from `α` is less than or equal to the ratio of the cardinality of the shadow of `𝒜` (denoted as `𝒜.shadow`) to the number of ways to choose `r - 1` objects from `α`. In mathematical terms, $|\mathcal{A}| / \binom{|α|}{r} \leq |\partial\mathcal{A}| / \binom{|α|}{r - 1}$. This inequality is a part of combinatorial mathematics and is used to compare the size of a set to the size of its "shadow".
More concisely: For any r-sized finite set A in a linear ordered field with decidable equality and fintype element type α, the ratio of A's cardinality to the number of combinations of r elements from α is less than or equal to the ratio of A's shadow's cardinality to the number of combinations of r-1 elements from α.
|
Finset.le_card_falling_div_choose
theorem Finset.le_card_falling_div_choose :
∀ {𝕜 : Type u_1} {α : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : DecidableEq α] {k : ℕ}
{𝒜 : Finset (Finset α)} [inst_2 : Fintype α],
k ≤ Fintype.card α →
IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜 →
((Finset.range (k + 1)).sum fun r =>
↑(𝒜.slice (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r))) ≤
↑(Finset.falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))
This theorem states a bound on any top part of the sum in Lonc-Winkler-Yaari-Milnor (LYM) inequality in terms of the size of `falling k 𝒜`. Specifically, for any linearly ordered field 𝕜 and any set 𝒜 of finite subsets of a finite set α with decidable equality, if 𝒜 is an antichain (no two distinct elements are related) with respect to the subset relation, then the sum over the range from 0 to `k+1`, where each term is the ratio of the cardinality of the `𝒜.slice (Fintype.card α - r)` to the binomial coefficient `choose (Fintype.card α - r)`, is less than or equal to the ratio of the cardinality of `falling (Fintype.card α - k) 𝒜` to the binomial coefficient `choose (Fintype.card α - k)`. Here, `falling k 𝒜` is the set of all subsets of 𝒜 of size `k`, and `𝒜.slice n` returns the set of all subsets of 𝒜 of size `n`.
More concisely: For any linearly ordered field 𝕜 and finite set α with decidable equality, if 𝒜 is an antichain of finite subsets of α and the sum of ratios of the cardinality of 𝒜.slice (|α| - r) to the binomial coefficient choose (|α| - r) for r from 0 to k+1 is less than or equal to the ratio of the cardinality of falling k 𝒜 to the binomial coefficient choose (|α| - k).
|
Finset.card_mul_le_card_shadow_mul
theorem Finset.card_mul_le_card_shadow_mul :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
Set.Sized r ↑𝒜 → 𝒜.card * r ≤ 𝒜.shadow.card * (Fintype.card α - r + 1)
This is the "downward local LYM inequality" theorem, which states that for any type `α` with decidable equality and finite elements, for any `𝒜` which is a set of finsets of `α` and any natural number `r`, if every finset in `𝒜` has size `r` (denoted by `Set.Sized r ↑𝒜`), then the product of the cardinality of `𝒜` and `r` is less than or equal to the product of the cardinality of the "shadow" of `𝒜` (denoted by `𝒜.shadow.card`) and the quantity obtained by subtracting `r` from the cardinality of `α` and then adding 1. In mathematical terms, if `𝒜` is a subset of `α` such that every element of `𝒜` is a finset of `α` of size `r`, then `|𝒜| * r ≤ |∂𝒜| * (|α| - r + 1)`, where `|.|` denotes cardinality and `∂𝒜` represents the "shadow" of `𝒜`.
More concisely: For any set `𝒜` of finsets of type `α` with decidable equality and finite elements, if every finset in `𝒜` has size `r` and `𝒜` is a subset of `α`, then the product of `|𝒜|` and `r` is less than or equal to the product of `|∂𝒜|` and `(|α| - r + 1)`, where `|.|` denotes cardinality and `∂𝒜` is the shadow of `𝒜`.
|
Finset.IsAntichain.disjoint_slice_shadow_falling
theorem Finset.IsAntichain.disjoint_slice_shadow_falling :
∀ {α : Type u_2} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {m n : ℕ},
IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜 → Disjoint (𝒜.slice m) (Finset.falling n 𝒜).shadow
The theorem states that for any type `α` with decidable equality and for any `𝒜` which is a finset of finsets of `α`, and any natural numbers `m` and `n`, if `𝒜` is an antichain, meaning no two distinct elements of it are related, then the `m`-slices of `𝒜` are disjoint from the shadow of `n`-sized subsets of `𝒜`. Here, "disjoint" means that the infimum of any element in the `m`-slices of `𝒜` and any element in the shadow of `n`-sized subsets of `𝒜` is the bottom element of the order. The "shadow" of a set is the set of all elements that can be obtained by removing one element from an element of the original set, and "falling" is the operation that gives all the `n`-sized subsets of a set. So, in essence, this theorem is about certain subsets of an antichain being disjoint from certain smaller subsets.
More concisely: For any antichain 𝒜 of decidably equal types α, the m-slices of 𝒜 are disjoint from the shadows of n-sized subsets of 𝒜, meaning their infimum is the bottom element for all elements from these sets.
|
Finset.sized_falling
theorem Finset.sized_falling :
∀ {α : Type u_2} [inst : DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)), Set.Sized k ↑(Finset.falling k 𝒜) := by
sorry
The theorem `Finset.sized_falling` states that for any type `α` with decidable equality and any natural number `k`, given a finset `𝒜` of finsets of `α`, every finset in the finset resulting from applying `Finset.falling` operation on `𝒜` with `k` has size `k`. In other words, it asserts that the `Finset.falling` operation on `𝒜` results in a finset where all its elements (which are finsets of `α`) have a cardinality of `k`. This operation essentially generates all subsets of elements in `𝒜` that have a size of `k`.
More concisely: For any type `α` with decidable equality and natural number `k`, `Finset.falling 𝒜 k` is a finset of `α` subsets with cardinality `k`, where `𝒜` is a finset of `α` finsets.
|