2020 06 17 Meeting

Participants: Cyril, Marie, Kazuhiko, Reynald

• https://github.com/math-comp/analysis/pull/180
  • lim notation requires more precise [lim ... in ...] notation.
  • we sometimes need to explicitly write types
  • TODO: run hierarchy.ml to find missing joins (Kazuhiko?)
• https://github.com/math-comp/analysis/pull/205
  • goal trying to get rid of ^o's
  • we need to give an lmodtype structure on the normed module to type check the scalar product
  • we have a canonical way to build normed modules for numFieldType's
  • TODOs:
    • in normedtype.v, Canonical numFieldType_pseudoMetricType := @PseudoMetric.Pack ... should not be a Pack but a packager
      • TODO: add this information to the CONTRIBUTING.md file
    • afte`r realField_lmodType
    • go on with LalgType up to field extension
    • squash this commit
• https://github.com/math-comp/analysis/issues/3
  • remove Rbar.v
• https://github.com/math-comp/analysis/issues/228
  • keep both sets of lemmas
  • use the suffix "E" for equations, use the prefix "not_" for views starting with a negation, put "P" at the end of view lemmas, "eqNNP" -> "eqNN", "forallN" -> "forallNE", "existsN" -> "existsNE", "existsNP" -> "existsNP", "existsPN" -> "not_existsP", "forallNP" -> "forallNP", "forallPN" -> "not_forallP"
• https://github.com/math-comp/analysis/pull/220
  • merged
• https://github.com/math-comp/analysis/pull/204
  • postponed
• Issues related to Landau notations
  • comes from difficulties working with holomorphy
    • difficulties rewriting Landau notations to non-Landau notations
    • makes it impossible to use derive.v
    • see: https://coq.zulipchat.com/#narrow/stream/237666-math-comp-analysis/topic/landau
  • Hints:
    • see definition 4.2.1 in https://hal.inria.fr/hal-01719918v3
    • should use the notation "f = g + '+o_' x e" because it chooses the witness
    • use eqaddOP to have an arbitrary witness
    • should we provide an interface w.o. Landau notations?
    • TODO: work to be rebooted in a week or two
• https://github.com/math-comp/analysis/pull/223
  • take out outer measure and put it in the integral sketch PR
  • is_measure, is_outer_measure -> remove is_
  • TODO:
    • go on like that with outer measure even though this is a specialized definition
    • prove convergence properties of extended reals in an ad hoc way
• IJCAR 2020:
  • have an outline ready by monday
• release 0.3.2
  • with the Boole inequality and pending cleaning