affeldt-aist issues

Results 148 issues of


                                            affeldt-aist

use set instead of fset in esum

##### 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...

ge0_integral_mscale

##### 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` ~~- [ ]...

Probability

TODO: - [ ] changelog

remove Rstruct lemmas about bigmax?

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...

potential generalization from `realDomainType` to `numDomainType`

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`)

enhancement :sparkles:

change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs

- from strict to large - also adds a few lemmas to `ereal.v` closed #122 @CohenCyril This is globally getting a bit bigger (only a few proofs are shortened). I...

experiment :test_tube:

Redundancies between `realseq.v` and `sequences.v`

There are redundancies between `altreals/realseq.v` (which predates MathComp-Analysis) and the newer `sequences.v`. How should we factorize? Related issue: "The merge of sequences and sums over general sets (see `esum.v` and...

question :question:

renaming/refactoring :wrench:

affeldt-aist