The Bell numbers

Content created by Egbert Rijke.

Created on 2025-02-11.
Last modified on 2025-02-11.

module elementary-number-theory.bell-numbers where
Imports 
open import elementary-number-theory.binomial-coefficients
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers
open import elementary-number-theory.strong-induction-natural-numbers
open import elementary-number-theory.sums-of-natural-numbers

Idea

The Bell numbers count the number of ways to partition a set of size . The Bell numbers can be defined recursively by and

The Bell numbers are listed as sequence A000110 in the OEIS [OEIS].

Definitions

The Bell numbers

bell-number-ℕ : ℕ → ℕ
bell-number-ℕ =
  strong-rec-ℕ 1
    ( λ n B →
      bounded-sum-ℕ
        ( succ-ℕ n)
        ( λ k H →
          binomial-coefficient-ℕ n k *ℕ B k (leq-le-succ-ℕ k n H)))

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.

Recent changes