Skip to Main content Skip to Navigation
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

https://hal.inria.fr/hal-01630411
Contributor : Florian Faissole <>
Submitted on : Tuesday, November 7, 2017 - 3:42:56 PM
Last modification on : Friday, April 30, 2021 - 9:55:34 AM
Long-term archiving on: : Thursday, February 8, 2018 - 1:18:08 PM

File

synasc_hal.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

369

Files downloads

577