Numerical Analysis in Coq

Formal developments and proofs in Coq of numerical analysis results.

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

This archive includes several Coq developments:

• FEM directory is about the Finite Element Method, including simplicial Lagrange finite elements (see PhD thesis, and report)

• Lebesgue directory is about the Lebesgue integration of nonnegative measurable 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.

Everything is compiling in Coq 8.20.

Dependencies:

• coq-coquelicot (>= 3.4.0)
• coq-flocq
• coq-mathcomp-algebra (>= 2.0.0)
• coq-mathcomp-classical