Stream: math-comp analysis

Topic: Measure Review

view this post on Zulip Zachary Stone (Mar 01 2022 at 15:48):

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.

view this post on Zulip Bas Spitters (Mar 02 2022 at 13:55):

I understand this is measure theory. Can you elaborate about your plans? We're using math-comp in SSProve.

view this post on Zulip Cyril Cohen (Mar 02 2022 at 16:01):

the plans have been discussed in the last mathcomp meeting, it consists in reviewing a posteriori the contents of math-comp/analysis#543

view this post on Zulip Reynald Affeldt (Mar 03 2022 at 05:45):

It was actually about the files functions.v, cardinality.v, esum.v and fsbigop.v (rather than the formalization of measure theory).

Last updated: Jun 25 2024 at 19:01 UTC