analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
a doc on - upgrading the local nix shell (shell.nix) on analysis? - or upgrading the package definitions (mathcomp/extra.nix) on nixpkgs? _Originally posted by @CohenCyril in https://github.com/math-comp/analysis/pull/147#issuecomment-508095855_
Provide and document derivation notations such as: - ``f^`(n)``, ``f^`()`` and ``f^`N(n)`` (as in `poly.v`) for derivation on`R` (and when available, on `C`) - `'D(A -> V)` for the type...
Indeed, otherwise locally' is not proper. Other issues? One way or another?
And define weak and sup filteredType, compare with weak and sup topology. And define the prod as the sup of the two comaps of π₁ and π₂. Credit @johoelzl for...
Try to substitute canonical structures for typeclasses everywhere, so that we only use CS instead of TC... (And maybe put in filteredType the axiom that canonical sets of sets must...
##### Motivation for this change Introduces probabilistic convergence ##### Things done/to do - [ ] add weak law of large numbers - [ ] prove Markov's and Chebyshev's inequality -...
##### Motivation for this change Versions of already existing lemmas to deal with sequences of non-positive numbers, motivated by their application when dealing with signed measures. ##### Things done/to do...
##### Motivation for this change this is trivial but I kept on proving it ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding...
##### Motivation for this change needed to develop measure theory ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers...