2021 06 22 Meeting

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
  • monotonicity of the inverse should be proved first and continuity derived from it
  • might solve one admitted in PR https://github.com/math-comp/analysis/pull/383 (the one about continuity)

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?

• postponed
  • Saikawa-san raised the question by opening a draft PR https://github.com/math-comp/analysis/pull/396
  • NB: previous contribution by Hivert https://github.com/hivert/FormalPowerSeries

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

• (Reynald observes that we use lra a lot in in https://github.com/affeldt-aist/infotheo)
• see also nsatz automation in https://github.com/math-comp/analysis/blob/1e98b26313131c612074fc3feccdd6c4852c4349/theories/nsatz_realtype.v

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

• TODO: ask developers about a timeline