Catalan numbers

TheoremCatalan numbers are at most \(4^n\)#✓fully proved

The nth Catalan number is at most 4 ^ n.

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

TheoremClosed form of the Catalan generating function#✓fully proved

Let \(C_n\) be the \(n\)th Catalan number. For every real number \(x\) with \(|x| < 1/4\) and \(x \neq 0\),

\[ \sum_{n=0}^{\infty} C_n x^n = \frac{1 - \sqrt{1 - 4x}}{2x}. \]

The hypothesis \(x \neq 0\) excludes the removable singularity of the right-hand side at \(x = 0\).

theorem catalan_generating_function_sqrt (x : ℝ) (hx : |x| < 1 / 4)
    (hx0 : x ≠ 0) :
    ∑' n : ℕ, (catalan n : ℝ) * x ^ n =
      (1 - Real.sqrt (1 - 4 * x)) / (2 * x)

Sources

• Paul Barry, "A Note on a Family of Generalized Pascal Matrices Defined by Riordan Arrays", Journal of Integer Sequences 16 (2013), Article 13.5.4, proposition lines 380–388, https://cs.uwaterloo.ca/journals/JIS/VOL16/Barry2/barry231.tex. Mathlib has PowerSeries.catalanSeries and its quadratic functional equation, but its source file explicitly lists the square-root closed form as a TODO; this theorem records the analytic closed form rather than duplicating the formal series definition.

Used by 1

Used byRamanujan's series for powers of the Catalan generating function

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.