analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
https://github.com/math-comp/analysis/blob/9ac498c5f38d1e4870ad4968bdd04d3e098de348/theories/sequences.v#L1635 to `nneseries_ge0`?
https://github.com/math-comp/analysis/blob/593c2448923f9b1577fbc97a871f75a8b43ac233/theories/measure.v#L866 shouldn't be this better named `discrete_measurable_nat` or `measurable_nat`?
https://github.com/math-comp/analysis/blob/fe3e6730467a67a155e1873800565bd87a5d17e7/theories/measure.v#L1971-L1976 Since this definition does not use `fset` anymore, it should maybe be renamed. Maybe `ring_finite_set`?
https://github.com/math-comp/analysis/blob/9ac498c5f38d1e4870ad4968bdd04d3e098de348/theories/constructive_ereal.v#L492-L496 rename to `fine_ge0` and `fine_gt0`?
##### Motivation for this change ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~- [ ] added corresponding documentation in the headers~ ##### Automatic note to reviewers...
##### Motivation for this change Splitting out another piece of the Banach Fixed Point PR, this just defines contractions and proves a simple fact about them. Note that this places...
##### Files available for porting ([x] means taken by someone) - [ ] topology.v (look for TODO_HB) - [ ] normedtype.v (look for TODO_HB) ##### Motivation for this change @affeldt-aist...
Manual note: I noted the 0.5.3 release, but couldn't run CI again. I expect you want 0.5.3. **Please leave this issue open until I updated to 0.5.3!** The Coq team...
https://github.com/math-comp/analysis/blob/82e29a05dfc54f40bf576961bec7fdd6bdfb5c34/theories/measure.v#L2278-L2282 maybe it'd better be `cvg_measure_inc` to avoid using the name of the variable `mu`
##### Motivation for this change fixes #664 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ ##### Automatic note...