search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
197 stars 44 forks source link

improve `Rstruct.v` #1014

Open affeldt-aist opened 1 year ago

affeldt-aist commented 1 year ago

It turns out that Rstruct.v was useful in PR #1002 and is also useful in porting results from infotheo (https://github.com/affeldt-aist/infotheo) to MathComp-Analysis but the file has not been maintained as well as other files. Improvements are welcome.

affeldt-aist commented 9 months ago

We have been using more extensively Rstruct.v for infotheo.0.6.0. In particular, @t6s realized that we can now use the following, easier lemmas about Rinv and Rdiv: https://github.com/affeldt-aist/infotheo/blob/master/lib/ssrR.v#L642C1-L652C37 This can already be PRed as an improvement. More generally, we should maybe reflect a bit on what we did with infotheo to PR a bit more improvements. For example, real_realType is a bit longish for an identifier. A multirule such as https://github.com/affeldt-aist/infotheo/blob/master/lib/ssrR.v#L657 might also be an improvement. Should the lemmas about bigop also be part of the PR? Mayve sumRE should not even exist but I am less sure about bigmaxRE.

affeldt-aist commented 1 month ago

Note that this (now merged PR) already introduced a few improvements: https://github.com/math-comp/analysis/pull/1235