analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change the easy bit of issue #1135 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference:...
Co-authored-by: @JeremyDubut Co-authored-by: @AkihisaYamada ##### Motivation for this change ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ Reference: [How to...
##### Motivation for this change TODO: maybe also rename `xsection` to `xsect`, that's clear enough. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding...
https://github.com/math-comp/analysis/blob/53a6bff77bd285d33cb91094cfbee9e092837f34/theories/topology.v#L4000 the `to_set` notation is declared here and also in other files but is redundant with the `xsection` definition (modulo the Prop/bool difference)
##### Motivation for this change See issue #965 Provides also the Borel-Cantelli lemma (and the limit superior of the sequence of sets) and continuity of the indefinite integral at the...
##### Motivation for this change This is a first step towards fixing the issue https://github.com/math-comp/analysis/issues/1225 : rename `setD_closed` to `setSD_closed` so that `setDI_closed` can be renamed `setD_closed` later. ##### Checklist...
##### Motivation for this change Draft PR containing the Bernoulli sampling theorem ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the...
##### Motivation for this change Adding topological vector spaces as a new structure. Further PRs will integrate the theory of topological vector spaces (duality, function spaces, characterization of topologies, distribution...
##### Motivation for this change New packages: * coq-mathcomp-reals * all_realsl.v * constructive_ereal.v * itv.v * nsatz_realtype.v * prodnormedzmodule.v * real_interval.v * reals.v * signed.v * coq-mathcomp-altreals * altreals/dedekind.v *...
##### Motivation for this change A few lemmas about `Rintegral`, `atan`, and `expR` that have found their use in an on-going development about the Gauss integral. ##### Checklist - [x]...