Catalan numbers

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-03-21.
Last modified on 2024-10-16.

module elementary-number-theory.catalan-numbers where

Imports

open import elementary-number-theory.binomial-coefficients
open import elementary-number-theory.distance-natural-numbers
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

open import univalent-combinatorics.standard-finite-types

Idea

The Catalan numbers^¶ $C_{n}$ is a sequence of natural numbers that occur in several combinatorics problems. The sequence starts

  n   0   1   2   3   4   5   6
  Cₙ  1   1   2   5  14  42 132 ⋯

The Catalan numbers may be defined by any of the formulas

$C_{n + 1} = \sum_{k = 0}^{n} C_{k} C_{n - k}$ , with $C_{0} = 1$ ,
$C_{n} = (n 2 n) - (n + 1 2 n)$ ,
$C_{n + 1} = \frac{2 ( 2 n + 1 )}{n + 2} C_{n}$ , with $C_{0} = 1$ ,
$C_{n} = \frac{1}{n + 1} (n 2 n)$ ,
$C_{n} = \frac{( 2 n )!}{( n + 1 )! n !}$ .

Where $(k n)$ are binomial coefficients and $n!$ is the factorial function.

Definitions

Inductive sum formula for the Catalan numbers

The Catalan numbers may be defined to be the sequence satisfying $C_{0} = 1$ and the recurrence relation

$C_{n + 1} = k = 0 \sum n C_{k} C_{n - k} .$

catalan-numbers : ℕ → ℕ
catalan-numbers =
  strong-ind-ℕ
    ( λ _ → ℕ)
    ( 1)
    ( λ k C →
      sum-Fin-ℕ k
        ( λ i →
          mul-ℕ
            ( C ( nat-Fin k i)
                ( leq-le-ℕ (nat-Fin k i) k (strict-upper-bound-nat-Fin k i)))
            ( C ( dist-ℕ (nat-Fin k i) k)
                ( leq-dist-ℕ
                  ( nat-Fin k i)
                  ( k)
                  ( leq-le-ℕ
                    ( nat-Fin k i)
                    ( k)
                    ( strict-upper-bound-nat-Fin k i))))))

Binomial difference formula for the Catalan numbers

The Catalan numbers may be computed as a distance between two consecutive binomial coefficients

$C_{n} = ∣ (n 2 n) - (n + 1 2 n) ∣ .$

Since $(n 2 n)$ in general is larger than or equal to $(n + 1 2 n)$ , this distance is equal to the difference

$C_{n} = (n 2 n) - (n + 1 2 n) .$

However, we prefer the use of the distance binary operation on natural numbers in general at it is a total function on natural numbers, and allows us to skip proving this inequality.

catalan-numbers-binomial : ℕ → ℕ
catalan-numbers-binomial n =
  dist-ℕ
    ( binomial-coefficient-ℕ (2 *ℕ n) n)
    ( binomial-coefficient-ℕ (2 *ℕ n) (succ-ℕ n))

External links

Catalan number at Mathswitch
Catalan number at Wikipedia
Catalan Number at Wolfram MathWorld
A000108 in the OEIS

Recent changes

2024-10-16. Fredrik Bakke. Some links in elementary number theory (#1199).
2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).