Colloquium (archives)

Les logiciels de vérification de démonstrations existent depuis la fin des années 60 et ont fait de grands progrès ces dernières années. On pourrait imaginer que les mathématiciens les utilisent, que ce soit à petite échelle ou pour vérifier des théories très techniques, ou encore pour enseigner la notion de démonstration. Cependant presque aucun mathématicien ne le fait. On sait depuis la vérification en 2012 du théorème de Feit-Thompson que, entre les mains d'informathématiciens experts, ces logiciels peuvent vérifier une démonstration longue et compliquée mais ne faisant intervenir que des objets simples à définir. Dans cet exposé, je rendrai compte d'expériences en cours où des mathématiciens, sans formation en informatique théorique, essayent de manipuler des objets mathématiques sophistiqués dans le logiciel de vérification Lean.

Dans cet exposé, je m'intéresse à l'approximation numérique des problèmes hyperboliques non linéaires. Il est bien connu que la solution générique du problème de Cauchy pour un problème de ce type n'est même pas continue, en général, d'où la notion de solution faible. Il faut aussi rajouter un principe de sélection au moyen d'entropies, et donc des inégalités supplémentaires. Du point de vue numérique, la notion de solution faible se traduit, grâce au théorème de Lax Wendroff (1960), par la notion de flux qui donne aussi la forme que doit posséder un schéma numérique pour fournir des solutions convergeant vers une solution faible. Les contraintes d'entropies se traduisent simplement par des contraintes sur des flux liés à l'entropie. Depuis longtemps, la recherche se résume à construire des schémas, donc des flux, de plus en plus robustes, précis, .... Je revisiterai la notion de conservation, pour introduire une variante un peu plus générale qui permettra de démontrer un théorème à la Lax Wendroff, et de montrer que tous les schémas classiques, éléments finis compris, ont une forme par flux, avec une expression analytique des flux. Je montrerai aussi qu'elle permet de construire, à partir d'un schéma quelconque, un schéma, toujours localement conservatif, mais qui satisfait d'autres relations (ou inégalités) de conservation, l'exemple typique étant celui de l'entropie.

Depuis une douzaine d'années, les modèles utilisant des patchs (ou imagettes) pour traiter les images ont conduit à des améliorations très significatives aussi bien dans la résolution de problèmes inverses de restauration (débruitage, inpainting, interpolation d'images) que dans des problèmes de synthèse ou d'édition d'images. Ils soulèvent des questions passionnantes touchant de nombreuses facettes des mathématiques appliquées (statistique, optimisation, géométrie), et nécessitent des méthodes numériques efficaces pour les résoudre. Une des questions se posant par exemple dans ce contexte est celle des modèles statistiques et géométriques adéquats pour représenter les espaces de patchs. En restauration d'images, de tels modèles peuvent par exemple servir d'a priori afin d'estimer un patch à partir de sa version dégradée. Cependant, l'inférence de ces modèles est complexe (espace de grande dimension), et d'autant plus délicate que les données sont dégradées. Je présenterai dans cet exposé quelques contributions à ce domaine.

Considérons une suite $un$ qui est définie par une relation de récurrence linéaire. Le théorème de Skolem, Mahler et Lech stipule que les indices $n$ en lesquels $un$ s’annule forment une union finie de progressions arithmétiques. J’expliquerai comment l’approximation des fonctions continues par des polynômes et les bases de l’analyse $p$-adique permettent d’obtenir un tel énoncé. La méthode employée couvre maintenant des situations non linéaires et a de multiples conséquences; j’en décrirai quelques unes.

