2021 12 16 Meeting - math-comp/analysis GitHub Wiki

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