Skip to content
Snippets Groups Projects
François Clément's avatar
François Clément authored
WIP: Open_equiv.
8de12aed
History
Name Last commit Last update
FEM
FiniteDim
LM
Lebesgue
.gitignore
COPYING
README.md

Numerical Analysis in Coq

Formal Developments and Proofs in Coq of Numerical Analysis Problems.

Authors: Aubry, Boldo, Clément, Faissole, Leclerc, Martin, Mayero, Mouhcine

This archive includes several Coq developments:

  • Lebesgue directory is about the Lebesgue Integration of Nonnegative Functions (see paper, report, and report);

  • Lebesgue/bochner_integral directory is about the Bochner integral (see report);

  • LM directory is about the Lax–Milgram theorem (see paper, and report);

  • FiniteDim directory is about finite dimensional subspaces (see paper).

Lebesgue is compiling in Coq 8.12 to 8.15. LM and FiniteDim are compiling in Coq 8.9.