affeldt-aist

naming and definition of `monotonous`

1

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?

1

##### Motivation for this change @t6s ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers ##### Automatic note...

convType instances

1

##### Motivation for this change address comment https://github.com/math-comp/analysis/pull/990/files/e686555022776816f6c70e98c00a1e6fd5923f95#diff-5edc277f753b88b71edd27b04c3075df73e37652e4c19c0f8dc6210fa57bf926 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers ##### Compatibility with...

better advertise the `coq-mathcomp-classical`

4

It was observed during the MathComp-Analysis dev meeting of 2023-12-21 that the existence of the `coq-mathcomp-classical` is not well-known @Tragicus We should maybe improve the MathComp website https://math-comp.github.io/installation.html so that...

notation for intervals

3

We have been using intervals with extended real numbers but this has the consequence that ``` `[0%E, +oo] = `[0%E, +oo[ ```. How can we handle that? @hoheinzollern @t6s

renaming of `conv`

3

https://github.com/math-comp/analysis/blob/0e392b5d36dd33e7e054a9a481bf9f4b17a90ed0/classical/set_interval.v#L340 1. rename to `line_path` or `affine_path` 2. add ```coq Definition wadd t a b : R := (1 - t) * a + t * b. ``` (this is...

https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L431 "The multiplication only works for realDomainType (and not for numDomainType), for relatively bad reasons."