Skip to content

2022 04 12 Meeting

Jump to bottom
Pierre Roux edited this page Apr 12, 2022 · 5 revisions

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

  • News: we have released 0.5 20 days ago
  • 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
    • we now have lra, nra and psatz (that calls CSDP)
    • 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)
Clone this wiki locally