Automatic positivity proofs for P-finite sequences

De nombreuses inégalités en combinatoire ou entre fonctions spéciales se ramènent à une question élémentaire : décider la positivité des termes d'une suite définie par une récurrence linéaire à coefficients polynomiaux avec conditions initiales. La question de positivité apparaît également dans des domaines variés tels que la vérification de code, l'analyse d'erreur ou la modélisation en biologie. Cette thèse porte sur la conception et la validation d'algorithmes efficaces pour la preuve automatique de la positivité de telles suites. Ce problème est généralement difficile : même pour les récurrences à coefficients constants, la décidabilité reste liée à des questions classiques non résolues en théorie des nombres. Dans le cas plus général des coefficients polynomiaux, seuls des résultats partiels étaient connus pour les récurrences d'ordre 2 ou 3, sous certaines hypothèses sur les racines du polynôme caractéristique et les conditions initiales. L'objectif de cette thèse est d'étendre ces résultats dans le cadre des coefficients polynomiaux à des ordres arbitraires. La contribution repose sur une approche géométrique: La positivité est établie en montrant que les termes de la suite restent dans des cônes convexes contractés, construits à l'aide d'une généralisation de la théorie de Perron-Frobenius aux cônes. Cette méthode permet d'établir la décidabilité de la positivité pour une large classe de récurrences, et se révèle applicable à de nombreux exemples issus de la littérature.