Catalan numbers

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

Created on 2022-03-21.
Last modified on 2023-05-13.

module elementary-number-theory.catalan-numbers where
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


The Catalan numbers are a sequence of natural numbers that occur in several combinatorics problems.


catalan-numbers :   
catalan-numbers =
  strong-ind-ℕ  _  ) (succ-ℕ zero-ℕ)
    ( λ k C 
      sum-Fin-ℕ k
        ( λ i 
            ( 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))))))

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

Recent changes