Non-commutative Elimination in Ore Algebras Proves Multivariate Identities

Many computations involving special functions, combinatorial sequences or theirq-analogues can be performed using linear operators and simple arguments on the dimension of related vector spaces. In this article, we develop a theory of ∂-finite sequences and functions which provides a unified framework to express algorithms for computing sums and integrals and for the proof or discovery of multivariate identities. This approach is vindicated by an implementation.