analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
The discussion in #1600 shows that the `{ae mu, P}` notation is used in places where `\forall x \ae mu, Q x` should be preferred (where `P = forall x,...
##### Motivation for this change @zstone1 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Merge policy...
https://github.com/math-comp/analysis/blob/d9ba8ca333776a539bfbe59270cc86a6533d6bad/theories/realfun.v#L2019-L2021 and write the equality the other way around?
##### Motivation for this change Initial PR for an implementation of the Giry monad after discussion with @affeldt-aist and @hoheinzollern (See also PR #1177) Co-authored with @markusdemedeiros. This is WIP...
Should `weak_topology` as described in [weak_topology.v](https://github.com/math-comp/analysis/blob/master/theories/topology_theory/weak_topology.v) be renamed to `initial_topology` ? In my opinion, "weak topology" is more often used to refer to the weak topology induced on a `E...
What they propose and what should be loaded to be what
The files in `lebesgue_integral_theory` should be organized in such a way that the following high-level topics can be easily identified: - Algebra of integrands: Linearity, order, that kind of thing...
That's the second time that I use `etc/packager` and this is a great help. Thank you @proux01 . However, it does not seem to generate the right checksum for me...
For the record, comment from PR #1396 by @zstone1 : "It would be nice to have this for any metric space (or indeed any first-countable space). But it's fine to...
https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L2747 https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L3105-L3106 I found a confusion of abbreviation `l` and `r`. I think that `cvgeMl` should be `cvgMr`, but I am not sure. NB(2025/04/21): the renaming of `cvgMr` is still...
