Travail en collaboration avec Thomas Alazard.

À la fin du 19e siècle, lors de l’étude du problème des 3 corps (le système Soleil-Terre-Lune), H. Poincaré fut amené à regarder la dynamique des applications des surfaces qui préservent l’aire au voisinage de leurs points fixes. Ensuite, dans les années 30, Birkhoff commença l’étude des applications twists conservatives de l’anneau 2-dimensionnel qui servent à modéliser la situation envisagée par Poincaré, mais aussi les mouvements d’une boule dans une table de billard convexe ou le mouvement d’un pendule rigide. Après avoir rappelé cela et expliqué précisément ce qu’est un twist conservatif, j’expliquerai certains résultats dûs à divers mathématiciens comme Birkhoff, Kolmogorov-Arnold et Moser, Aubry, Mather, Herman, Le Calvez qui concernent : -la stabilité, et plus précisèment les courbes invariantes ; -l’instabilité, et plus précisément les orbites qui se promènent entre différentes courbes invariantes.

Les assistants à la preuve sont une famille relativement méconnue de logiciels pour faire des mathématiques avec un ordinateur. Ils permettent à leurs utilisateurs de vérifier avec la plus grande certitude possible la validité des démonstrations qu’ils ont préalablement décrites à la machine. Le premier grand succès de cette approche de la vérification mathématique date sans doute de 2005, lorsque la preuve du théorème des quatre couleurs a été formalisée complètement à l’aide d’un tel assistant à la preuve. La seule preuve de ce résultat connue à ce jour mélange des arguments de combinatoire avec des calculs importants, impossible à effectuer à la main, qui confèrent pour certains un statut controversé à la démonstration. En septembre 2012, une preuve du théorème de l’ordre impair (Feit-Thompson, 1963), pierre angulaire de la classification des groupes simples finis, a également été vérifiée par un assistant à la preuve. Cette preuve ne repose aucunement sur des arguments calculatoires. Il s’agit d’une combinaison sophistiquée de théories algébriques, et la preuve de Feit et Thompson fut en son temps l’une les plus longues de la littérature mathématique.

Nous allons discuter la notion de réductibilité (souvent appelée “théorie de Floquet” ) pour les co-cycles quasi-périodiques. Un cocycle quasi-périodique est le nom commun d’un système linéaire d’équations différentielles ou de différences, dépendant du temps de façon quasi-périodique. De tels systèmes apparaissent à la fois dans la théorie linéaire (l’équation stationnaire de Schrödinger) et dans la théorie non-linéaire (l’équation variationnelle pour une solution quasi-périodique) et la réductibilitée est une propriété naturelle, au moins pour les systèmes proches du cas constant. Pour les EDO (=dimension finie) nous avons une image détaillée et assez complète de cette propriété dans le régime perturbatif : sous des conditions assez générales, tout système est “presque réductible” et “presque tout" systéme est réductible. Pour les EDP (= dimension infinie) l’état de notre connaissance est bien plus lacunaire, mais il y a quelques résultats