Skip to content
Snippets Groups Projects
Select Git revision
  • 3d771c3a7851190cc3ebda3828c47df90ecca3ac
  • master default protected
  • Subset
  • 2.1
  • FE_new_def
  • 2.0 protected
  • 1.0 protected
  • 2.0.0 protected
  • PhD_HM_2024
  • 1.0 protected
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
13 results

rocq-num-analysis

François Clément's avatar
hilbert, continuous_linear_map, hierarchyD, lax_milgram, lax_milgram_cea, finitedim:
François Clément authored 
Add AbelianMonoid stage in the hierarchy.
Use rewrite/apply from SSReflect when necessary.

check_sub_structure:
Obsolete, use FEM/Linalg/Sub_struct.
3d771c3a
History
François Clément's avatar 3d771c3a
History
Name Last commit Last update
FEM
FiniteDim
LM
Lebesgue
.gitignore
COPYING
README.md
opam
README.md

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.