The Lax-Milgram Theorem. A detailed proof 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. Le théorème de Lax-Milgram peut être vu comme l'un de ces fondements théoriques : sous des hypothèses de complétude et de coercivité, il énonce l'existence et l'unicité de la solution de certains problèmes aux limites posés sous forme faible. L'objectif de ce document est de fournir à la communauté preuve formelle une preuve papier très détaillée du théorème de Lax-Milgram.
Type de document :
Rapport
[Research Report] RR-8934, Inria Paris. 2016
Liste complète des métadonnées

https://hal.inria.fr/hal-01344090
Contributeur : Francois Clement <>
Soumis le : lundi 3 octobre 2016 - 13:04:19
Dernière modification le : mercredi 5 octobre 2016 - 01:08:32

Fichiers

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

Identifiants

  • HAL Id : hal-01344090, version 2
  • ARXIV : 1607.03618

Collections

Citation

François Clément, Vincent Martin. The Lax-Milgram Theorem. A detailed proof to be formalized in Coq. [Research Report] RR-8934, Inria Paris. 2016. <hal-01344090v2>

Partager

Métriques

Consultations de
la notice

144

Téléchargements du document

101