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
fsbigop.v (rather than the formalization of measure theory).
Last updated: Nov 29 2023 at 19:01 UTC