-
Notifications
You must be signed in to change notification settings - Fork 43
2023 06 21 Meeting
affeldt-aist edited this page Jun 21, 2023
·
2 revisions
Participants: Reynald, Cyril, Pierre, Julien, Zachary, Takafumi
- splitting files
-
topology.v
into multiple files?- split into 4 files, all at once:
- filters + near
- topology
- uniformity + completeness
- function space topologies (because of many notations, etc.)
- wait for hierarchy-builder (because otherwise it will be painful to cherry-pick)
- plan the mca release 1.0.0 to be based on HB
- wait for the FTC?
- there is the subspace problem about derivatives
- wait for the FTC?
- derivable on the interior should be a reasonable restriction to allow for the FTC
- still we do not want to wait for this theorem to release 1.0.0
- performance problem right now, compiling mca is 45 min. while mc is 35 min.
- there is hope that this will improve in the near future though
- plan a 0.6.4 and waita bit for performance improvements
- plan 0.6.4 in July
- plan 1.0.0 in September
- split of topology to happen in August once master is set to HB
- performance problem right now, compiling mca is 45 min. while mc is 35 min.
- splitting of topology should maybe be thought together with an update of the documentation header
to follow https://github.com/math-comp/math-comp/wiki/How-to-document
(see
measure.v
for an example in MathComp-Analysis) (even before moving to the hiearchy-builder version)- there is also the problem of the changelog
- split into 4 files, all at once:
-
lebesgue_integral.v
into (1) one file up-to non-negative simple functions and (2) the rest?- yes
- because in the near future we want to replace the integral by the Bochner integral
- a matter of months rather than weeks, should make it easier to deal with extended real numbers though
- need to define the space of all linear functionals, the subspace of all linear continuous functionals, etc.
- also needs the theory of dual spaces
- Cyril: don't we have the solution for subspaces?
- Zachary:
- for a function at a time yes
- some properties are nice expressed with types, other with sets, so the subspace solution does not solve everything
- TODO(Zachary->Cyril): illustration with a concrete problem in the path development
- Cyril: this is not a problem of displays? (i.e., absence of robust notations)
- Zachary: the problem is when working with the type, sometimes we want the whole type
- yes
-
- about the documentation
- example of poorly formatted doc: https://math-comp.github.io/analysis/htmldoc_0_6_3/mathcomp.analysis.measure.html
- should we hack the parser again?
- Cyril: make an issue to have md in coqdoc, otherwise we'll have to do escaping
- TODO: special set rule for the << >>
- TODO: try to put the whole header in verbatim to see what goes out
- Pierre: Should we try https://coq.inria.fr/refman/using/tools/coqdoc.html#verbatim
- Cyril: https://github.com/math-comp/math-comp/blob/master/etc/utils/builddoc_lib.sh
- TODO: more over, there is a problem with HB commands
- Cyril: make an issue to have md in coqdoc, otherwise we'll have to do escaping
- what to do with https://math-comp.github.io/analysis/?
- TODO(rei): put a link in the readme with a disclaimer
- after the split of the
classical
package, what about further packages? reals? topology?- some user only want the real numbers (Rstruct.v, reals.v only?)
- put reals under classical?
- constructive_ereal is also independent
- separate package for everything that is before topology.v? for measure theory?
- let's wait for the HB branch
- some user only want the real numbers (Rstruct.v, reals.v only?)
- PR triaging:
-
https://github.com/math-comp/analysis/pull/915 (smallest filter)
- maybe rename smallest_filter_stage
- smallest_filter is not a good choice because there are several choices
- current way is by taking finite intersections but it used to be built all at once
- 2nd version: it is helpful to have it built inductively
- 3rd version: intersection of all filters containing the a set
- having a version without the choice type was convenient
- Urysohn's lemma ready for review?
- current definition of metric space does not guarantee the metric function in R
- we need a slightly stronger structure (for a every two points, there is a ball that contains both)
- that guarantees the metric that we need for Urysohn's lemma
- we want it to be non-Hausdorff
- the proof cannot be completed without HB
- the last mile should be done with the HB branch only
-
https://github.com/math-comp/analysis/pull/939 (minor fixes and additions to
exp.v
)- used for Hoelder and Minkowski
- TODO: zachary to take a look
-
https://github.com/math-comp/analysis/pull/950 (opam files for hierachy-builder branch)
- merged
-
https://github.com/math-comp/analysis/pull/677 (Lebesgue-Stieltjes)
- show case subdir for the module about Lebesgue measure?
- Stieltjes is a strict generalization
- merge both files?
- Saikwa: about the Sorgenfrey line?
- shouldn't be there anyway
- not a blocker
- it should simplofy a bit the definition: not a new structure but the same notion of continuous but over a different domain, but you sill need non-decreasing
- we should have a structure for continuity but this involves subspaces
- Cumulative makes sense anyway for probability
-
https://github.com/math-comp/analysis/pull/915 (smallest filter)
- help wanted: https://github.com/math-comp/analysis/pull/917 (C1 and lipschitz)
- what about the current definition of C1?
- fix: derivable f b 1
- line 75 is wrong -> ask f' to converge without saying to what it converges
- line 76 is broken: it computes f' at a (f' is two-sided!)
-> take the open interval (within + open is the same as using
in
, there is a lemma for that)
- f uniformly continuous on the open interval it has a limit on the end-points (converges to the right and left correctly)
- try to get away without the value of the derivatives of the end points
- "don't take derivatives on closed intervals"
- what about the current definition of C1?
- other questions?
- status of probability.v
-
https://github.com/math-comp/analysis/pull/834
- cantor sets are used to find counter-examples but not sure they are useful for the FTC
- TODO(rei): review
- outline of the proof is reasonable but the details might not be that important
- not really an original proof but a refactoring of the standard proof
two standard proofs:
- for every compac metric space there is a continuous surjection from a cantor set
- two approaches:
- embed that space in a larger one
- contruct a finitely branching tree and build two functions with the same technique the PR has factored out the technique