Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Positivity certificates for linear recurrences

Alaa Ibrahim, Bruno Salvy

TL;DR

Given a $P$-finite sequence defined by a recurrence of $Poincaré$ type with a unique simple dominant eigenvalue, the paper develops an algorithm to decide positivity of the sequence. The method uses a matrix-first-order formulation $U_{n+1}=A(n)U_n$, a convergence result of Friedland, and a cone-based positivity certificate encoded by a quadruple $(T,r,N,m)$ to certify positivity via a finite inductive argument. For generic initial conditions, the algorithm either proves positivity or certifies non-positivity, with complexity singly exponential in the order. The certificate reduces the verification to checking finitely many univariate polynomial sign conditions (via Sturm sequences) and to a finite induction on a convex cone, enabling automatic proofs and contributing to the decidability landscape for $P$-finite recurrences. The work also discusses limitations (non-generic cases may fail to terminate) and outlines potential extensions to multiple dominant eigenvalues or parametric recurrences.

Abstract

We consider linear recurrences with polynomial coefficients of Poincaré type and with a unique simple dominant eigenvalue. We give an algorithm that proves or disproves positivity of solutions provided the initial conditions satisfy a precisely defined genericity condition. For positive sequences, the algorithm produces a certificate of positivity that is a data-structure for a proof by induction. This induction works by showing that an explicitly computed cone is contracted by the iteration of the recurrence.

Positivity certificates for linear recurrences

TL;DR

Given a -finite sequence defined by a recurrence of type with a unique simple dominant eigenvalue, the paper develops an algorithm to decide positivity of the sequence. The method uses a matrix-first-order formulation , a convergence result of Friedland, and a cone-based positivity certificate encoded by a quadruple to certify positivity via a finite inductive argument. For generic initial conditions, the algorithm either proves positivity or certifies non-positivity, with complexity singly exponential in the order. The certificate reduces the verification to checking finitely many univariate polynomial sign conditions (via Sturm sequences) and to a finite induction on a convex cone, enabling automatic proofs and contributing to the decidability landscape for -finite recurrences. The work also discusses limitations (non-generic cases may fail to terminate) and outlines potential extensions to multiple dominant eigenvalues or parametric recurrences.

Abstract

We consider linear recurrences with polynomial coefficients of Poincaré type and with a unique simple dominant eigenvalue. We give an algorithm that proves or disproves positivity of solutions provided the initial conditions satisfy a precisely defined genericity condition. For positive sequences, the algorithm produces a certificate of positivity that is a data-structure for a proof by induction. This induction works by showing that an explicitly computed cone is contracted by the iteration of the recurrence.
Paper Structure (15 sections, 6 theorems, 35 equations, 1 figure, 1 algorithm)

This paper contains 15 sections, 6 theorems, 35 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Previous works
  3. Contributions
  4. Background
  5. Algebraic coefficients
  6. Dominant eigenvalues
  7. Asymptotics
  8. Positivity certificates
  9. Certificates and their verification
  10. Complexity questions
  11. Two examples of certificate verification
  12. Convergent contractions
  13. Algorithm and proof
  14. Conclusion and Future Works
  15. Acknowledgements.

Key Result

Theorem 1

Let $A(n)$ be in $\operatorname{GL}_d(\mathbb C)$ for $n\in\mathbb N$ and tend to a finite limit $A$ as $n\rightarrow\infty$, such that $A$ has exactly one dominant eigenvalue $\lambda$. Then there exist two nonzero vectors $v,w$ and a sequence of real numbers $\theta_n$ such that $Av=\lambda v$ and A vector of initial conditions $U_0$ is called generic when $w^\mathsf{T}U_0\neq0$.

Figures (1)

  • Figure 1: The first values of $U_n$ in the examples of \ref{['subsec:example']} (in red), together with the corresponding cones $T^{-1}(B_r(v))$ (in black or blue). In both cases, the dimension is decreased by scaling the vectors $U_n$ so that their last coordinate is 1 and by taking the intersection of the cone with the hyperplane setting the last coordinate to 1.

Theorems & Definitions (18)

  • Example 1
  • Example 2
  • Definition 1
  • Definition 2: Dominant eigenvalues
  • Example 3
  • Theorem 1: Friedland Friedland2006
  • Example 4
  • Definition 3
  • Theorem 2
  • Corollary 1
  • ...and 8 more