analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change Finally, we prove that countable products of metrics are metrizable! In particularly, the cantor set is metrizable. I have - A definition for `countable_uniformity`. Several...
##### Motivation for this change Paths and loops are a critical feature of complex analysis. So we get started here with some basic definitions. Note this is still in draft...
https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/probability.v#L20 https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/probability.v#L70 The header documentation says `distribution` takes only one argument `X : {RV P >-> R}`, but its actual definition requires two arguments `P : probability T R` and...
##### Motivation for this change This is track D of issue #965 ~~This is based of PR #995~~ (merged) ~~Based on PR #1121~~ (merged) ##### Things done/to do - [x]...
##### Motivation for this change Three important changes here. 1. The `topology.v` file is huge, and kinda unpleasant for development. This splits all the function space topology stuff into a...
##### Motivation for this change I'm opening this draft PR to track the progress on this branch. The PR contributes a definition of Bernoulli trials and its central limit theorem....
##### Motivation for this change Part of the inference mechanism was missing and the canonical structures were not accessible. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` -...
##### Motivation for this change Introducing the Giry monad for probabilities, draft PR for now to track progress. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [...
https://github.com/math-comp/analysis/blob/7933dc1ebfcf48f44c18893e43762f120db10bef/theories/measure.v#L2702 indeed, we usually use `subdef`/`subproof` suffixes for internals