# mathlib3documentation

combinatorics.catalan

# Catalan numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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: the nth Catalan number, defined recursively as catalan (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).

• trees_of_nodes_eq_card_eq_catalan: The number of binary trees with n internal nodes is catalan n

## 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.
def catalan  :

The recursive definition of the sequence of Catalan numbers: catalan (n + 1) = ∑ i : fin n.succ, catalan i * catalan (n - i)

Equations
@[simp]
theorem catalan_zero  :
= 1
theorem catalan_succ (n : ) :
catalan (n + 1) = finset.univ.sum (λ (i : fin n.succ), * catalan (n - i))
theorem catalan_succ' (n : ) :
catalan (n + 1) = (λ (ij : × ), catalan ij.fst * catalan ij.snd)
@[simp]
theorem catalan_one  :
= 1
theorem catalan_two  :
= 2
theorem catalan_three  :
= 5
@[reducible]
def tree.pairwise_node (a b : finset (tree unit)) :

Given two finsets, find all trees that can be formed with left child in a and right child in b

Equations

A finset of all trees with n nodes. See mem_trees_of_nodes_eq

Equations
• = (λ (ijh : {x // ,
@[simp]
theorem tree.trees_of_nodes_eq_succ (n : ) :
= (λ (ij : × ),
@[simp]
theorem tree.mem_trees_of_nodes_eq {x : tree unit} {n : } :
@[simp, norm_cast]
theorem tree.coe_trees_of_nodes_eq (n : ) :
= {x : | x.num_nodes = n}