2021 12 16 Meeting

Participants: Cyril, Kazuhiko, Marie, Pierre, Reynald, Takafumi, Zachary

• PR #410 (subspace)
  • generic construction that should maybe be tested more
  • Cyril refactored it
  • Marie asking about extending the definition to sub normed spaces for application to sub vector spaces and topological spaces
  • Cyril thinks that it can be extended to encompass that kind of applications
  • one last look before merging
    • TODO: Reynald will go through it
• PR #474 (hausdorff product)
  • needed for PR [#397]
  • TODO: we should remove Eqdep_dec.eq_rect_eq_dec, can be replaced by eq_axiomK
• status of PR #397 (Arzela-Ascoli)
  • the proof is not nice enough, Zachary is splitting it into smaller pieces
  • maybe two or more PRs to extract from it (at least the two directions of the theorem, and about equi-continuity)
• PR #489 about the definition of sup
  • sup for reals: 0 when it is unbounded or empty
  • sup for ereals: -oo when empty and +oo when unbounded
  • it looks fine
  • Cyril: the supremum cannot return always an extended element, because on \bar R it would return a \bar (\bar R)
  • Is the lacking structure conditionally complete lattices?
    • Pierre: there are complete lattices in dioid
  • Cyril: make explicit conditions about boundedness and nonemptyness in the general theory of supremums, and have a specialized version for lattices with a top and bottom (such as \bar X)
  • TODO: document reals.v (Cyril to issue)
• issue #154 (Missing canonical declaration in topology.v)
  • probably not done, we addressed for arbitrary numFieldTypes, we might need to several instantiations for the real closure
  • TODO: Marie to push cauchetoile.v
• Will PR #492 close PR #83?
  • yes, but not because it subsumes it, but rather maybe because it make it useless
• About documentation:
  • PR #457 adding coqdoc files
  • important to have an online documentation
  • TODO: PR on the mathcomp website in a analysis directory
  • NB: doc with alectryon for later (see https://github.com/math-comp/analysis/pull/458 for issues)
    • TODO: use 4.07 to generate the doc
• easy PRs:
  • PR #487 strict->large inequality
    • TODO: make it also for pinfty_nbhs and ninfty_nbhs
    • TODO: have lemmas to switch from large to strict
    • TODO: the size should be decreasing
  • PR #472 cover lemmas
    • should be ok
  • PR #438 T0, T1
    • maybe later reintroduce T0 and T1 names as notations
    • maybe accessible_space (frechet too overloaded?) and kolmogorv_space, haussdorf_space
• PR #383 and what we should do with power series (Laurent)
  • pseries should be marked as experimental
  • TODO: do a pass and propose a merge by next week (Reynald)
  • TODO: contact florent about formal power series
  • NB: truncated power series to handle power series constructively
  • TODO: work on the topic with Takafumi by next month
• Add MathComp-Analysis to https://github.com/coq/coq/tree/master/dev/ci?
  • Proposed by Bas Spitters
  • we need to add finmap (coq-elpi is already there) and bigenough and then add analysis
  • TODO: rediscuss that on zulip in a week or two
• TODO: release 0.3.12
• Next meeting at the end of January
  • poll: January 17-21