2025‐04‐11 Meeting

Participants: Alessandro, Cyril, Kazuhiko, Marie, Pierre, Quentin, Reynald, Takafumi, Yosuke, Zachary

• work in progress: the online documentation

  • using rocq-navi, now available on opam (see)

• per-PR changelog, similar to https://github.com/math-comp/math-comp/pull/1328

  • should we keep the name of the author of the PR in the changelog?
    • maybe not
  • are changes reorganized for each file?
    • should be done
  • anyway, we cannot avoid curating the changelog in the end
  • tak: adding comment to lemmas to have the history of name changes and changes in statement?
    • cyr: we need an attribute in Rocq to keep the history
    • TODO: RFCs https://github.com/rocq-prover/rfcs
  • tak: adding in separated changelog a description of the intent of the PR in addition to the number of the PR
    • maybe not needed because there is a link

• check unstable.v

  • mathcomp_extra.v were welcoming things that were actually not backported as such
  • now mathcomp_extra.v just duplicates the information that is already backported
  • https://github.com/math-comp/analysis/blob/master/classical/unstable.v
  • check unstable.v to elect things to be backported (but not before the release, too much work the release manager)
  • when do we flush that?
    • during the meetings and the sharing day

• add lra and interval to the dependencies? (ale)

  • CoqInterval depends on the stdlib so no (pie)
  • ale: special packet for experiments/applications of MathComp-Analysis?
    • like showcase (showcase not intended to be reused)
    • like experimental_reals (pi) ?
  • cyr: we just need to rewrite from mathcomp to the stdlib and call the interval tactic
    • pie: this is already in Rstruct.v
    • produce a table for every real function (sin, cos, +, *, etc.), they are not the same that ours but we can have theorems
  • tak: evaluation of Taylor expansion?
    • need to prove that Lebesgue and Riemann from the standard library agree
    • cyr: does the standard library handle piecewise-continuous? yes (pie)
  • TODO: is showcase the right word?
  • TODO(rei): new package for sfppl
  • TODO: sampling theorem -> might end up to analysis_stdlib

• move separation_axioms.v into topology_theory

  • tak: why is it outside?
    • no specific reason
  • breaking change?
    • should not break external development
  • TODO: PR (list it in topology.v? -> yes! (zak))

• splitting of normedtype.v: PR 1544

  • Marie ok with the split and the fix
  • TODO(zac): review
    • urysohn.v might end up in topology
    • put a deprecation notice before urysohn in the Export file for the transition
  • tvs.v will depend on pseudometric_normed_Zmodule.v file
    • lemmas standard_add_continuous and standard_scale_continuous are duplicates
    • TODO: try later to eliminate these duplicates
    • NB(que): take the standard_topology section outside of the file and maybe this tvs.v should not be moved to normedtyped.v

• cumulative distribution function

  • intended to be used in actuary
  • TODO: merge
  • cdf should be an instance of Cumulative
    • cumulative is R -> R
    • cdf is R -> \bar R
  • TODO: generalize to topological order space, just add an instance of cumulative as a separate
  • generalize later (e.g., cadlag)

• lspace master

  • Lp norm are defined with codomain \bar R but specialized everywhere to R, this should be uniformized
  • generalizing the p?
    • this has actually been generalized but need check
  • generalizing the function? e.g., l.475: Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)).
  • the goal is to uniformize to help future changes
  • functions should never by cast to reals
  • TODO(ale, rei): review all the lemmas
  • milestone: 1.11

• PR triaging:

  • about derive incr/decr lemmas
    • TODO(cyr): review
  • normal pdf
    • TODO: Yosuke to take a look?
  • variants of deriveMr and deriveMl
    • The problem is that ^`() is in %R
    • TODO: put that in function_scope (automatically inserted when it is in function application! (default Rocq behavior))
  • finite transition kernels
    • TODO(ale): review

• prod/pair naming issue 1514

  • TODO(cyr): review

• Small lemmas from the formalization of the Gamma function

  • easy generalization
  • limits of ln and powR functions
  • TODO(zak): review

• PR 1491 --- Boost derive

  • TODO: merge when CI green

• recurring topic: flush unstable.v

  • maxr_absE, minr_absE go to ssrnum.v
  • TODO(rei): PR

• about the naming of weak topologies: new issue