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.