Riordan numbers
DefinitionRiordan numbers#✓fully proved
MetaMathlibExt.riordanNumber
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
Sources
- closed form (Kirgizov lines 436-438).
TheoremRiordan numbers as an alternating Catalan sum#✓fully proved
MetaMathlibExt.riordanNumber_eq_sum
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)))
def riordanNumber (n : Nat) : Int :=
∑ k ∈ Finset.range (n + 1),
(-1 : Int) ^ (n - k) * ((n.choose k : Int) * ((catalan k : Int)))
MathlibExt/Combinatorics/Enumerative/RiordanNumber.lean:24
Uses 1
Statement usesRiordan numbers
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.