Computing error bounds for asymptotic expansions of regular p-recursive sequences

Over the last several decades, improvements in the fields of ana-lytic combinatorics and computer algebra have made determining the asymp-totic behaviour of sequences satisfying linear recurrence relations with poly-nomial coefficients largely a matter of routine, under assumptions that hold often in practice. The algorithms involved typically take a sequence, encoded by a recurrence relation and initial terms, and return the leading terms in an asymptotic expansion up to a big-O error term. Less studied, however, are ef-fective techniques giving an explicit bound on asymptotic error terms. Among other things, such explicit bounds typically allow the user to automatically prove sequence positivity (an active area of enumerative and algebraic combi-natorics) by exhibiting an index when positive leading asymptotic behaviour dominates any error terms.In this article, we present a practical algorithm for computing such asymp-totic approximations with rigorous error bounds, under the assumption that the generating series of the sequence is a solution of a differential equation with regular (Fuchsian) dominant singularities. Our algorithm approximately follows the singularity analysis method of Flajolet and Odlyzko [SIAM J. Dis-crete Math. 3 (1990), pp. 216-240], except that all big-O terms involved in the derivation of the asymptotic expansion are replaced by explicit error terms. The computation of the error terms combines analytic bounds from the liter-ature with effective techniques from rigorous numerics and computer algebra. We implement our algorithm in the SageMath computer algebra system and exhibit its use on a variety of applications (including our original motivating example, solution uniqueness in the Canham model for the shape of genus one biomembranes).