Skip to content

2021 06 22 Meeting

affeldt-aist edited this page Jun 22, 2021 · 3 revisions

Participants: Zachary, Reynald, Pierre, Marie, Yves

About PR https://github.com/math-comp/analysis/pull/311

  • ok with pred instead of set in patch
  • TODO: changelog
  • TODO: merge by the end of the week

About PR https://github.com/math-comp/analysis/pull/397

  • create a new file for advanced topology with Arzela-Ascoli instead of appending to topology.v?
    • and other advanced topology results such as Tychonoff?

About PR https://github.com/math-comp/analysis/pull/180

  • direction is to merge
  • TODO(marie): make a list of the points that we do not understand yet
  • TODO: ask for a review by the end of the week
  • TODO: merge

About PR https://github.com/math-comp/analysis/pull/318

  • reminder: main result is the geometric series converges compactly
    • should go to sequences.v
  • waiting for hb, ok if it takes time

About PR https://github.com/math-comp/analysis/pull/385

  • work in progress, may still need one or two weeks

About issue https://github.com/math-comp/analysis/issues/271

  • TODO(marie): open a PR to solve this issue by next Tuesday

Inputs about the formalization of power series?

Pierre proposes lra automation with R: https://github.com/math-comp/analysis/pull/398

TODO: plan a week to work on porting mathcomp-analysis

  • TODO: ask developers about a timeline