Les équations de Navier-Stokes constituent un modèle mathématique de base pour décrire le mouvement d'un fluide. Dans son célèbre article « Sur le mouvement d'un liquide visqueux emplissant l'espace » publié dans Acta Mathematica en 1934, Jean Leray (1906-1998) introduit (entre autres) le concept de solutions faibles globales en temps en donnant une définition précise de ce qu'est une solution irrégulière du système, et montre qu'il existe une telle solution faible pour les équations de Navier-Stokes dans leur version incompressible et homogène (densité constante). On appelle maintenant « solutions à la Leray » ces solutions d'énergie finie. En 2007, J.-Y. Chemin donne un très bel exposé intitulé "Jean Leray et les fondements mathématiques de la turbulence" à la Bibliothèque Nationale de France:

                     http://smf.emath.fr/content/chemin-jean-yves-jean-leray-et-les-fondements-mathématiques-de-la-turbulence

qui fait suite à un très bel article qu'il a publié en 2004 pour les 70 ans de l'article fondateur de J. Leray paru dans Acta Mathematica: l'auditoire du colloquium est convié à consulter ces deux références.

Même si l'existence globale de solutions faibles apporte assez peu sur le caractère bien posé du système, une telle analyse a de nombreux intérêts pratiques. En plus de la signification physique (fondements de la turbulence), car la régularité supposée sur les données initiales est minimale et fortement liée à des quantités physiques bien identifiées, les propriétés de stabilité des solutions faibles du modèle continu aident à mieux comprendre comment construire des schémas numériques stables qui le plus souvent ne préservent pas les estimations de régularité forte.

Dans cette balade autour des équations de Navier-Stokes, j'essaierai de dresser un état de l'art sur les « solutions à la Leray ». Nous verrons notamment que nous sommes bien loin d'une théorie générale sur les versions compressibles et que de nombreux problèmes ouverts importants perdurent toujours même si des résultats fondateurs ont été obtenus ces 20 dernières années.

Les systèmes toriques (ou variétés toriques) sont bien connus en géométries algébrique et symplectique, en particulier depuis les travaux d'Atiyah, Guillemin-Sternberg et Delzant dans les années 1980. Ils correspondent à des systèmes hamiltoniens intégrables dont tous les flots sont périodiques. Mais ce sont des objets trop rigides pour la mécanique (classique ou quantique). Il y a une dizaine d'années, une timide généralisation a vu le jour: les systèmes semi-toriques, qui s'est finalement révélée très riche et a donné lieu à de nombreuses applications, de la topologie à l'analyse microlocale et la théorie spectrale. J'essaierai de faire le point, et d'évoquer les pistes de développements futurs.

En s'inspirant de travaux de Benjamini et Schramm sur les empilements de sphères, on introduit une notion d'application conforme à grande échelle entre espaces métriques. Elle contient toutes les classes précédemment étudiées. Néanmoins, on démontre une obstruction à l'existence de telles applications, entre groupes hyperboliques notamment.

En 1959, R.V. Kadison et I.M. Singer demandaient si tout état pur sur l'algèbre des opérateurs diagonaux bornés sur $\ell^2$, admet une extension unique en un état pur de $B(\ell^2)$. La réponse positive a été donnée en juin 2013 par A. Marcus, D. Spielman et N. Srivastava, après une série de traductions du problème original, par C. Akemann, J. Anderson, N. Weaver... Au final, le problème se ramène à une estimation du plus grand zéro de l'espérance du polynôme caractéristique d'une somme de variables aléatoires indépendantes à valeurs dans les matrices semi-définies positives de rang 1 dans l'algèbre des matrices n-fois-n.

Résumé : Certaines questions d'analyse harmonique motivent également les\break edp-istes: les uns travaillent dans R^n, les autres prennent le risque de la non-commutativité en se plongeant dans des groupes exotiques dont la "star" est sans conteste le groupe d'Heisenberg. Notre objectif dans cet interlude * microlocal sera de s'appuyer sur un de ces sujets communs pour se familiariser avec l'approche microlocale et comprendre comment celle-ci peut être mise en oeuvre dans des contextes variés.

*Un interlude est une petite pièce instrumentale jouée entre deux morceaux plus considérables.