2022 11 22 Meeting

Participants: Cyril, Pierre, Reynald, Yves, Zachary

• PR triaging:

  • second countable, clopen PR 797
    • local_base: the neighborhood is equal to the filter_from of B
    • topological_base: there is an alternative definition
    • maybe this could be merged as it is with the current definition
      • even keep the definition and add the other definitions with lemmas for the equivalence
    • what about the idiom cid (iffLR (exists2P _ _) (h n))?
      • put a name for all these idioms is not reasonable
      • TODO: maybe put this somewhere in the wiki
      • TODO: try to use sigW (one layer of abstraction on top of cid) instead of cid (the axiom)
  • Product embedding PR 768
    • question about displays for the open predicate (see https://github.com/zstone1/analysis/pull/2/commits/0e639029ceb6ce6a6bcdf7cafd05f55c577c47a7)
      • see l.6728: @open weakT? add a notation to print @open weakT as weak_open
    • same for supremum, with a local notation ("print only" notations)
      • just notations for this PR, no displays
      • wait for a tool might be the best solution but for topology we maybe cannot wait
      • putting displays would be needed for topologies only, no need to add displays for normed spaces and higher in the hiearchy
  • integral of constant and generalization of le_integral_abse PR 781
    • TODO: expose both lemmas
      • rename the second, more general lemma with comp_abse
      • put Cyril as a reviewer

• Easy PRs:

  • naming, following discussion of an issue, PR 767
    • TODO: avoid (d : _) by replacing Variables with Context
  • add a lemma to classical_sets.v PR 791
    • TODO: merge
  • fix generated sigma-algebras of extended real numbers PR 793
    • collision of naming with when there are two notions of infinity
    • notation is not correct for lattices with a bottom and a top
    • don't know of a good fix yet
      • forbid interval with infty bounds using a trick similar to nonProp, a type that can only be instantiated by something which is not proposition: https://github.com/coq/coq/blob/master/theories/ssr/ssreflect.v#L30-L34
    • see also issue 795
  • fix deprecated declarations PR 798
    • we need to make the proxies...
    • this should be fixed at the the Coq level
      • send to the Coq call?

• RFC:

  • in a previous meeting [2022-02-24] we concluded that the complex exponential is better defined as a power series PR 770 does so and prove exp x%:C = (expR x)%:C it requires undesirable type constraints (: complex_ringType _) how to tackle expD?
    • TODO: Cyril to look at it

• TODO: release of MathComp-Analysis 0.6

  • milestone
  • add PR 799 to the milestone
    • Cyril was about to introduce something similar to product_embed to MathComp as a forthcoming PR
    • TODO: Zachary to rename (projection to proj) and move code in mathcomp_extra.v
      • may need to re-alias in topology.v

• rebase of the HB branch in progress

  • before this rebase, we were at product_topologicalType

• project of re-licensing to MIT following MathComp? (see https://github.com/math-comp/math-comp/wiki/Minutes-October-5-2022)

• short progress report about measure theory