A Coq formal proof of the Lax–Milgram theorem
| Autor: | Florian Faissole, Vincent Martin, François Clément, Sylvie Boldo, Micaela Mayero |
|---|---|
| Přispěvatelé: | Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA), Inria de Paris, Laboratoire de Mathématiques Appliquées de Compiègne (LMAC), Université de Technologie de Compiègne (UTC), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Labex Digicosme, Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Babuška–Lax–Milgram theorem
Computer science finite element method Lax-Milgram theorem 0102 computer and information sciences 02 engineering and technology [MATH.MATH-FA]Mathematics [math]/Functional Analysis [math.FA] 01 natural sciences Formal proof functional analysis symbols.namesake Lions–Lax–Milgram theorem 020204 information systems Completeness (order theory) formal proof 0202 electrical engineering electronic engineering information engineering Calculus Coq Uniqueness Soundness Hilbert space [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 010201 computation theory & mathematics Linear algebra symbols [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA] |
| Zdroj: | 6th ACM SIGPLAN Conference on Certified Programs and Proofs 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩ CPP |
| DOI: | 10.1145/3018610.3018625⟩ |
| Popis: | International audience; The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. To obtain the highest confidence on the correction of numerical simulation programs implementing the Finite Element Method, one has to formalize the mathematical notions and results that allow to establish the sound-ness of the method. The Lax–Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. This article presents the full formal proof of the Lax–Milgram theorem in Coq. It requires many results from linear algebra, geometry, functional analysis , and Hilbert spaces. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|