Skip to content

2020 07 24 Meeting

affeldt-aist edited this page Jul 25, 2020 · 3 revisions

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
  • 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