Catalan numbers #
The Catalan numbers (http://oeis.org/A000108) are probably the most ubiquitous sequence of integers in mathematics. They enumerate several important objects like binary trees, Dyck paths, and triangulations of convex polygons.
Main definitions #
catalan n
: then
th Catalan number, defined recursively ascatalan (n + 1) = ∑ i : fin n.succ, catalan i * catalan (n - i)
.
Main results #
catalan_eq_central_binom_div
: The explicit formula for the Catalan number using the central binomial coefficient,catalan n = nat.central_binom n / (n + 1)
.
Implementation details #
The proof of catalan_eq_central_binom_div
follows
https://math.stackexchange.com/questions/3304415/catalan-numbers-algebraic-proof-of-the-recurrence-relation
TODO #
- Prove that the Catalan numbers enumerate many interesting objects.
- Provide the many variants of Catalan numbers, e.g. associated to complex reflection groups, Fuss-Catalan, etc.