Skip to Main content Skip to Navigation
New interface
Conference papers

Formalization and closedness of finite dimensional subspaces

Florian Faissole 1 
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Florian Faissole Connect in order to contact the contributor
Submitted on : Tuesday, November 7, 2017 - 3:42:56 PM
Last modification on : Tuesday, October 25, 2022 - 4:16:50 PM
Long-term archiving on: : Thursday, February 8, 2018 - 1:18:08 PM


Files produced by the author(s)


  • HAL Id : hal-01630411, version 1


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⟩



Record views


Files downloads