Survol

[ English ]

Au cours de la dernière décennie, l'informatique rigoureusement vérifiée a été principalement appliquée à une gamme d'équations différentielles ordinaires. Nous assistons à l'émergence du champ des preuves informatiques pour les dynamiques non linéaires à dimensions infinies générées par des équations aux dérivées partielles, des équations intégrales, des équations à retard et des cartes à dimensions infinies.

Parmi les premières applications réussies de ces méthodes pour des problèmes de dimensions infinies, citons: la résolution partielle d'une conjecture de longue date pour l'équation du retard de Wright; démonstration du comportement spatio-temporel dans l'EDP Kuramoto-Sivashinsky; recherche d'états stables 2D et 3D dans le modèle Ohta-Kawasaki pour les copolymères di-blocs; et établir des orbites périodiques spontanées dans le flux de Navier-Stokes. Mais ce n'est qu'un début. Pour préparer l'avenir, deux problèmes non résolus se profilent à l'horizon:

  1. Connexion des orbites dans l'équation de Navier-Stokes pour les fluides. Récemment, des preuves numériques ont été trouvées pour des trajectoires dans les équations de Navier-Stokes (avec des conditions aux limites convenablement choisies) qui soient homocliniques aux orbites périodiques. Si nous pouvons valider rigoureusement l'existence de telles orbites, cela impliquerait, en forçant des résultats, la première preuve mathématiquement rigoureuse du flux chaotique dans les fluides (comme décrit par les équations de Navier-Stokes en 3D).
  2. Connecter des orbites dans des PDE mal posées. Les PDE mal posés (sans problème de valeur initiale approprié) accompagnant une structure variationnelle permettent la construction d'une homologie de Floer. Les orbites de connexion sont des ingrédients essentiels de cette construction. Si nous pouvons calculer rigoureusement de telles orbites de connexion, elles fournissent des informations «locales» spécifiques qui, combinées à des arguments analytiques globaux génériques, génèrent de puissants résultats de forçage. Les premiers pas vers cet objectif à long terme commencent à apparaître.

Ces deux problèmes soulignent que l'interaction, à travers des théorèmes de forçage, d'analyse globale et de calculs rigoureux locaux, peut conduire à des résultats très puissants dans des systèmes dynamiques à dimensions infinies. De plus, étant donné que la dynamique est extrêmement non linéaire, une approche assistée par ordinateur semble être le seul moyen de résoudre ce type de problèmes.

L'objectif de l'atelier est de favoriser la collaboration afin de développer une stratégie analytique flexible associée à des algorithmes rapides et robustes correspondants. La combinaison d'une analyse globale qualitative avec des informations quantitatives provenant de calculs rigoureusement vérifiés fournira de nouvelles informations sur la dynamique des systèmes à dimensions infinies qui modélisent la formation de modèles, les réseaux biologiques, les écoulements de fluides, etc.