Recurrences of the Catalan numbers

Mathlib defines catalan by the convolution recurrence and proves (n + 1) * catalan n = Nat.centralBinom n. Combined with the ratio recurrence of the central binomial coefficients, this gives the first-order recurrence (n + 2) * catalan (n + 1) = 2 * (2 * n + 1) * catalan n. This is the form in which Catalan numbers arise as solutions of linear moment recurrences, such as the even moments of the semicircle law.

The signed Catalan numbers (-1)^k C_k satisfy the Catalan recurrence up to a sign: ∑_{i ≤ k} (-1)^i C_i (-1)^(k-i) C_(k-i) = (-1)^k C_(k+1). This is the recurrence satisfied by the Möbius function μ(0̂, 1̂) of the lattice of noncrossing partitions.

Main results

• Nat.catalan_le_four_pow — the exponential bound Cₙ ≤ 4ⁿ.
• Nat.add_two_mul_catalan_succ — the first-order recurrence (n + 2) Cₙ₊₁ = 2 (2n + 1) Cₙ.
• TauCeti.sum_range_neg_one_pow_mul_catalan — the convolution of the signed Catalan numbers.

theorem Nat.catalan_le_four_pow (n : ℕ) : catalan n ≤ 4 ^ n

The Catalan numbers have exponential growth bounded by 4 ^ n.

theorem Nat.add_two_mul_catalan_succ (n : ℕ) : (n + 2) * catalan (n + 1) = 2 * (2 * n + 1) * catalan n

The first-order recurrence (n + 2) Cₙ₊₁ = 2 (2n + 1) Cₙ of the Catalan numbers.

theorem TauCeti.sum_range_neg_one_pow_mul_catalan {R : Type u_1} [CommRing R] (k : ℕ) : ∑ i ∈ Finset.range (k + 1), (-1) ^ i * ↑(catalan i) * ((-1) ^ (k - i) * ↑(catalan (k - i))) = (-1) ^ k * ↑(catalan (k + 1))

The convolution of the signed Catalan numbers: ∑_{i ≤ k} (-1)^i C_i (-1)^(k-i) C_(k-i) = (-1)^k C_(k+1).