Regarding the review of the new measure stuff that came up at the last meeting. I have some time to review stuff, but wanted to coordinate so we don't duplicate effort. I suppose an issue with a checklist for each file to review is the easiest? I'll start with fsbigop, as I'm interested in how that works.
I understand this is measure theory. Can you elaborate about your plans? We're using math-comp in SSProve.
the plans have been discussed in the last mathcomp meeting, it consists in reviewing a posteriori the contents of math-comp/analysis#543
It was actually about the files functions.v
, cardinality.v
, esum.v
and fsbigop.v
(rather than the formalization of measure theory).
Last updated: Oct 13 2024 at 01:02 UTC