2020 07 24 Meeting

Participants: Cyril, Kazuhiko, Reynald

• about PR 180
  • hierarchy.ml has been run
    • find missing join at the level of complete normed modules so this can't be the source of the problem
  • related to PR 232
  • a quick check revealed an exposed match at line 2016
    • the sort projection is unfolded to a match of pseudoMetricNormedZmodule
  • TODO: investigate: type_of_filter is the culprit?
• about PR 205
  • coercion paths that are not convertible in mathcomp (see PR 546 in mathcomp)
    • this PR should solve the ambiguous paths in mathcomp analysis
      • but it is ad hoc
      • it should use primitive projections for class records
        • sometimes the choice of the base matters (may cause ambiguous paths)
      • e.g., comUnitRing
    • TODO(cyril): put this in the next mathcomp meeting with high priority
    • TODO(marie?): don't wait for the fix, use Kazuhiko's branch 546
• about PR 204
  • (skipped)
• about Landau notations
  • PR 216 has been merged
  • issue postponed to a next meeting once more concrete input is available
• PR 233
  • to merge once green lighted
  • TODO: missing lemma open_nbhsE : open_nbhsP = open && nbhs
    • add asap or create an issue
• PR 224
  • ereal_cvg_ge0 should be a one-liner using the closedness property on the model of lim_ge (sequences.v)
  • TODO: fix fin_ereal_cvg_neg
    1. "unlift" (from ereal to real)
    2. using cvg_comp_addn
  • sketch for a better proof of ereal_cvgD:
    1. adde is continuous as a binary function
    2. case analysis
  • about Caratheodory's theorem
    • the interface of outer_measure is not on the right carrier
    • it should be setRingType (https://en.wikipedia.org/wiki/Ring_of_sets)
• PR 236
  • NB: lte_ conflicts with interval conventions but let's take care of this later
• 0.3.2
  • release shortly after merging the PR that renames locally to nbhs
• contributing guide
  • avoid direct proofs about sequences
    • use instead lemmas such as closed_cvg_loc, cvg_comp_addn, etc.
  • TODO: use this experience to enrich the contributing guide
• about dead branches
  • do not delete summability
  • merge summability, realseq and sequences
  • realsum is an independent development
  • TODO: open an issue about this topic