Discovering and Proving Infinite Pochhammer Sum Identities

We consider nested sums involving the Pochhammer symbol at infinity and rewrite them in terms of a small set of constants, such as powers of or zeta values. In order to perform these simplifications, we view the series as specializations of generating series. For these generating series, we derive integral representations in terms of root-valued iterated integrals or directly in terms of cyclotomic harmonic polylogarithms. Using substitutions, we express the root-valued iterated integrals as cyclotomic harmonic polylogarithms. Finally, by applying known relations among the cyclotomic harmonic polylogarithms, we derive expressions in terms of several constants. We provide an algorithimic machinery to prove identities which so far could only be proved using classical hypergeometric approaches. These methods are implemented in the computer algebra package HarmonicSums.