Introduction aux preuves assistées par ordinateur en analyse non-linéaire (Damien Galant, Université de Mons & UPHF)

Résumé :

Comment les ordinateurs calculent-ils ?

Nous nous intéresserons dans un premier temps à cette question et découvrirons les nombres à virgule flottante, la façon la plus courante de réaliser informatiquement des calculs impliquant des grandeurs continues. Nous verrons que ces calculs présentent nécessairement des erreurs numériques, ce que nous illustrerons par plusieurs exemples, parfois spectaculaires. Se pose alors une seconde question :

Comment obtenir des résultats mathématiques rigoureux basés sur des calculs numériques par ordinateur ?

Nous introduirons l'arithmétique d'intervalles, basés sur l'idée simple de remplacer les nombres réels par des couples de nombres correspondant à un minorant et à un majorant de la quantité d'intérêt. Nous mentionnerons quelques exemples célèbres de problèmes dont la solution a utilisé l'arithmétique d'intervalles.

Finalement, nous présenterons brièvement l'application de telles méthodes à l'analyse de symétries de solutions pour une équation de Schrödinger non-linéaire posée sur le "graphe tétraèdre", dans un régime "presque linéaire". Nous verrons que l'ordinateur sera très utile dans l'analyse du problème. Cette dernière partie est issue d'une collaboration avec mes directeurs de thèse, le Pr. Colette De Coster (CERAMATHS/DMATHS, Valenciennes) et le Pr. Christophe Troestler (UMONS, Mons, Belgique).