Skip to content

2022 02 24 Meeting

Jump to bottom
affeldt-aist edited this page Feb 25, 2022 · 2 revisions

Participants: Cyril, Laurent, Marie, Pierre, Reynald, Yves, Zachary

  • issue 498 (wish list?)
    • a wish could be a ticket.
    • TODO: create a wish label
  • issue 456 (conflict fct_ringType/Morphism)
  • new PR: Tvs and duality theory
    • topological vector spaces
      • interest to define the spectrum of objects
    • interaction of a vector space with its dual (in the sense of vector spaces)
      • interesting when the dimension is not finite
      • certainly nothing yet in mathcomp whose setting is constructive
    • distribution theory
      • link with probability theory? maybe take a look at PR 516
    • some theory about convexity to be merged as part of PR 371
    • about the Zulip stream #linear_zmodType
      • see the space of linear morphisms declared by Zachary at the end of topology.v
  • points to discuss in #511
    • should notations such as %:pos and %:nng be in ring_scope?
      • this would allow for similar notations in ereal_scope
      • generalization for neg and nnp
      • main machinery in signed.v
      • TODO: Reynald to review
      • TODO: ask Cyril about fix two problems in the application of le_num
    • discuss construction of orderType on signs (c.f., commented Section Order)
      • several ways to build an orderType
      • not really an issue to be addressed now
    • there is also PR 375 about extended reals to be merged after this one
      • not urgent
  • separate boolp and classical_sets (as discussed in https://coq.zulipchat.com/#narrow/stream/237666-math-comp-analysis/topic/boolp)
    • Pierre also has an interest, happy with the implementation as such
    • Reynald: this could make a good replacement for the aging Ensemble
    • TODO: document boolp
    • TODO: separate package, a la mathcomp, let's call it mathcomp-classical
  • progress report about Arzela?
    • merged PR 527
    • we are almost done
    • forward direction is PR 545
      • textbook proofs use compact covers but they do not play nice with filters
      • important pieces of machinery:
        • near_compact_covering is an important lemma to turn a global property into two local properties
          • Cyril: no finiteness condition?
        • sets_of_filters: we have no epsilons but entourages in uniform spaces, could use downwards set as filters
      • Zachary a bit annoyed with the near notation
      • TODO: Zachary to post two issues about technicalities
      • TODO: review the PR
      • Cyril: about equicontinuous, don't take a set for a collection of objects but a family, like trivIset, bigcup, filter_from, etc., because this composes better (coercion from a family of morphisms to a family of arrows)
      • TODO: this is an idiom worth documenting in contributing.md
    • small PR last night
    • TODO: review PR 547
  • plan to merge PR 543 (simplify set_interval.v)
    • which contains PR 371 (Lebesgue measure and integral)
    • to be followed later by PR 541 (displays for measurables)
    • which closes draft PR 492 (functions and cardinality) and closes PR 435 (rat is countable)?
    • but does not close draft PR 83 (WIP: Rewriting countability and finiteness)
      • which contains a missing bit with the compatibility with finiteness
    • TODO: dispatch the lemmas to the right places (in particular, in fsbigop.v), rename csum to esum, put a closes to merge PR 371 in the branch "simplify set_interval.v"
    • TODO(later): replace fset by finite_set in csum/esum
    • TODO: release of 0.4 afterwards
    • Laurent: couldn't functions.v be a separate PR?
      • Cyril: we want Lebesgue anyway, merge without review
      • TODO: after the merge, tag the files functions.v, cardinality.v, csum.v and fsbigop.v for a second round review
  • additions to ereal.v:
  • Do you have generic lemmas about complex that could make their way to real-closed?
    • from PR 1921 (holomorphy)
    • TODO: PR to real-closed
  • complex exponential?
    • rather define it as a power series
    • the set up for the series will be useful
    • theory developed for compact convergence to be useful
    • ask Zachary
  • stalled, input appreciated if any:
  • Marie: drop mathcomp 1.12?
    • let's drop mathcomp 1.12 and support 8.14 and later and mathcomp 1.13 and later
Clone this wiki locally