Description du livre
Récemment, divers problèmes mathématiques ont été résolus par des preuves assistées par ordinateur, parmi lesquels la conjecture de Kepler, l'existence du chaos, l'existence de l'attracteur de Lorenz, le célèbre problème des quatre couleurs, et plus. Dans de nombreux cas, les épreuves assistées par ordinateur ont l'avantage remarquable (par rapport à une épreuve "théorique") de fournir des informations quantitatives précises.
Les auteurs ont travaillé plus d'un quart de siècle pour établir les calculs vérifiés de solutions pour les équations aux dérivées partielles, principalement aux problèmes elliptiques non linéaires de la forme - ? u=f(x,u, ? u) avec conditions limites de Dirichlet. Par "calcul vérifié", on entend ici une approche numérique assistée par ordinateur pour prouver l'existence d'une solution dans un voisinage proche et explicite d'une solution approximative. Par conséquent, l'information quantitative obtenue à l'aide de la technique présentée ici devrait également être significative du point de vue des estimations des erreurs a posteriori pour la solution approximative des équations aux dérivées partielles concernées avec un sens mathématique rigoureux.
Dans cette monographie, les auteurs décrivent une enquête sur les calculs vérifiés ou les preuves assistées par ordinateur pour les équations aux dérivées partielles qu'ils ont élaborées. Dans la première partie, les méthodes principalement étudiées par les auteurs Nakao et Watanabe sont présentées. Ces méthodes sont fondées sur la projection dimensionnelle finie et les estimations constructives des erreurs a priori pour l'approximation par éléments finis de l'équation de Poisson. Dans la partie II, les approches assistées par ordinateur à l'aide de limites de valeurs propres mises au point par le deuxième auteur, Plum, sont expliquées en détail. La tâche principale de cette méthode consiste à définir des limites de valeurs propres pour les problèmes non linéaires correspondants des opérateurs linéarisés. De brèves remarques sont également formulées sur d'autres approches dans la Partie III. Chaque méthode des parties I et II est suivie d'exemples numériques appropriés qui confirment l'utilité réelle des méthodes des auteurs. Dans certains exemples également, les algorithmes informatiques pratiques sont fournis afin que les lecteurs puissent facilement mettre en œuvre le programme de vérification par eux-mêmes.