README.md

# 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](https://theses.hal.science/tel-04884651), and
[report](https://inria.hal.science/hal-04713897))

* *Lebesgue* directory is about the Lebesgue integration of nonnegative
measurable functions
(see [paper](https://hal.inria.fr/hal-03471095),
[paper](https://hal.inria.fr/hal-03889276), and
[report](https://hal.inria.fr/hal-03105815));

* *Lebesgue/bochner_integral* directory is about the Bochner integral
(see [report](https://hal.inria.fr/hal-03516749));

* *LM* directory is about the Lax–Milgram theorem
(see [paper](https://hal.inria.fr/hal-01391578),
[paper](https://hal.inria.fr/hal-01630411), and
[report](https://hal.inria.fr/hal-01344090));

Opam package [*coq-num-analysis*](https://coq.inria.fr/opam/www/):
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