2020 11 05 Meeting - math-comp/analysis GitHub Wiki

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