2023 10 16 Meeting

Participants: Alessandro, Cyril, Pierre, Quentin, Reynald, Takafumi, Zachary

• merge the Idioms section of CONTRIBUTING.md and the Wiki FAQ ?
  • CONTRIBUTING.md: not a good idea, it triggers compilation
  • Alessandro should be given rights
  • TODO(rei): let's merge into the wiki
• PR triaging:
  • PRs used to prove Chernoff's bound
    • PR 1061 (the composition of mfun's is an mfun)
      • looks ok even though f f is specialized
      • related issue: https://github.com/math-comp/analysis/issues/662
    • the problem is that we do not get the real measurable type but the discrete measurable type
    • TODO(Cyr): to try again?
      • ok to merge even without a generic solution but mark it clearly as limitation
    • PR 1060 (properties of normr that couldn't be found)
      • PR to mathcomp_extra.v and also MathComp
      • Pierre: add gt0 and le0 versions
    • MathComp as Num.pos but no Num.nonpos
      • TODO(ale): add the missing notation to MathComp
  • PR 1047 (generalization of expR to extended real numbers)
    • TODO: changelog and documentation
  • PR 1000 (Minkowski's inequality)
    • CHANGELOG needs to be cleaned (le_bigseq_seq, etc. are unrelated)
    • some repetitions wrt to ge0_le_integral, may be factorized by doing several le_trans's in one-go
    • TODO(ale): to go through the script before review
• undraft https://github.com/math-comp/analysis/pull/1041 ?
  • contains the counterexample of https://github.com/math-comp/analysis/pull/1040 but thanks to a weird hypothesis (an assumption that something like complete numbers exist)
  • mergeable right away, modulo changelog
  • does it supersede https://github.com/math-comp/analysis/pull/1040 ?
    • no, because this one does not have the weird hypothesis but rely on real-closed
    • TODO: keep this PR until we rely on real-closed
• MathComp-Analysis 1.0 (for MathComp 2) to be released in January 2024?
  • although a MathComp 2 branch is kept up-to-date, it has a number of "competing inheritance path" warnings...
    • the ones in the module numFieldTopology (for numdomaintype, etc.) are intentional, it are inside a module and are marked appropriately https://github.com/math-comp/analysis/blob/hierarchy-builder/theories/topology.v#L5531C37-L5547
    • NB: there is an option to selectively silence warnings of HB
    • topology.v:5448 is a tricky warning
      • sometimes we rely on the fact that point is 0
      • Cyril: we should put point at the bottom and have the 0 of ZModType to be the point
      • Pierre: should pointed be in MathComp?
      • Zachary: would prefer to have Pointed out
    • normedtype.v:3719
      • this one should be encapsulated in a module
      • problems comes from the fact that we do not use a single type for real numbers
      • the solution should be to reason modulo isomorphism
  • Pierre: we also need to complete the documentation before releasing MathComp 1
  • NB: MathComp-Analysis 0.6.6 also planned
• follow-up from the last meeting:
  • balls in Vitali's lemmas:
    • tentative definition: https://github.com/affeldt-aist/analysis/blob/vitali_lemma/theories/normedtype.v#L6162-L6177
    • new statement: https://github.com/affeldt-aist/analysis/blob/vitali_lemma/theories/normedtype.v#L6311-L6321
  • Cyril: this is indeed what I had in mind
• issue triaging:
  • renamings:
    • https://github.com/math-comp/analysis/issues/1051
    • https://github.com/math-comp/analysis/issues/1052
  • Cyril: these renaming are ok
• Assigning PRs:
  • https://github.com/math-comp/analysis/pull/834 (Alexandroff-Hausdorff Theorem and the Cantor Space)
    • compact metric space is the continuous image from the cantor space
    • mostly internal code
    • not a textbook proof, but a textbook proof in a more convenient format
    • TODO(rei): to look at it but not before Friday
  • https://github.com/math-comp/analysis/pull/926 (Curry is continuous)
    • curry is an isomorphism (lemma needed for homotopy)
    • definition of the compact-open topology
    • useful to define Cartesian Closed Categories locally compact (in fact, this could be weakened) are CC
    • it is still a draft because it should be split in two
• Takafumi: any work on Stone's representation theorem?
  • totally disconnected Hausdorff spaces are in 1-to-1 with boolean algebra
  • there is an algebra of open-closed sets with a uniqueness property
  • Zachary:
    • PR #834 contains some results about totally disconnected spaces (0-dim implies totally disconnected, etc.)
    • we certainly have enough to state it
• https://github.com/math-comp/analysis/pull/677 (Lebesgue-Stieltjes)
  • TODO: Takafumi to review