2020 11 05 Meeting

Participants: Marie, Kazuhiko, Pierre-Yves, Reynald

Release 0.3.3 this week-end?

• Merged the following:
  • https://github.com/math-comp/analysis/pull/267 (Closed ball)
    • because used by Banach-Steinhaus (draft PR based on it)
    • TODO: rename normrxx
    • TODO: rename the commented lemma with Landau notation and prepare another PR with the lemmas lifted with Landau notations
    • TODO: squash contiguous commits
    • TODO: reynald to review and ping Cyril
  • https://github.com/math-comp/analysis/pull/268 (lemmas about closure and connected)
    • one comment not yet completely addressed
    • however, it used in https://github.com/math-comp/analysis/pull/267 (Closed ball)
    • TODO: marie to take a look at the equivalence limit_point and cluster (globally ...)
  • https://github.com/math-comp/analysis/pull/270 (update the readme and file maintenance)
    • fixes one issue
    • TODO(marie): mention the TYPES abstract by Marie and Assia, put a link to the Hahn-Banach PR?
    • TODO(rei?): link to the slides from the Coq workshop 2018
  • https://github.com/math-comp/analysis/pull/206 (Add a distrLattice canonical structure to set T.) TODO: Kazuhiko to skim through it by [2020-11-06 Fri] TODO: ping Cyril
  • https://github.com/math-comp/analysis/pull/263 (minor changes and additions to ereal.v) ?
    • TODO: ping Cyril
    • TODO: squash the first commits
  • https://github.com/math-comp/analysis/pull/264 (more lemmas about sequences of extended real numbers)
    • no discussion but it has been indirectly improved by the PR it is based on
    • lemmas of interest: lee_lim, ereal_cvgD
    • can still be improved later without causing much trouble
    • integral_sketch depends on it
    • TODO: squash the commits
    • TODO: ping Cyril
• other TODOs:
  • TODO: delete https://github.com/math-comp/analysis/pull/183 (LinearContinuousBounded)
    • because contents duplicated in https://github.com/math-comp/analysis/pull/267 (Closed ball)
  • TODO(marie): document nbhs_ballP in the header to topology.v and possibly also in the FAQ
• wip:
  • https://github.com/math-comp/analysis/pull/204 to be over within two weeks (holomorphy <-> Cauchy-Riemann) working with two different lmodtype structure over the same normedtype by hand TODO: should we make real_complex a coercion?
  • Marie working on https://github.com/math-comp/analysis/pull/205 (Topological structures on numfields)
    • TODO(rei): check that we can compile the master of mathcomp-analysis against the master of mathcomp
      • contact Kazuhiko should a problem occur