Schröder Numbers Power Series

This file defines lemmas and theorems about the power series for large and small Schröder numbers.

Main Definitions

• PowerSeries.largeSchroderSeries: The power series for large Schröder numbers.
• PowerSeries.smallSchroderSeries: The power series for small Schröder numbers.

Main Results

• largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq: The functional equation for the large Schröder numbers power series.

TODO

• Prove the small Schröder numbers power series.

def PowerSeries.largeSchroderSeries : PowerSeries ℕ

The power series for large Schröder numbers

Equations

• PowerSeries.largeSchroderSeries = PowerSeries.mk Nat.largeSchroder

@[simp]

theorem PowerSeries.coeff_largeSchroderSeries (n : ℕ) : (coeff n) largeSchroderSeries = n.largeSchroder

@[simp]

theorem PowerSeries.constantCoeff_largeSchroderSeries : constantCoeff largeSchroderSeries = 1

@[simp]

theorem PowerSeries.coeff_X_mul_largeSchroderSeries (n : ℕ) (hn : 0 < n) : (coeff n) (X * largeSchroderSeries) = (n - 1).largeSchroder

theorem PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq (n : ℕ) (hn : 0 < n) : (coeff n) (X * largeSchroderSeries ^ 2) = ∑ i ∈ Finset.range n, i.largeSchroder * (n - 1 - i).largeSchroder

theorem PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq : largeSchroderSeries = 1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2