Formalization and closedness of finite dimensional subspaces

Florian Faissole 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : This article presents a Coq formalization of finite dimensional subspaces of Hilbert spaces: we prove that such subspaces are closed submodules. This result is one of the basic blocks to prove the correctness of the finite element method which approaches the solution of partial differential equations. The exact solution is valued in a continuous volume (Hilbert space) while the approximation is valued in a mesh (finite dimensional subspace) which fits the shape of the volume. When applied to a submodule which is finite dimensional, Lax– Milgram Theorem and Céa Lemma ensure the finite element method is sufficiently precise. We rely on filters as basis for topological reasoning: filters provide a very general framework to express local properties and limits. However, most such mathematical literature does not rely on filters, making our Coq formalization unusual.
Type de document :
Communication dans un congrès
SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01630411
Contributeur : Florian Faissole <>
Soumis le : mardi 7 novembre 2017 - 15:42:56
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : jeudi 8 février 2018 - 13:18:08

Fichier

synasc_hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01630411, version 1

Citation

Florian Faissole. Formalization and closedness of finite dimensional subspaces. SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7. 〈hal-01630411〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

35