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, paper, and report);
-
Lebesgue/bochner_integral directory is about the Bochner integral (see report);
-
LM directory is about the Lax–Milgram theorem (see paper, paper, and report);
Opam package coq-num-analysis: version 1.0 provides Lebesgue, and LM.
Lebesgue and LM are compiling in Coq 8.12 to 8.16.
Dependencies:
- coq-mathcomp-ssreflect (prior to version 2)
- coq-mathcomp-bigenough
- coq-mathcomp-finmap
- coq-mathcomp-fingroup
- coq-coquelicot
- coq-mathcomp-algebra
- coq-mathcomp-multinomials
- coq-mathcomp-classical
- coq-flocq