Accéder directement au contenu Accéder directement à la navigation
Rapport

Lebesgue integration. Detailed proofs to be formalized in Coq

Résumé : Pour obtenir la plus grande confiance en la correction de programmes de simulation numérique implémentant la méthode des éléments finis, il faut formaliser les notions et résultats mathématiques qui permettent d'établir la justesse de la méthode. Les espaces de Sobolev sont le cadre mathématique dans lequel la plupart des formulations faibles pour résoudre les équations aux dérivées partielles sont posées, et où les solutions sont recherchées. La construction de ces espaces fonctionnels repose sur le calcul intégral et la théorie de la mesure. Ce chapitre de l'analyse fonctionnelle est donc un fondement théorique nécessaire à la définition de la méthode des éléments finis. L'objectif de ce document est de fournir à la communauté des chercheurs en preuve formelle des preuves papiers très détaillées des principaux résultats du calcul intégral et de la théorie de la mesure.
Liste complète des métadonnées

https://hal.inria.fr/hal-03105815
Contributeur : Francois Clement <>
Soumis le : jeudi 1 avril 2021 - 18:33:36
Dernière modification le : dimanche 4 avril 2021 - 03:07:25

Fichiers

RR-9386.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-03105815, version 2
  • ARXIV : 2101.05678

Citation

François Clément, Vincent Martin. Lebesgue integration. Detailed proofs to be formalized in Coq. [Research Report] RR-9386, Inria Paris. 2021, pp.284. ⟨hal-03105815v2⟩

Partager

Métriques

Consultations de la notice

55

Téléchargements de fichiers

223