# Documentation

Mathlib.Combinatorics.Catalan

# 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: the nth Catalan number, defined recursively as catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i).

## Main results #

• catalan_eq_centralBinom_div : The explicit formula for the Catalan number using the central binomial coefficient, catalan n = Nat.centralBinom n / (n + 1).

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

## Implementation details #

The proof of catalan_eq_centralBinom_div follows https://math.stackexchange.com/questions/3304415

## 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
Instances For
@[simp]
theorem catalan_zero :
= 1
theorem catalan_succ (n : ) :
catalan (n + 1) = Finset.sum Finset.univ fun i => catalan i * catalan (n - i)
theorem catalan_succ' (n : ) :
catalan (n + 1) = Finset.sum () fun ij => catalan ij.fst * catalan ij.snd
@[simp]
theorem catalan_one :
= 1
theorem catalan_eq_centralBinom_div (n : ) :
= / (n + 1)
theorem catalan_two :
= 2
@[reducible]
def Tree.pairwiseNode (a : ) (b : ) :

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

Instances For

A Finset of all trees with n nodes. See mem_treesOfNodesEq

Equations
• One or more equations did not get rendered due to their size.
• = {Tree.nil}
Instances For
@[simp]
theorem Tree.treesOfNumNodesEq_zero :
= {Tree.nil}
@[simp]
theorem Tree.mem_treesOfNumNodesEq {x : } {n : } :
@[simp]
theorem Tree.coe_treesOfNumNodesEq (n : ) :
= {x | }