Commits · Tonelli.1.0 · Micaela Mayero / Numerical Analysis in Rocq · GitLab

Snippets Groups Projects

Feb 07, 2022
- Remove spurious whites. · ad20240b
  François Clément authored 3 years ago
  
  ad20240b
- Remove already commented useless stuff. · 1def54d6
  François Clément authored 3 years ago
  
  1def54d6
- rm les 8.15 · 86824f9a
  Micaela Mayero authored 3 years ago
  
  86824f9a
- passage 8.15 · 808d0bad
  Micaela Mayero authored 3 years ago
  
  808d0bad
Feb 06, 2022
- Add measurable_fun_Rbar_R', Mplus_plus_R, Mplus_mult_R. · 0a866848
  François Clément authored 3 years ago
  
  0a866848
Feb 04, 2022
- (sigma_algebra.v) Add measurable_seq. · 02b2b2ac
  François Clément authored 3 years ago
  02b2b2ac
Jan 28, 2022
- Def swap_var and use genUxV local defs. · 9885b861
  François Clément authored 3 years ago
  
  9885b861
Jan 24, 2022
- Add measurable_fun_swap_R. · 3aaeec9c
  François Clément authored 3 years ago
  
  3aaeec9c
Jan 22, 2022
- Add results on scal-charac. · 30096c86
  François Clément authored 3 years ago
  
  30096c86
Jan 19, 2022
- Replace use of subset_compl for charac by Subset_charac. · 1ef4ebf3
  François Clément authored 3 years ago
  
  1ef4ebf3
Jan 18, 2022
- Naming: *non_neg* -> *nonneg*. · b462d2ba
  François Clément authored 3 years ago
  
  b462d2ba
- Unify naming: remove most prime from statement names (-> _alt, _rev, _aux). · 53cf56d8
  François Clément authored 3 years ago
  53cf56d8
Dec 10, 2021
- Renamings again + moving lemmas · e38fc42a
  Sylvie Boldo authored 3 years ago
  
  e38fc42a
Dec 08, 2021
- Move Tonelli.measurable_swap to sigma_algebra. · 4ca8e5ef
  François Clément authored 3 years ago
  4ca8e5ef
Nov 23, 2021
- Spurious white. · 84e0b92e
  François Clément authored 3 years ago
  
  84e0b92e
- Proof of measurable_fun_ext{1,2}. · 327f232b
  François Clément authored 3 years ago
  
  327f232b
Nov 05, 2021
- delete non_neg_plus lemma. It already exists in sum_Rbar_nonneg.v file. · 844f7ae5
  Mouhcine authored 3 years ago
  
  844f7ae5
Oct 28, 2021
- Try to solve the problematic merge of 2021/10/27 by reverting to commit · 85c24dca
  François Clément authored 3 years ago
  85c24dca
- Revert "Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis" · bf09a470
  François Clément authored 3 years ago
  bf09a470
Oct 27, 2021
- Problem with git push · a55c3560
  Mouhcine authored 3 years ago
  
  a55c3560
- Add and prove measurable_fun_plus_count_non_neg' lemma. · e105f260
  Mouhcine authored 3 years ago
  
  e105f260
- Add new lemma. · ed83aaa3
  Mouhcine authored 3 years ago
  
  ed83aaa3
- Add and prove measurable_fun_plus_count_non_neg' lemma. · 7e4c71c3
  Mouhcine authored 3 years ago
  
  7e4c71c3
- Add measurable_fun_plus_count_non_neg' lemma. · 8da2b532
  Mouhcine authored 3 years ago
  
  8da2b532
Oct 26, 2021
- finish the proof of measurability of finite and countable sums of measurable functions · e3b171a3
  Mouhcine authored 3 years ago
  
  e3b171a3
- sigma_algebra_R_Rbar.v -> sigma_algebra_R_Rbar-old.v · 4c03ae3e
  François Clément authored 3 years ago
  4c03ae3e
Oct 22, 2021
- Add measurability of finite and countable sums of measurable functions. · 9ea727d4
  François Clément authored 4 years ago
  
  9ea727d4
Oct 04, 2021
- Réunion 4/10 · be3e81e7
  Sylvie Boldo authored 4 years ago
  
  be3e81e7
Sep 07, 2021
- initial sept. 2021 · fb0ef3a3
  Micaela Mayero authored 4 years ago
  
  fb0ef3a3
- initial from another archive · e51d4943
  Micaela Mayero authored 4 years ago
  
  View commits for tag LInt_p.1.0 LInt_p.1.0
  
  e51d4943