analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
https://github.com/math-comp/analysis/blob/1f462809ae6cfdddeea2c6a64ae36d1398063944/theories/realfun.v#L1927 `itv_partition` is now defined over `R : realType` as `seq R` with two conditions. However, the definition of `itv_partition` uses only the equality and an order structure of `R`....
##### Motivation for this change When deriving differential equations using lsubmx/rsubmx, we need proofs of their differentiability. This PR also contains a lemma making use of the "is_derive1_sqrt" lemma to...
https://github.com/math-comp/analysis/blob/5e727ceca161fd469db6fa76daa5ce4cf9f28ccd/theories/topology_theory/order_topology.v#L25 when dropping support for MathComp < 2.5
in `contra.v`: https://github.com/math-comp/analysis/blob/61acc8dd2fa007265e5aabcd76cf47f6ee7a812c/classical/contra.v#L272 and in `boolp.v`: https://github.com/math-comp/analysis/blob/61acc8dd2fa007265e5aabcd76cf47f6ee7a812c/classical/boolp.v#L686 causing different behaviors according to which module is require imported.
https://github.com/math-comp/analysis/blob/0e4fbab71717e572542e3c8069018412a954c025/classical/cardinality.v#L448
https://github.com/math-comp/analysis/blob/0e4fbab71717e572542e3c8069018412a954c025/theories/realfun.v#L2172 might be better to have `c` as a non-implict argument put first
##### Motivation for this change ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Merge...
##### Motivation for this change This PR adds notions of differential calculus that we want for differential geometry. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [...
##### Motivation for this change This PR contains the formalization of the Gamma function. This PR is over #1674 and #1761. ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md`...
https://github.com/math-comp/analysis/blob/72c8678f8def77da4c1c2682f857cfb8cf770352/theories/normedtype_theory/normed_module.v#L1799 @IshiguroYoshihiro @holgerthies