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

• catalan 0 = 1
• catalan (Nat.succ n) = Finset.sum Finset.univ fun (i : Fin (Nat.succ n)) => catalan ↑i * catalan (n - ↑i)

@[simp]

theorem catalan_zero : catalan 0 = 1

theorem catalan_succ (n : ℕ) : catalan (n + 1) = Finset.sum Finset.univ fun (i : Fin (Nat.succ n)) => catalan ↑i * catalan (n - ↑i)

theorem catalan_succ' (n : ℕ) : catalan (n + 1) = Finset.sum (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => catalan ij.1 * catalan ij.2

@[simp]

theorem catalan_one : catalan 1 = 1

theorem catalan_eq_centralBinom_div (n : ℕ) : catalan n = Nat.centralBinom n / (n + 1)

theorem succ_mul_catalan_eq_centralBinom (n : ℕ) : (n + 1) * catalan n = Nat.centralBinom n

theorem catalan_two : catalan 2 = 2

theorem catalan_three : catalan 3 = 5

@[reducible]

def Tree.pairwiseNode (a : Finset (Tree Unit)) (b : Finset (Tree Unit)) : Finset (Tree Unit)

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

Equations

• Tree.pairwiseNode a b = Finset.map { toFun := fun (x : Tree Unit × Tree Unit) => Tree.node () x.1 x.2, inj' := Tree.pairwiseNode.proof_1 } (a ×ˢ b)

def Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit)

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.treesOfNumNodesEq 0 = {Tree.nil}

@[simp]

theorem Tree.treesOfNumNodesEq_zero : Tree.treesOfNumNodesEq 0 = {Tree.nil}

theorem Tree.treesOfNumNodesEq_succ (n : ℕ) : Tree.treesOfNumNodesEq (n + 1) = Finset.biUnion (Finset.antidiagonal n) fun (ij : ℕ × ℕ) => Tree.pairwiseNode (Tree.treesOfNumNodesEq ij.1) (Tree.treesOfNumNodesEq ij.2)

@[simp]

theorem Tree.mem_treesOfNumNodesEq {x : Tree Unit} {n : ℕ} : x ∈ Tree.treesOfNumNodesEq n ↔ Tree.numNodes x = n

theorem Tree.mem_treesOfNumNodesEq_numNodes (x : Tree Unit) : x ∈ Tree.treesOfNumNodesEq (Tree.numNodes x)

@[simp]

theorem Tree.coe_treesOfNumNodesEq (n : ℕ) : ↑(Tree.treesOfNumNodesEq n) = {x : Tree Unit | Tree.numNodes x = n}

theorem Tree.treesOfNumNodesEq_card_eq_catalan (n : ℕ) : (Tree.treesOfNumNodesEq n).card = catalan n