Fubini numbers
DefinitionFubini numbers#✓fully proved
The Fubini number (ordered Bell number) of a natural number \(n\) is \(F(n) = \sum_{k=0}^{n} S(n,k)\, k!\), where \(S(n,k)\) is the Stirling number of the second kind.
\(F(n)\) counts the weak orderings, equivalently the ordered set partitions, of an \(n\)-element set.
def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kUsed by 10
TheoremFubini numbers as sums of Stirling numbers#✓fully proved
For every natural number \(n\), the Fubini number \(F(n)\) equals \(\sum_{k=0}^{n} S(n,k)\, k!\), where \(S(n,k)\) is the Stirling number of the second kind.
theorem fubiniNumber_eq_sum (n : Nat) :
fubiniNumber n =
∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kdef fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
Uses 1 · Used by 2
TheoremFubini number of zero#✓fully proved
The Fubini number \(F(0)\) equals \(1\): the empty set has exactly one weak ordering.
@[simp]
theorem fubiniNumber_zero : fubiniNumber 0 = 1def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
Uses 1
TheoremFubini number of one#✓fully proved
The Fubini number \(F(1)\) equals \(1\).
@[simp]
theorem fubiniNumber_one : fubiniNumber 1 = 1def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
Uses 1
TheoremFubini number of two#✓fully proved
The Fubini number \(F(2)\) equals \(3\).
theorem fubiniNumber_two : fubiniNumber 2 = 3def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
Uses 1
TheoremFubini number of three#✓fully proved
The Fubini number \(F(3)\) equals \(13\).
theorem fubiniNumber_three : fubiniNumber 3 = 13def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
Uses 1
TheoremAlternating recurrence for the Fubini numbers#✓fully proved
For every natural number \(n\), the Fubini number \(F(n)\) satisfies
where \(s(n, k)\) is the signed Stirling number of the first kind.
theorem fubiniNumber_eq_factorial_sub_sum_signed_stirling (n : ℕ) : (fubiniNumber n : ℤ) =
(Nat.factorial n : ℤ) -
∑ j ∈ Finset.Icc 1 n, signedStirlingFirst n (n - j) * (fubiniNumber (n - j) : ℤ)def fubiniNumber : Nat → Nat :=
fun n => ∑ k ∈ Finset.range (n + 1), Nat.stirlingSecond n k * Nat.factorial kMathlibExt/Combinatorics/Enumerative/FubiniNumber.lean:32
def signedStirlingFirst : ℕ → ℕ → ℤ :=
fun n k => (-1 : ℤ) ^ (n - k) * (Nat.stirlingFirst n k : ℤ)MathlibExt/Combinatorics/Enumerative/SignedStirlingFirst.lean:20
Sources
- Benjamin Schreyer, "Rigged Horse Numbers and their Modular Periodicity," Journal of Integer Sequences 28 (2025), Article 25.4.1, Corollary, lines 253–257, https://cs.uwaterloo.ca/journals/JIS/VOL28/Schreyer/schreyer7.tex
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.