Schröder numbers

The Schröder numbers (https://oeis.org/A006318) are a sequence of integers that appear in various combinatorial contexts.

Main definitions

• largeSchroder n: the nth large Schröder number, defined recursively as L 0 = 1 and L (n + 1) = L n + ∑ i ≤ n, L i * L (n - i).
• smallSchroder n: the nth small Schröder number, defined as S 0 = 1 and S n = L n / 2 for n > 0.

Main results

• largeSchroder_even : The large Schröder numbers are positive and even for n > 0.
• smallSchroder_succ : A recursive formula for small Schröder numbers: S (n + 1) = 3 * S n + 2 * ∑ i < n - 2, S (i + 2) * S (n - 1 - i).

Tags

Schroeder, Schroder

@[irreducible]

def Nat.largeSchroder : ℕ → ℕ

The recursive definition of the sequence of the large Schröder numbers : a (n + 1) = a n + ∑ i : Fin n.succ, a i * a (n - i)

Equations

• Nat.largeSchroder 0 = 1
• n.succ.largeSchroder = n.largeSchroder + ∑ i : Fin n.succ, (↑i).largeSchroder * (n - ↑i).largeSchroder

@[simp]

theorem Nat.largeSchroder_zero : largeSchroder 0 = 1

@[simp]

theorem Nat.largeSchroder_one : largeSchroder 1 = 2

@[simp]

theorem Nat.largeSchroder_two : largeSchroder 2 = 6

theorem Nat.largeSchroder_succ (n : ℕ) : (n + 1).largeSchroder = n.largeSchroder + ∑ i ∈ Finset.Iic n, i.largeSchroder * (n - i).largeSchroder

@[irreducible]

theorem Nat.even_largeSchroder {n : ℕ} : n ≠ 0 → Even n.largeSchroder

def Nat.smallSchroder : ℕ → ℕ

The small Schröder number is equal to : largeSchroder n = 2 * smallSchroder (n + 1), n ≥ 1

Equations

• Nat.smallSchroder 0 = 1
• Nat.smallSchroder 1 = 1
• n.succ.smallSchroder = n.largeSchroder / 2

@[simp]

theorem Nat.smallSchroder_zero : smallSchroder 0 = 1

@[simp]

theorem Nat.smallSchroder_one : smallSchroder 1 = 1

theorem Nat.smallSchroder_succ_eq_largeSchroder_div_two {n : ℕ} (h : n ≠ 0) : (n + 1).smallSchroder = n.largeSchroder / 2

theorem Nat.two_mul_smallSchroder_succ {n : ℕ} (hn : n ≠ 0) : 2 * (n + 1).smallSchroder = n.largeSchroder

theorem Nat.smallSchroder_succ {n : ℕ} (hn : 1 < n) : (n + 1).smallSchroder = 3 * n.smallSchroder + 2 * ∑ i ∈ Finset.Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder