Elimination of Variables in Linear Solvable Polynomial Algebras and ∂-Holonomicity

Let k be a field of characteristic 0. Based on the Gelfand–Kirillov dimension computation of modules over solvable polynomial k-algebras, where solvable polynomial algebras are in the sense of A. Kandri-Rody and V. Weispfenning (1990, J. Symbolic Comput.9, 1–26), we prove that the elimination lemma, obtained from D. Zeilberger (1990, J. Comput. Appl. Math.32, 321–368) by using holonomic modules over the Weyl algebra An(k) and used in the automatic proving of special function identities, holds for a class of solvable polynomial k-algebras without any “holonomicity” restriction. This opens a way to the solution of the extension/contraction problem stemming from the automatic proving of multivariate identities with respect to the ∂-finiteness in the sense of F. Chyzak and B. Salvy (1998, J. Symbolic Comput.26, 187–227). It also yields a ∂-holonomicity so that automatic proving of multivariate identities may be dealt with by manipulating polynomial function coefficients instead of rational functions.