Riordan numbers

DefinitionRiordan numbers#✓fully proved

For a natural number \(n\), the \(n\)-th Riordan number is the integer

\[r_n = \sum_{k=0}^{n} (-1)^{n-k} \binom{n}{k} C_k,\]

where \(C_k\) is the \(k\)-th Catalan number.

def riordanNumber (n : Nat) : Int :=
  ∑ k ∈ Finset.range (n + 1),
    (-1 : Int) ^ (n - k) * ((n.choose k : Int) * ((catalan k : Int)))
Sources
  • closed form (Kirgizov lines 436-438).
Used by 3

TheoremRiordan numbers as an alternating Catalan sum#✓fully proved

For every natural number \(n\), the \(n\)-th Riordan number \(r_n\) equals

\[\sum_{k=0}^{n} (-1)^{n-k} \binom{n}{k} C_k,\]

where \(C_k\) is the \(k\)-th Catalan number.

theorem riordanNumber_eq_sum (n : Nat) :
    riordanNumber n =
      ∑ k ∈ Finset.range (n + 1),
        (-1 : Int) ^ (n - k) * ((n.choose k : Int) * ((catalan k : Int)))
Uses 1
Statement usesRiordan numbers
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.