Skip to content
Snippets Groups Projects
Select Git revision
  • no_ms
  • master default protected
  • test_skolem_ko
  • Subset
  • essais-8.18
  • pr_no_math-comp
  • released
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
12 results
Compare
François Clément's avatar
Add map2F_correct,
François Clément authored 
    f_{plus,zero}_compat_mapF, morphism_m_{mapF,map2F},
    f_{opp,minus}_compat_mapF, morphism_g_{mapF,map2F},
    f_{mult,one}_compat_mapF, morphism_r_{mapF,map2F},
    lm_sum, lm_fct_plus,
    f_scal_compat_mapF, lm_{mapF,map2F}.
Rename lm_f_scal_l -> fct_scal_l_lm,
       lc_lm_compat_l -> fct_lc_l_lm,
       lm_f_scal_r -> fct_scal_r_lm,
       lc_lm_compat_r* -> fct_lc_r_lm*,
       lc_fun_lc -> f_lc_compat_lms.
WIP: lm_fct_{zero,sum,opp,minus,scal}, fct_scalF_l_lm.
fdc5fdb6
History
François Clément's avatar fdc5fdb6
History
Name Last commit Last update
FEM
LM
Lebesgue
.gitignore
.gitlab-ci.yml
COPYING
Makefile
README.md
_CoqProject
flake.lock
flake.nix
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.

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