2023 10 16 Meeting - math-comp/analysis GitHub Wiki

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