Finite element method. Detailed proofs to be formalized in Coq - Laboratoire LMAC - Laboratoire de Mathématiques Appliquées de Compiègne
Rapport Année : 2024

Finite element method. Detailed proofs to be formalized in Coq

Méthode des éléments finis. Preuves détaillées en vue d'une formalisation en Coq

Résumé

To obtain the highest confidence on the correction of numerical simulation programs for the resolution of Partial Differential Equations (PDEs), one has to formalize the mathematical notions and results that allow to establish the soundness of the approach. The finite element method is one of the popular tools for the numerical resolution of a wide range of PDEs. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs for the construction of the Lagrange finite elements of any degree on simplices in positive dimension.
Pour obtenir la plus grande confiance dans l'exactitude des résultats de programmes de simulation numérique pour la résolution d'Équations aux Dérivées Partielles (EDPs), il faut formaliser les notions mathématiques sur lesquelles ils sont basés. La méthode des éléments finis est l'un des outils les plus utilisés pour la résolution de larges gammes d'EDPs. L'objectif de ce document est de fournir à la communauté des chercheurs en preuve formelle des preuves papiers très détaillées pour la construction des éléments finis de Lagrange de tout degré sur des simplexes en dimension quelconque.
Fichier principal
Vignette du fichier
RR-9557.pdf (1.93 Mo) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04713897 , version 1 (30-09-2024)

Licence

Identifiants

Citer

François Clément, Vincent Martin. Finite element method. Detailed proofs to be formalized in Coq. RR-9557, Inria Paris. 2024, pp.172. ⟨hal-04713897⟩
103 Consultations
40 Téléchargements

Altmetric

Partager

More