Soutenance de Alaa IBRAHIM sous la direction de Bruno SALVY
Résumé de la thèse
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.
Behind many inequalities in combinatorics or involving special functions lies an elementary question: deciding the positivity of the terms of a sequence defined by a linear recurrence with polynomial coefficients and initial conditions, known as a P-finite sequence. The question of positivity also arises in various fields such as code verification, error analysis or modelling in biology.
This thesis focuses on finding efficient algorithms for automatically proving the positivity of P-finite sequences. This problem is generally difficult: even for recurrences with constant coefficients, decidability is still linked to classical open problems in number theory. In the more general case of polynomial coefficients, only partial results were known for recurrences of order 2 or 3, under certain assumptions about the roots of the characteristic polynomial and the initial conditions. The aim of this thesis is to extend these results in the polynomial framework to arbitrary orders.
The contribution is based on a geometric approach: positivity is established by showing that the terms of the sequence remain in contracted convex cones, constructed using a generalisation of Perron-Frobenius theory to cones. This method leads to the decidability of positivity for a large class of recurrences, and is applicable to many examples from the literature.
Gratuit
Disciplines