mathlib3 documentation

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

catalan (n + 1) = finset.univ.sum (λ (i : fin n.succ), catalan ↑i * catalan (n - ↑i))
catalan 0 = 1

@[simp]

theorem catalan_zero :

theorem catalan_succ (n : ℕ) :

catalan (n + 1) = finset.univ.sum (λ (i : fin n.succ), catalan ↑i * catalan (n - ↑i))

theorem catalan_succ' (n : ℕ) :

catalan (n + 1) = (finset.nat.antidiagonal n).sum (λ (ij : ℕ × ℕ), catalan ij.fst * catalan ij.snd)

@[simp]

theorem catalan_one :

theorem catalan_eq_central_binom_div (n : ℕ) :

catalan n = n.central_binom / (n + 1)

theorem succ_mul_catalan_eq_central_binom (n : ℕ) :

(n + 1) * catalan n = n.central_binom

theorem catalan_two :

theorem catalan_three :

@[reducible]

def tree.pairwise_node (a 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.pairwise_node a b = finset.map {to_fun := λ (x : tree unit × tree unit), tree.node unit.star() x.fst x.snd, inj' := tree.pairwise_node._proof_1} (a ×ˢ b)

def tree.trees_of_num_nodes_eq :

ℕ → finset (tree unit)

A finset of all trees with n nodes. See mem_trees_of_nodes_eq

Equations

tree.trees_of_num_nodes_eq (n + 1) = (finset.nat.antidiagonal n).attach.bUnion (λ (ijh : {x // x ∈ finset.nat.antidiagonal n}), tree.pairwise_node (tree.trees_of_num_nodes_eq ijh.val.fst) (tree.trees_of_num_nodes_eq ijh.val.snd))
tree.trees_of_num_nodes_eq 0 = {tree.nil}

@[simp]

theorem tree.trees_of_nodes_eq_zero :

tree.trees_of_num_nodes_eq 0 = {tree.nil}

theorem tree.trees_of_nodes_eq_succ (n : ℕ) :

tree.trees_of_num_nodes_eq (n + 1) = (finset.nat.antidiagonal n).bUnion (λ (ij : ℕ × ℕ), tree.pairwise_node (tree.trees_of_num_nodes_eq ij.fst) (tree.trees_of_num_nodes_eq ij.snd))

@[simp]

theorem tree.mem_trees_of_nodes_eq {x : tree unit} {n : ℕ} :

x ∈ tree.trees_of_num_nodes_eq n ↔ x.num_nodes = n

theorem tree.mem_trees_of_nodes_eq_num_nodes (x : tree unit) :

x ∈ tree.trees_of_num_nodes_eq x.num_nodes

@[simp, norm_cast]

theorem tree.coe_trees_of_nodes_eq (n : ℕ) :

↑(tree.trees_of_num_nodes_eq n) = {x : tree unit | x.num_nodes = n}

theorem tree.trees_of_nodes_eq_card_eq_catalan (n : ℕ) :

(tree.trees_of_num_nodes_eq n).card = catalan n