-
Notifications
You must be signed in to change notification settings - Fork 47
2021 12 16 Meeting
Cyril Cohen edited this page Dec 16, 2021
·
4 revisions
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 byeq_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
analysisdirectory - 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 to overloaded?) and kolmogorv_space, haussdorf_space
- PR #487 strict->large inequality
- 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