Catalan generating function via compositional inversion
substInv_X_sub_X_sq_eq_catalan
Submitter: Kim Morrison.
Notes: The compositional inverse of X - X² is the generating function for Catalan numbers. This is a classical application of Lagrange inversion in enumerative combinatorics, connecting formal power series inversion to Dyck paths, binary trees, and triangulations.
Source: E. Catalan, Note sur une équation aux différences finies, 1838; J.-L. Lagrange, Nouvelle méthode pour résoudre les équations littérales, 1770.
Informal solution: The compositional inverse C(x) satisfies C - C² = x, giving C = (1 - √(1-4x))/2. By the binomial series, its coefficients are the Catalan numbers C_n = (2n choose n)/(n+1).
theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := n:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2))
n:ℕ⊢ Invertible 1; All goals completed! 🐙
coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
(Nat.choose (2 * n) n : ℚ) / (↑n + 1) := n:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1)
All goals completed! 🐙