Skip to content
Snippets Groups Projects
François Clément's avatar
François Clément authored
d2965642

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