Commits · 905473288e381d61201bf52d7a089a57472f0a5a · Micaela Mayero / Numerical Analysis in Coq

Mar 23, 2022
- Inductive type (instead of def with exists) is more convenient. · 90547328
  François Clément authored 2 years ago
  
  But need to keep both for one proof.
  90547328
- WIP: new implementation. · 4d0d28d9
  François Clément authored 2 years ago
  
  4d0d28d9
- WIP: playing with image (exists -> Inductive). · b5b0bed3
  François Clément authored 2 years ago
  
  b5b0bed3
- Add equivalence binary relation same_fun. · 83ad0021
  François Clément authored 2 years ago
  
  Add extensionality results on (pre)image.
  83ad0021
- Try this one? · 71e54c62
  François Clément authored 2 years ago
  
  71e54c62
- Add some results + cleaning. · d25a85b7
  François Clément authored 2 years ago
  
  WIP: being lazy with proofs of measurable_Rbar_abs and measurable_Rbar_scal.
  d25a85b7
- Proofs of measurable_Rbar_{(g|l)(e|t),(c|o)(c|o)}. · e9c98dbd
  François Clément authored 2 years ago
  
  e9c98dbd
- Proofs of measurable_Rbar_topo_basis_gt and measurable_Rbar_topo_basis_lt. · 602c59aa
  François Clément authored 2 years ago
  
  602c59aa
Mar 22, 2022
- Rm useless try's. · 150d5ecd
  François Clément authored 2 years ago
  
  150d5ecd
- WIP: other generators of measurable_Rbar_Borel. · 41809e6c
  François Clément authored 2 years ago
  
  41809e6c
- Add approximations based on the Archimedean property. · e0f8f77a
  François Clément authored 2 years ago
  
  e0f8f77a
- Useless. · 3a78a310
  François Clément authored 2 years ago
  
  3a78a310
- Renaming (unique prefix = measurable_Rbar_). · 9cd62ee8
  François Clément authored 2 years ago
  
  9cd62ee8
- Renaming: unify _distr. · c086ef47
  François Clément authored 2 years ago
  
  c086ef47
- Renaming: unify _distr. · 47e69b85
  François Clément authored 2 years ago
  
  Add missing proofs/results.
  47e69b85
- Renaming: unify _distr. · 76c643f9
  François Clément authored 2 years ago
  
  76c643f9
- WIP: measurable subspace. · 24c0d69d
  François Clément authored 2 years ago
  
  24c0d69d
- Renaming: unification (_monot, _compat, _l, _r) · 38c247a6
  François Clément authored 2 years ago
  
  38c247a6
- Add and move references to RR-9386. · 26dbcad3
  François Clément authored 2 years ago
  
  26dbcad3
Mar 21, 2022
- WIP: playing with streams... · 0be32827
  François Clément authored 2 years ago
  
  0be32827
- More compact. · 60a7a33e
  François Clément authored 2 years ago
  
  60a7a33e
Mar 18, 2022
- WIP: select True values in nat predicate. · 0f829fa7
  François Clément authored 3 years ago
  
  0f829fa7
- Monotony is actually useless! · 126e62bb
  François Clément authored 3 years ago
  
  126e62bb
- Equip FEM folder for compilation. · 239c046a
  François Clément authored 3 years ago
  
  239c046a
- R_AbsRing -> R_Ring. · 60630864
  François Clément authored 3 years ago
  
  60630864
- Renaming sections. · 5dd24100
  François Clément authored 3 years ago
  
  5dd24100
- Finite dimension · 10db5fe4
  Sylvie Boldo authored 3 years ago
  
  10db5fe4
Mar 17, 2022
- Evening train... · 15465098
  François Clément authored 3 years ago
  
  15465098
- WIP: proof of measurable_gen_Preimage. · b752b3fa
  François Clément authored 3 years ago
  
  b752b3fa
- Unify with Lebesgue folder: CoqMakefile -> Makefile. · e9998154
  François Clément authored 3 years ago
  
  e9998154
- Proofs of image_diff, image_compl and preimage_empty_equiv. · b0a05d81
  François Clément authored 3 years ago
  
  b0a05d81
- Proofs of image_{union,inter}*. · cd311819
  François Clément authored 3 years ago
  
  cd311819
Mar 16, 2022
- Add Image/Preimage. · 6b466dc7
  François Clément authored 3 years ago
  
  WIP: add facts about Image/Preimage.
  6b466dc7
- Add measurable_Rbar_gen_lub_up_{m,p}. · 42f1fbda
  François Clément authored 3 years ago
  
  42f1fbda
- Equiv -> impl. · dc3b0de3
  François Clément authored 3 years ago
  
  dc3b0de3
- Add image/preimage. · 71731d6c
  François Clément authored 3 years ago
  
  WIP: many facts about image/preimage.
  71731d6c
Mar 11, 2022
- WIP: proofs of measurable_Borel_Rbar_eq_(l|g)(t|e). · 4abd489e
  François Clément authored 3 years ago
  
  Proofs of measurable_Rbar_*.
  4abd489e
- Order (imports) + renaming (section). · 730777b8
  François Clément authored 3 years ago
  
  730777b8
- Add Rbar_oo_diag_is_empty. · cefb2c05
  François Clément authored 3 years ago
  
  Remove useless.
  cefb2c05
Mar 10, 2022
- Proof of measurable_Rbar_R_correct and measurable_R_Rbar_correct. · 11d85fc4
  François Clément authored 3 years ago
  
  11d85fc4