Preuves formelles en mathématiques appliquées : formalisation en Coq des éléments finis de Lagrange simpliciaux

Formal Proofs in Applied Mathematics : A Coq Formalization of Simplicial Lagrange Finite Elements Cette thèse est dédiée au développement de preuves formelles de théorèmes et propositions mathématiques dans le domaine de l'analyse réelle, en utilisant l'assistant de preuve Coq pour garantir leur exactitude. Le cœur de ce travail est divisé en deux parties principales.La première partie se concentre sur l'utilisation de Coq pour formaliser des principes mathématiques clés tels que le principe d'induction de Lebesgue et le théorème de Tonelli, permettant le calcul d'intégrales doubles sur des espaces produits en intégrant de manière itérative par rapport à chaque variable. Ce travail s'appuie sur des recherches antérieures en théorie de la mesure et sur l'intégrale de Lebesgue.La deuxième partie de cette thèse fonctionne dans le cadre de la méthode des éléments finis (MEF), une technique numérique largement utilisée pour résoudre des équations aux dérivées partielles (EDP). La MEF joue un rôle important dans de nombreux programmes de simulation industrielle, notamment dans l'approximation des solutions à des problèmes complexes tels que le transfert de chaleur, la dynamique des fluides et les simulations de champs électromagnétiques. Plus spécifiquement, nous visons à construire des éléments finis, en nous concentrant sur les éléments finis de Lagrange simpliciaux avec des degrés de liberté répartis uniformément. Ce travail mobilise un large éventail de concepts algébriques, y compris les familles finies, les monoïdes, les espaces vectoriels, les espaces affines, les sous-structures et les espaces de dimensions finies.Pour mener à bien cette étude, nous formalisons dans Coq en logique classique plusieurs composants fondamentaux. Nous commençons par construire un élément fini général, puis nous procédons à la définition de plusieurs composants fondamentaux, y compris la construction de l'espace d'approximation de Lagrange, l'expression de sa base de polynômes de Lagrange et la formalisation des transformations géométriques affines et de la propriété d'unisolvance des éléments finis de Lagrange.