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

Project 'mayero/coq-num-analysis' was moved to 'mayero/rocq-num-analysis'. Please update any links and bookmarks that may still have the old path.

Browse files

Feb 07, 2022
- Remove spurious whites. · ad20240b
  François Clément authored 3 years ago
  
  ad20240b
- Rm Lebesgue_scheme (replaced by induction on Mp/Mp2/Mp1 types). · b9a5aa64
  François Clément authored 3 years ago
  
  b9a5aa64
- 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 SFplus_seq. · 2e73eb5e
  François Clément authored 3 years ago
  
  2e73eb5e
- Move SFplus from Mp.v to simple_fun.v. · 272ef563
  François Clément authored 3 years ago
  
  272ef563
- Move adapted_seq from LInt_p.v to simple_fun.v to provide the dependency · 7e7f94ca
  François Clément authored 3 years ago
  7e7f94ca
- Spurious white. · 53bc75d3
  François Clément authored 3 years ago
  
  53bc75d3
Feb 04, 2022
- (sigma_algebra.v) Add measurable_seq. · 02b2b2ac
  François Clément authored 3 years ago
  02b2b2ac
Jan 29, 2022
- Renaming. · 0804fa1a
  François Clément authored 3 years ago
  0804fa1a
Jan 28, 2022
- More compact form. · 6558f483
  François Clément authored 3 years ago
  
  6558f483
Jan 26, 2022
- Some renaming: _measurable_fun -> _measurable. · d7c1f87e
  François Clément authored 3 years ago
  
  d7c1f87e
Jan 24, 2022
- Further simplification. · f4051cbe
  François Clément authored 3 years ago
  
  f4051cbe
- Proof of Lebesgue_scheme_step2_hyp_equiv. · 0d122ddc
  François Clément authored 3 years ago
  0d122ddc
- Add SF_measurable_fun_Rbar. · e4601c0c
  François Clément authored 3 years ago
  
  e4601c0c
- Oups. · 6def6c81
  François Clément authored 3 years ago
  
  6def6c81
- Quiet! · 885662c7
  François Clément authored 3 years ago
  
  885662c7
- Add doc + simplify poofs of finite_vals_canonic_cons and Lebesgue_scheme_step2. · c58a9721
  François Clément authored 3 years ago
  c58a9721
Jan 22, 2022
- Proof of Lebesgue_scheme_step2_hyp_equiv almost doe from that of Lebesgue_scheme_step2... · 9555ba30
  François Clément authored 3 years ago
  
  9555ba30
- Generalize SF_0 to any constant (SF_cst). · 3cd0db5f
  François Clément authored 3 years ago
  3cd0db5f
- Add SF_measurable_fun. · 5a2b62a6
  François Clément authored 3 years ago
  5a2b62a6
- Change name: *_step2 <-> *_step2_alt. · b30e378c
  François Clément authored 3 years ago
  
  b30e378c
- Proof of Lebesgue_scheme_step2. · d4a68453
  François Clément authored 3 years ago
  
  d4a68453
Jan 21, 2022
- Mv stuff about Lebesgue scheme step 2 from LInt_p.v to simple_fun.v. · 0c31fc9b
  François Clément authored 3 years ago
  
  0c31fc9b
Jan 20, 2022
- proof of Lebesgue_scheme_step2_alt · d2ae37d3
  Sylvie Boldo authored 3 years ago
  
  d2ae37d3
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
Jan 12, 2022
- WIP: proof of SF_aux_cons. · a35e6c80
  François Clément authored 3 years ago
  
  a35e6c80
- Augment statements of finite_vals_canonic_cons and SF_aux_cons. · cc28d393
  François Clément authored 3 years ago
  
  cc28d393
- Add finite_vals_canonic_cons and SF_aux_cons (still to be proved). · 89f6e54c
  François Clément authored 3 years ago
  
  89f6e54c
Oct 28, 2021
- 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 26, 2021
- sigma_algebra_R_Rbar.v -> sigma_algebra_R_Rbar-old.v · 4c03ae3e
  François Clément authored 3 years ago
  4c03ae3e
Sep 08, 2021
- Rm spurious white lines. · 4bb8c14b
  François Clément authored 3 years ago
  
  4bb8c14b
Sep 07, 2021
- initial sept. 2021 · fb0ef3a3
  Micaela Mayero authored 3 years ago
  
  fb0ef3a3
- initial from another archive · e51d4943
  Micaela Mayero authored 3 years ago
  
  View commits for tag LInt_p.1.0 LInt_p.1.0
  
  e51d4943