Holonomic sequence

Summary

A holonomic sequence, also called a P-recursive sequence, is a sequence that satisfies a linear recurrence with polynomial coefficients. A sequence is holonomic exactly when its generating function is a holonomic function. The class is closed under sums, termwise products and many other operations, which makes it the basis of automatic proofs of identities for sums. It contains the solutions of linear recurrences with constant coefficients, the factorials, the Catalan numbers and the harmonic numbers.