analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change address comment https://github.com/math-comp/analysis/pull/990/files/e686555022776816f6c70e98c00a1e6fd5923f95#diff-5edc277f753b88b71edd27b04c3075df73e37652e4c19c0f8dc6210fa57bf926 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers ##### Compatibility with...
##### Motivation for this change Adding the theory of topological vector spaces ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation...
It was observed during the MathComp-Analysis dev meeting of 2023-12-21 that the existence of the `coq-mathcomp-classical` is not well-known @Tragicus We should maybe improve the MathComp website https://math-comp.github.io/installation.html so that...
We have been using intervals with extended real numbers but this has the consequence that ``` `[0%E, +oo] = `[0%E, +oo[ ```. How can we handle that? @hoheinzollern @t6s
https://github.com/math-comp/analysis/blob/0e392b5d36dd33e7e054a9a481bf9f4b17a90ed0/classical/set_interval.v#L340 1. rename to `line_path` or `affine_path` 2. add ```coq Definition wadd t a b : R := (1 - t) * a + t * b. ``` (this is...
https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L431 "The multiplication only works for realDomainType (and not for numDomainType), for relatively bad reasons."
https://github.com/math-comp/analysis/blob/81969914159f7f0c957e627a54263eae72871744/theories/realfun.v#L611 "Most of the important lemmas like this one are probably true of limf_sup. At least lime_sup_ge0,, lime_supD, lime_inf_sup, and lim_lime_inf. There may be some conditions to replace with `\forall...
https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L650-L825 "The proof of the multiplication could probably be improved using wlog."
https://github.com/math-comp/analysis/blob/36680bc768401672853271c9981a0c48555c4ab5/theories/itv.v#L845-L891 or at the very least provide a better (informative?) set of tests
https://github.com/math-comp/analysis/blob/7da865547861fd6937802e1f6e99f3c6d7f4b7b6/theories/lebesgue_integral.v#L2760-L2762 NB: has been renamed to `ge0_subset_integral` TODO: use a condition such as `forall x, B x -> ~ A x -> 0