AhlswedeZhang.infSum_eq_one
theorem AhlswedeZhang.infSum_eq_one :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {𝒜 : Finset (Finset α)} [inst_2 : Nonempty α],
𝒜.Nonempty → ∅ ∉ 𝒜 → AhlswedeZhang.infSum 𝒜 = 1
The **Ahlswede-Zhang Identity** theorem states that given a nonempty universe `α` of finite type, with decidable equality, and a nonempty family `𝒜` of nonempty subsets of `α`, the weighted sum of the sizes of the truncated infima of the family `𝒜` equals to one. The weight of each subset from the family is defined as the reciprocal of the product of the cardinality of the subset and the binomial coefficient "cardinality of `α` choose cardinality of the subset". The term "truncated infima" refers to the minimum element of each subset, truncated to the given universe.
More concisely: Given a finite universe with decidable equality and a family of nonempty subsets, the weighted sum of the sizes of their truncated minima equals 1, where the weight of each subset is the reciprocal of its size multiplied by the binomial coefficient of the universe's size and its subset's size.
|
Finset.truncatedSup_of_not_mem
theorem Finset.truncatedSup_of_not_mem :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] [inst_2 : DecidableRel fun x x_1 => x ≤ x_1]
{s : Finset α} {a : α}, a ∉ lowerClosure ↑s → s.truncatedSup a = ⊤
The theorem `Finset.truncatedSup_of_not_mem` states that for any type `α` that forms a semilattice with a top element (`OrderTop α`) and a decidable relation (`DecidableRel`) for less than or equal to (`x ≤ x_1`), any given set of elements from `α` (`s : Finset α`) and an element `a : α`, if `a` is not present in the least lower set containing the set `s` (i.e. `a ∉ lowerClosure ↑s`), then the supremum of the elements of `s` that are less than `a` (computed using `Finset.truncatedSup s a`) is equal to the top element of the semilattice (`⊤`).
More concisely: If `α` is a semilattice with a top element and `s` is a finite subset of `α` such that `a ∉ lowerClosure s` for some `a ∈ α`, then `Finset.truncatedSup s a = ⊤`.
|
Finset.truncatedInf_of_not_mem
theorem Finset.truncatedInf_of_not_mem :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : BoundedOrder α] [inst_2 : DecidableRel fun x x_1 => x ≤ x_1]
{s : Finset α} {a : α}, a ∉ upperClosure ↑s → s.truncatedInf a = ⊥
The theorem `Finset.truncatedInf_of_not_mem` states that for any given type `α` with a semi-lattice structure and a bounded order, along with a decidable relation for less than or equal to, for any finite set `s` of type `α` and any element `a` of type `α`, if `a` is not in the upper closure of `s`, then the truncated infimum of `s` and `a` is the bottom element of the bounded order. In other words, if `a` is not an upper bound of any element in `s`, the greatest element of `s` that is less than or equal to `a` does not exist, so we return the smallest possible value.
More concisely: If `α` is a type with a semi-lattice structure and a decidable order relation, and `s` is a finite set of `α`, then `∀a ∈ α, a ∉ ⨆s �Rightarrow ⨋s ⊥`. Here, `⨆s` is the upper closure of `s`, `⨋s` is the infimum of `s`, and `⊥` is the bottom element of the bounded order on `α`.
|
AhlswedeZhang.infSum_compls_add_supSum
theorem AhlswedeZhang.infSum_compls_add_supSum :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Nonempty α] (𝒜 : Finset (Finset α)),
AhlswedeZhang.infSum 𝒜.compls + AhlswedeZhang.supSum 𝒜 =
(↑(Fintype.card α) * (Finset.range (Fintype.card α)).sum fun k => (↑k)⁻¹) + 1
The Ahlswede-Zhang Identity states that for any finite type `α` with decidable equality and at least one element, and any set `𝒜` of finite subsets of `α`, the sum of the weighted sizes of the truncated infima of the complements of `𝒜` and the weighted sizes of the truncated suprema of `𝒜` is equal to the product of the size of `α` and the sum of the reciprocals of the numbers less than the size of `α`, plus 1. The weights are determined by the size of the truncated infima/suprema, the size of the subset, and the number of ways to choose the subset from `α`.
More concisely: For any finite type `α` with decidable equality and at least one element, and any set `𝒜` of finite subsets of `α`, the sum of the weighted sizes of the truncated infima of the complements and suprema of `𝒜` equals the product of `α`'s size and the sum of the reciprocals of `α`'s cardinality minus one. The weights are determined by the sizes of the infima/suprema, subset sizes, and subset choices.
|
Finset.truncatedSup_of_mem
theorem Finset.truncatedSup_of_mem :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] [inst_2 : DecidableRel fun x x_1 => x ≤ x_1]
{s : Finset α} {a : α} (h : a ∈ lowerClosure ↑s),
s.truncatedSup a = (Finset.filter (fun b => a ≤ b) s).sup' ⋯ id
This theorem, `Finset.truncatedSup_of_mem`, states that for any given type `α` that has a semilattice sup operation, a top order, and a decidable relation for `≤`, given a finite set `s` of type `α`, and an element `a` of type `α` that belongs to the lower closure of `s`, the truncated sup of `s` and `a` is equal to the supremum of the set obtained by filtering `s` to only keep elements `b` such that `a ≤ b`.
More concisely: For any semilattice `α` with top element, a finite set `s �rivial subset α`, and `a ∈ cl_≤(s)`, we have `sup (s ∩ {b : α | a ≤ b}) = truncated_sup s a`.
|
Finset.truncatedInf_of_mem
theorem Finset.truncatedInf_of_mem :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : BoundedOrder α] [inst_2 : DecidableRel fun x x_1 => x ≤ x_1]
{s : Finset α} {a : α} (h : a ∈ upperClosure ↑s),
s.truncatedInf a = (Finset.filter (fun x => x ≤ a) s).inf' ⋯ id
The theorem `Finset.truncatedInf_of_mem` states that for any type `α` that is a semilattice with respect to the operation "infimum", has a bounded order, and has a decidable relation for less than or equal to operation, if a given element `a` of type `α` is in the upper closure of a finite set `s` (i.e., `a` is an upper bound of some element of `s`), then the truncated infimum of `s` and `a` is equivalent to the infimum of the set obtained by filtering `s` to include only those elements less than or equal to `a`.
This essentially means that the lower bound of the elements of `s` that are less than or equal to `a` (or the least element if it exists) is the same whether we consider it within the entire set `s` or within the subset of `s` that is less than or equal to `a`.
More concisely: If `α` is a semilattice with decidable order relation and bounded order, and `a` is an upper bound of some element in the finite set `s` of `α`, then the truncated infimum of `s` and `a` equals the infimum of `s` restricted to elements less than or equal to `a`.
|