2022 07 27 Meeting

Participants: Reynald, Laurent, Cyril, Takafumi, Pierre

• Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2022-04-12-Meeting)
• splitting of ereal.v and of analysis: decide a schedule
  • Split ereal.v in ereal.v and classical_ereal.v (#645) this would allow to move ereal.v to mathcomp-algebra and use it in interval.v, simplifying it
  • classic/analysis split OPAM packages (#600)
  • these PRs are mostly ready
  • TODO: design a nix package architecture before the next rebase of the split of analysis
    • another instance of multiple packages in one directory: automate?
  • agreed on the split of ereal.v and its moving to mathcomp
    • NB: https://github.com/math-comp/real-closed/pull/29
  • TODO: split for 0.6 (before [2022-09-30 Fri])
• HB port has started PR #698
  • following the recent completion of the port of mathcomp to HB PR #733
• FYI: coqdoc documentation still wip
  • see the current result here: https://math-comp.github.io/analysis/htmldoc_0_5_2/
  • reminder: how to document
  • NB: the HB port will trigger documentation changes
  • e.g.: issue, https://github.com/math-comp/analysis/issues/658
  • please: at least generate issue for missing documentation
• discussion: type of reals within an interval
  • extending signed.v to intervals ?
    • (could be useful for [0, 1) intervals: https://github.com/math-comp/analysis/pull/678#issuecomment-1161335738)
  • what about this approach to "reals into [0, 1]":
    • link to infotheo
    • proved useful in previous work
    • we would like to introduce it in mathcomp-analysis to define, e.g., Bernoulli distributions
  • application to Banach fixpoint theorem? PR #678
  • another approaches:
    • automation-based tools, defer to lra, trigger a resolution in coq-elpi and ultimately called lra
    • use the same idea of abstract interpretation using a deep embedding of a polytope representation
      • there should be related work on polytopes, e.g., https://github.com/Coq-Polyhedra/Coq-Polyhedra
    • leverage on Interval? (would be less precise than polytopes, does not distinguish open and closed)
  • TODO: Pierre to have a closer look at interval
• issue triaging:
  • issue about nix: https://github.com/math-comp/analysis/issues/699
  • update the doc to mention the daemon/no-daemon option (maybe recommend the daemon option)
    • Pierre never got the daemon option to work
• PR triaging:
  • about iter: PR #690
  • might need attention: PR #674
  • about measure theory:
    • merge PR #706?
    • merge PR #705?
      • maybe a bit long, k in R and condition that k is nonneg so that when we apply the lemma we do not need to shape the arguments
    • merge PR $636?
    • status of PR #672?
      • there was a workaround with a stack overflow, still pending
      • measurable comRingType, etc. might be another solution, we need to be sure it doesn't cause a stackoverflow
    • fyi: Lebesgue-Stieljes measure PR #677 to take the place of the Lebesgue measure
    • fyi: basics of probability is now axiom free PR #516 but still needs work
      • we need several passes of review
      • discrete RV using HB instead of telescope
      • notation for p.-integrable
      • mpushforward rather than pushfoward
  • still pending: PR #487