Dedekind numbers

DefinitionDedekind numbers#✓fully proved

For a natural number \(n\), the Dedekind number \(M(n)\) is the number of antichains with respect to inclusion among the subsets of the \(n\)-element set \(\{0, 1, \dots, n-1\}\), that is, of families of subsets in which no member is contained in a different member; the empty family and the family \(\{\emptyset\}\) are counted.

noncomputable def antichainCount (n : ℕ) : ℕ :=
  {F : Finset (Finset (Fin n)) | IsAntichain (· ⊆ ·) (F : Set (Finset (Fin n)))}.ncard

Used by 1

Used byErdős Problem 497: the asymptotic statement for Dedekind numbers

DefinitionErdős Problem 497: the asymptotic statement for Dedekind numbers#✓fully proved

Let \(M(n)\) be the number of antichains with respect to inclusion among the subsets of an \(n\)-element set (the Dedekind number). The statement is that \(\log_2 M(n) / \binom{n}{\lfloor n/2 \rfloor} \to 1\) as \(n \to \infty\); equivalently, \(M(n) = 2^{(1 + o(1)) \binom{n}{\lfloor n/2 \rfloor}}\).

def antichainCountLogAsymptotic : Prop :=
  Filter.Tendsto (fun n : ℕ => Real.logb 2 (antichainCount n) / (n.choose (n / 2) : ℝ))
    Filter.atTop (nhds 1)

Uses 1 · Used by 1

Statement usesDedekind numbers

Used byKleitman's theorem on Dedekind numbers

TheoremKleitman's theorem on Dedekind numbers#●ready to prove

Let \(M(n)\) be the number of antichains with respect to inclusion among the subsets of an \(n\)-element set. Then \(\log_2 M(n) / \binom{n}{\lfloor n/2 \rfloor} \to 1\) as \(n \to \infty\); that is, \(M(n) = 2^{(1 + o(1)) \binom{n}{\lfloor n/2 \rfloor}}\).

public theorem_wanted antichainCountLogAsymptotic_holds : antichainCountLogAsymptotic

Sources

• T. F. Bloom, Erdős Problems, Problem #497, https://www.erdosproblems.com/497 (status SOLVED (LEAN)); resolution: D. Kleitman, On Dedekind's problem: the number of monotone Boolean functions, Proc. Amer. Math. Soc. (1969), 677-682, erdosproblems.com/497: resolved by Kleitman, the number is 2^{(1 + o(1)) C(n, ⌊n/2⌋)}, https://www.erdosproblems.com/497.

Uses 1

Statement usesErdős Problem 497: the asymptotic statement for Dedekind numbers

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.