2022 11 22 Meeting - math-comp/analysis GitHub Wiki

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