2020 09 28 Meeting

Participants: Marie, Cyril, Kazuhiko, Pierre-Yves, Reynald

• PR 179 (https://github.com/math-comp/analysis/pull/179)
  • has been rebased, on top of PR 183 (https://github.com/math-comp/analysis/pull/183)
  • displays 114 commits
    • might require a rebase --onto
  • the introduction of entourages in the hierarchy is not transparent
    • use nbhs_ballP? look at the files of the merge PR 242 (https://github.com/math-comp/analysis/pull/242/files) for illustration?
  • TODO: put in the header documentation information about crucial lemmas (nbhs_ballP?)
• PR 183 (https://github.com/math-comp/analysis/pull/183)
  • TODO: split into several PRs
    • one with linear-continuous stuff only
    • one with closed_ball (btw, add compacity to it) for further discussion
    • one with Landau notations (but this is for later)
• PR 262 (https://github.com/math-comp/analysis/pull/262)
  • introduces closed_ball which is often more practical than open balls (avoid cutting epsilon's in half)
• stalled PRs
  • PR 205 (https://github.com/math-comp/analysis/pull/205), doubts that it might go as expected
  • PR 204 (https://github.com/math-comp/analysis/pull/204), application envisioned
  • PR 180 (https://github.com/math-comp/analysis/pull/180)
    • problems with filter types can be addressed by selecting simpl's
• TODO: have the CI handle hb (e.g., in https://github.com/math-comp/analysis/pull/224)
• PR 224 (https://github.com/math-comp/analysis/pull/224)
  • Progress report about integral_sketch:
    • started with the file integral.v written by the meeting participants some time ago (just a sketch, in particular no proofs, measurableType not available, theory of extended real numbers under-developed)
    • since then, we have merged into master:
      • a theory of sequences of real numbers (sequences.v)
      • the pseudometric structure of extended real numbers
      • a small theory of sequences of extended real numbers
      • the basics of measurableType (with the proof of the Boole inequality (measure.v))
    • during this summer, we have:
      • further developed the theory of sequences of extended real numbers (PR 264)
      • developed a small theory of countable sums (http://fourier.math.uoc.gr/~mathweb/lnotes/papadimitrakis+graduate-measure-theory.pdf definition 1.4 page 23, proposition 2.3 page 23, proposition 2.6 page 26)
      • based on a small theory of countable sets (cardinality.v))
      • measure.v now features a small hierarchy using hierearchy-builder (SemiRingOfSets, RingOfSets, Measurable) and + definitions of "negligibe" and outer measure
      • measure_wip.v contains two proofs of interest for measure theory (https://lefevre.perso.math.cnrs.fr/PagesPerso/enseignement/Archives/Lebesgue.pdf, theorem 5 page 3 (Caratheodory's theorem), proposition 11 (construction of an outer measure from a measure))
  • discussion on how to use proposition 11 to build Lebesgue's measure, on the use of Caratheodory-Hahn theorem
  • TODO: formalize CH theorem in two steps: first the build measure in terms of a function (Def Hahn_measure := fun x => ...), and then declare a Canonical instance tagged on mu_ext (similarly to ^o) to have a measure on the generated sigma-algebra (instead of Caratheodory)
  • TODO: define the generated sigma-algebra using an inductive type with 3 constructors (the first one for the starting point, the other for complement and union), prove equivalence with the current definition (by intersection)
  • TODO: theorem 15 by Li (construction of the ring of sets of intervals from a semi-ring of sets)
• Issue 255 (https://github.com/math-comp/analysis/issues/255)
  • TODO: framadate with Reynald, Pierre-Yves, and Cyril to merge realseq.v and sequences.v, should take less than two hourse
  • TODO: plan a similar meeting for countable sums after that
• TODO: merging of eudoxus reals
• Issue 261 (https://github.com/math-comp/analysis/issues/261)
  • TODO: extract ereal contents from normedtype.v to ereal.v