-
Notifications
You must be signed in to change notification settings - Fork 43
2022 04 12 Meeting
Pierre Roux edited this page Apr 14, 2022
·
5 revisions
Participants: Reynald, Kazuhiko, Takafumi, Yves, Laurent, Zachary, Pierre, Cyril
- News: we have released 0.5 20 days ago
- doc updated as
https://math-comp.github.io/analysis/htmldoc_0_5_0/index.html
- TODO: revert previous documentations
- TS: coqdoc pages should better indicate the version number of mathcomp-analysis
- doc updated as
https://math-comp.github.io/analysis/htmldoc_0_5_0/index.html
- classic/analysis split OPAM packages #600
- Cyril: let's draw a line now
-
boolp
,classical_sets
,functions
,cardinality
,fsbigop
- and maybe a part of
set_interval
-
-
reals
,ereal
, etc., may go in real_closed if they are not too classic or in a further package mathcomp-real, see github's conversation - TODO: to be cont'd during the next meeting
- Cyril: let's draw a line now
- notation
oo
/infty
(#597)- use
y
as a short identifier (i.e., only for suffixes) for infinity - this has been closed by #615
- use
- external contributors can't use the
wish
tag? (see #607)- let's not allow people from outside to add tags
- new notation scheme for integrals, closer to mathcomp's ASCII
- related minor PR: #634
- look at
lebesgue_integral.v
line 32 for an example of the current notation - new proposal:
\int[mu]_(x in D) (f x)
- ZS: ok, 1. as long a there are no subscripts and superscripts the former notation was not so close to the math practice anyway 2. notation looks concise even for Stokes' theorem
- TS commented on differential forms but that should be another integral
- a PR is in preparation
- PR to merge?:
-
#541 (displays for measures)
- same trick as
order.v
- see for example
lebesgue_measure.v
line 1009 - TODO(cyril or reynald?): rebase and merge
- ZS: can we do that in
topology.v
for function space topologies? - the current PR could be a reference to implement such a feature but it uses HB, maybe to wait for MathComp 2.0
- same trick as
-
#624 (renaming of
funennp
)- YB:
nneg
,npos
more natural - new naming scheme:
funepos
,funeneg
- YB:
-
#574 (countable additivity of integral for non-negative functions)
- could somebody approve?
- about naming:
bigsetU_bigcup
->subbigsetU_bigcup
- need the positivity condition for the finite version (
ge0_integral_bigsetU
?) ?
- about naming:
-
#632 (countable additivity for integrable functions)
- postponed
- could somebody approve?
-
#545 (Arzela main lemmas)
- do we need
2735: have PG : ProperFilter G by [].
? - needed a proper filter,
done
finds the proof but not type class resolution - PR is good to go, nothing to add to it
- TODO: approve and merge
- do we need
-
#541 (displays for measures)
- is the use of
esumB
in #628 (equivalence between series and integral over the counting measure) ok? - progress on LRA math-comp/algebra-tactics#54 (time permitting)
- PR has been following advice by KS on Coq code modification (?) and CC advice to use
realDomainType
instead ofrealFieldType
- we now have
lra
,nra
andpsatz
(that calls CSDP) - should be available with Coq 8.16
- PR has been following advice by KS on Coq code modification (?) and CC advice to use
- theory of cantor sets (https://github.com/math-comp/analysis/pull/627)
- moitvation: cantor sets are useful but awful to work with
- status: not ready to merge, just to make sure that nobody's working on it
- consider merging #489 (expressed sup with supremums)?
- it also improves the documentation of reals
- could we merge it and go back to it later?
- TODO: postpone the discussion online
- stalled PR:
- #487 (change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs)
- Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2022-02-24-Meeting)