analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change This PR defines `esum` using `finite_set` instead of `fset`. TODO: ~- rename `fsets`~ (not sure anymore... maybe `fsubsets`?) some small proofs become useless but on...
##### Motivation for this change integration over a scaled measure (useful to deal with probabilities) ##### Things done/to do - [ x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ]...
Fixes #550 Classical currently contains boolp and classical_sets, we may also consider adding functions and signed there.
https://github.com/math-comp/analysis/blob/2ae3b628d12cacdc000c4cd70e6f3cae26ecf429/theories/Rstruct.v#L502-L671 It looks like we do not use these lemmas anymore and since there are already bigmax/bigmin lemmas (see e.g. PR #712 ) in master should we think about removing...
I'm encountering some issues with certain applications of the `near` tactics. One set of issues is getting instances of `\near F, ...` to typecheck. The example that I encountered was...
In the spirit of giving real-world reproductions, rather than minimal ones, here's a failed attempt from the arzela ascoli proofs. I proved ``` Lemma small_ent_split {Y : uniformType} (E :...
https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2037 https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2266 https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2279 (also `lee_pmul2l` and `lee_pmul2r`)
https://github.com/math-comp/analysis/blob/3404704fa195f16d5035d8d87806e155dc6d5581/topology.v#L33
After PR[#267](https://github.com/math-comp/analysis/pull/267) is merged, should we add to `landau.v` lemmas about bounded functions using landau notations ? [This](https://github.com/math-comp/analysis/blob/309f5131169a15542e29d9e55a0ee23a2bb67862/theories/banachsteinhaus.v#L219) is needed for Banach-Steinhauss for example. NB(rei): PR #267 has been closed...
