Catalan Power Series

We introduce the Catalan generating function as a formal power series over ℕ: catalanSeries = ∑_{n ≥ 0} catalan n * X^n

Main Definitions

• PowerSeries.catalanSeries: The Catalan generating function as a power series.

Main Results

• PowerSeries.catalanSeries_one_add_X_mul_self_sq: The Catalan generating function satisfies the equation catalanSeries = 1 + X * catalanSeries ^ 2.

TODO

• Find and prove the closed formula for the Catalan generating function: C(X) = (1 - √(1 - 4X)) / (2X)

def PowerSeries.catalanSeries : PowerSeries ℕ

The Catalan generating function as a power series.

Equations

• PowerSeries.catalanSeries = PowerSeries.mk catalan

@[simp]

theorem PowerSeries.catalanSeries_coeff (n : ℕ) : (coeff n) catalanSeries = catalan n

@[simp]

theorem PowerSeries.catalanSeries_constantCoeff : constantCoeff catalanSeries = 1

theorem PowerSeries.catalanSeries_sq_mul_X_add_one : catalanSeries ^ 2 * X + 1 = catalanSeries