2022 04 12 Meeting

Participants: Reynald, Kazuhiko, Takafumi, Yves, Laurent, Zachary, Pierre, Cyril

• News: we have released 0.5 20 days ago
  • doc updated as https://math-comp.github.io/analysis/htmldoc_0_5_0/index.html
    • TODO: revert previous documentations
    • TS: coqdoc pages should better indicate the version number of mathcomp-analysis
• classic/analysis split OPAM packages #600
  • Cyril: let's draw a line now
    • boolp, classical_sets, functions, cardinality, fsbigop
    • and maybe a part of set_interval
  • Pierre has a longer list including reals, ereal, etc., see github's conversation
  • TODO: to be cont'd during the next meeting
• notation oo/infty (#597)
  • use y as a short identifier (i.e., only for suffixes) for infinity
  • this has been closed by #615
• external contributors can't use the wish tag? (see #607)
  • let's not allow people from outside to add tags
• new notation scheme for integrals, closer to mathcomp's ASCII
  • related minor PR: #634
  • look at lebesgue_integral.v line 32 for an example of the current notation
  • new proposal: \int[mu]_(x in D) (f x)
    • ZS: ok, notation looks concise even for Stokes' theorem
    • TS commented on differential forms but that should be another integral
  • a PR is in preparation
• PR to merge?:
  • #541 (displays for measures)
    • same trick as order.v
    • see for example lebesgue_measure.v line 1009
    • TODO(cyril or reynald?): rebase and merge
    • ZS: can we do that in topology.v for function space topologies?
    • the current PR could be a reference to implement such a feature but it uses HB, maybe to wait for MathComp 2.0
  • #624 (renaming of funennp) 　　 * YB: nneg, npos more natural
    • new naming scheme: funepos, funeneg
  • #574 (countable additivity of integral for non-negative functions)
    • could somebody approve?
      • about naming: bigsetU_bigcup -> subbigsetU_bigcup
      • need the positivity condition for the finite version (ge0_integral_bigsetU?) ?
    • #632 (countable additivity for integrable functions)
      • postponed
  • #545 (Arzela main lemmas)
    • do we need 2735: have PG : ProperFilter G by [].?
    • needed a proper filter, done finds the proof but not type class resolution
    • PR is good to go, nothing to add to it
    • TODO: approve and merge
• is the use of esumB in #628 (equivalence between series and integral over the counting measure) ok?
  • based on #598 (counting measure)
  • assumes
    • #614 (improvements of sequences.v)
    • #616 (dirac measure)
    • #620 (sum of measures)
  • TODO: RA to assign PRs
• progress on LRA math-comp/algebra-tactics#54 (time permitting)
  • PR has been following advice by KS on Coq code modification (?) and CC advice to use realDomainType instead of realFieldType
  • should be available with Coq 8.16
• theory of cantor sets (https://github.com/math-comp/analysis/pull/627)
  • moitvation: cantor sets are useful but awful to work with
  • status: not ready to merge, just to make sure that nobody's working on it
• consider merging #489 (expressed sup with supremums)?
  • it also improves the documentation of reals
  • could we merge it and go back to it later?
  • TODO: postpone the discussion online
• stalled PR:
  • #487 (change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs)
• Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2022-02-24-Meeting)