2021 09 28 Meeting

Participants: Reynald Affeldt, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, Laurent Thery

• issue https://github.com/math-comp/analysis/issues/157 about the documentation of filters
  • about the 1st point: define what is "canonical"
  • about the 2nd point:
    • we have overloading: we first coerce using the element and then infer the filter
    • the goal is to be able to talk about a limit of a filter in R while covering both the finite and the infinite case, as in convergence in \bar R
    • TODO: provide an example to solve this issue
      • maybe not used yet in fact, put as undocumented until there is an actual use
    • LT: document the fact that it is a read-only notation
• https://github.com/math-comp/analysis/pull/411 (is_interval large inequalities)
  • OK to merge
• https://github.com/math-comp/analysis/pull/374 (dual real)
  • -oo + +oo = +oo
  • CC: notice a problem with scopes
  • TODO: CC to do the review after a fix by PR
  • put a link to the development that uses this feature as part of the documenting header?
• CC: put Coq developments depending on MathComp-Analysis in nix and coq-packages to have the CI check the dependencies
  • see README in https://github.com/coq-community/coq-nix-toolbox
• https://github.com/math-comp/analysis/pull/438 (T0, T1)
  • TODO: reformat definitions and double-check statements
  • ZS: raise a more general question, use filter meet for these definitions?
    • CC: favor filter definition, equivalence with the same description in terms of sets
  • TODO: merge almost as is, just do reformatting
  • TODO: RA to review
• https://github.com/math-comp/analysis/pull/311 (domain restriction)
  • CC have a completed branch and just need to update the changelog
  • NB: ZS unavailable for the next two weeks
  • the patch function should replace fer in the PRs on integration
• https://github.com/math-comp/analysis/pull/410 (subspace)
  • CC has almost completed his review
  • this PR can be uses in the "continuous inverse PR" to replace continuity on a segment but there is no need to be delay the merge, this can be fixes later
  • ZS: see also https://github.com/math-comp/analysis/issues/408 to weaken the statement of the mean value theorem using continuity at the end points but on the subspace topology
• https://github.com/math-comp/analysis/pull/385 (continuous inverse)
  • TODO: update changelog, put the right lemmas in the right places, create a realfun.v file, before merging the trigo PR
  • TODO: AR to commit
• https://github.com/math-comp/analysis/pull/383 (trigo)
  • most things to go in realfun.v
  • TODO: get rid of names with prime suffixes
  • CC: it is only about R for the exponential? LT: yes
  • some things could be subsumed by power series (notation of radius of convergence, etc)
  • TODO: ping TS about that and report on Zulip
  • ZS: the Arzela-Ascoli PR contains some related elements
• https://github.com/math-comp/analysis/pull/434 (density of rat)
  • rename archimedean
  • prove the relation with the dense predicate, it should be 5 lines
  • TODO: AR
• https://github.com/math-comp/analysis/pull/435 (rat is countable)
  • redundancy with domain restriction
  • leq_card predicate should be better defined
  • should be merged after the domain restriction PR
• inclusion in the Coq platform?
  • see messsage on Zulip and also https://github.com/coq/platform/issues/21#issuecomment-929068379
  • as "full"
• a quick work about getting rid of the type classes by CC
  • approach: copy the infrastructure for subalgebra (submodules, etc.) predicaates from MathComp
• TODO: AR to release 0.3.11
• https://github.com/math-comp/analysis/pull/398
  • lra to realType
    • it is not parametrical yet, it is based on a certificate, no relation with mczify
  • just work with the R in RStruct as of today