analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
This PR is an application of s-finite kernels to probabilistic programs. (NB: an early version of this PR appeared as PR #749 which is scheduled for closing) It provides a...
(I am just posting for the record an installation failure that I ran into last night but can't investigate right now, hoping somebody as a quick clue.) This opam command...
We've discussed at a handful of meetings that `topology.v` is too big at 8000 lines long. It causes at least 3 problems. 1. It makes it a pain to develop...
https://github.com/math-comp/analysis/blob/a5e2c659ea31a86b4789c9094f771d960187bf5c/theories/realfun.v#L14-L15 @CohenCyril I remember that you recently made a comment about this documentation being wrong but I cannot find your comment. What was it?
https://github.com/math-comp/analysis/blob/437d12c836f530fe5dfc8a26e7330b2653d175a3/classical/mathcomp_extra.v#L1491 "According to WP (https://en.wikipedia.org/wiki/Monotonic_function), this should rather be monotonic and I would expect it to be non strict (with homo instead of mono). Maybe we should also have a...
of `expRMm`? https://github.com/math-comp/analysis/blob/1d1d9bf2f8efb61ee33e73f3220d855ce7cce8e2/theories/exp.v#L410
https://github.com/math-comp/analysis/blob/7622cc7f7392b8866d7900ffb6ab6b1e48e81a7f/theories/measure.v#L2514 Shouldn't this be `Content_SigmaSubAdditive_isMeasure` to match the name of the predicate `sigma_sub_additive`? Also, we have `sigma_sub_additive` and `sigma_subadditive`. What about using `sigma_subset_subadditive` for `sigma_sub_additive`? (Or maybe the intent of...
https://github.com/math-comp/analysis/blob/c518e2a302126cbc96a7527e28cac28aaf443822/theories/lebesgue_integral.v#L3420 i.e., `f \_ D` instead of `f \* \1_ D` ?
qbs?
##### Motivation for this change @t6s ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers ##### Automatic note...
##### Motivation for this change tentative definition C1 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers ##### Compatibility with...
