Skip to content
Snippets Groups Projects
user avatar
Mouhcine authored
Prove is_linear_mapping_f_scal_l
	& comb_lin_linear_mapping_compat_l lemmas.
c1658422
Name Last commit Last update
FEM
FiniteDim
LM
Lebesgue
.gitignore
COPYING
README.md
opam

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.