affeldt-aist
affeldt-aist
https://github.com/math-comp/analysis/blob/81969914159f7f0c957e627a54263eae72871744/theories/realfun.v#L611 "Most of the important lemmas like this one are probably true of limf_sup. At least lime_sup_ge0,, lime_supD, lime_inf_sup, and lim_lime_inf. There may be some conditions to replace with `\forall...
https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L650-L825 "The proof of the multiplication could probably be improved using wlog."
https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L845-L891 or at the very least provide a better (informative?) set of tests
https://github.com/math-comp/analysis/blob/7da865547861fd6937802e1f6e99f3c6d7f4b7b6/theories/lebesgue_integral.v#L2760-L2762 NB: has been renamed to `ge0_subset_integral` TODO: use a condition such as `forall x, B x -> ~ A x -> 0
##### Motivation for this change fixes #1092 `mulr_rev` had nothing to do in `derive.v` ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [] added corresponding documentation...
NB: this is an issue that makes more sense with the HB version of MathComp-Analysis Some contents of `cantor.v` can/should be moved to `topology.v` such as lemma `discrete_bool_compact` or `pointed_principal_filter`/`pointed_discrete_topology`....
This was a remark made by @zstone1 in the conversation about PR #973 . "Much of the results we've made will generalize to borel measures, (but without HB it's a...
##### Motivation for this change This was previously part of the PR #516 on probabilities. It might be better developed elsewhere. Subsumed by PR #1230 ##### Things done/to do -...
##### Motivation for this change Bernoulli probability measure as defined in ~~PR #749~~ draft PR #912 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added...
https://github.com/math-comp/analysis/blob/c8adb03b2de691e9ed7def8bbd1028720ef918e4/theories/lebesgue_integral.v#L41 what about using a notation such as ```coq Reserved Notation "x '=ae' y " (at level 60, format "x '=ae' y"). ``` or `=a.e.` ?