# 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

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 are a sequence of natural numbers that occur in several combinatorics problems.

## Definitions

catalan-numbers : ℕ → ℕ
catalan-numbers =
strong-ind-ℕ (λ _ → ℕ) (succ-ℕ zero-ℕ)
( λ 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))))))

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