2021 01 26 Meeting

Participants: Marie, Kazuhiko, Cyril, Reynald

• About PR https://github.com/math-comp/analysis/pull/205
  • hiearchy used to start at numDomainType, now starts at numFieldType
    • using "non-forgetful inheritance"
    • no more ^o in sequences.v
    • one ^o left related to nbhs' because it uses numDomainType (should go away with numFieldType)
  • TODO: git reset --hard with fork by Sakaguchi https://github.com/pi8027/analysis/tree/numfield_topology
  • TODO: normedtype.v:886 https://github.com/pi8027/analysis/blob/0b19ca11e48c44f77a6d46c36e0bd0853dfb006f/theories/normedtype.v#L886 Module nonforgetful_inheritance ill-named (shouldn't reveal internals) Introduce a "numFieldTopology" module
• About PR https://github.com/math-comp/analysis/pull/183
  • TODO: use field inverse instead of ring inverse, look at where unitfE is used (normrV -> normfV, mulrV, ...)
  • Shouldn't bounded_funP use a near notation?
  • TODO: try to get rid of exists's in favor of near
    • except when nbhs_ex is used
• About PR https://github.com/math-comp/analysis/pull/204
  • experiment on defining the same topology on difference vector spaces
  • TODO: sync with zstone1 contributions
• About Issue https://github.com/math-comp/analysis/issues/301
  • DONE: write a comment to point to PR #283 and close
• About the next release:
  • release 0.3.6 by the end of the month, possibly with PR #205 and PR #183
• About measure theory:
  • TODO: spurious pselect before {subset _ <= _}
  • problem with the definition of finite sets of intervals as a ring of sets
    • problem 1: R is not a Type but a realType, the head symbol if Real.sort
    • problem 2: by completion, we'll get a new measurable type on R, itvs_ringOfSets should therefore be a local instance, should go into a module (then close the module and redefine the measure on R as the one given by caratheodory_measurableType)
  • NB: can't replace the Definition itvs_ringOfSets_carrier in Prop by, say, an inductive in Type
  • flow:
    1. l.525, Canonical canonical_outer_measure OuterMeasure.OuterMeasure should not appear, rename the constructor OuterMeasure as Axioms or Build (l.716, measure.v)
    2. l.265, Definition caratheodory_measurableType builds a measure from an outer measure l.292, HB.instance Definition instance is global on measurables mu (not on R)
    3. in section Hahn, Let M : measurableType := caratheodory_measurableType mstar. should become Let M : measurableType := [measurableType of measurables (mu_ext mu)]. but since we do not have yet the notation [measurableType of ...] (and also because mu_ext mu is not of the right type(?)) it will become Let M : measurableType := [the measurableType of measurables [outer_measure of mu_ext mu]]. NB: [measurableType of ...] available as a feature of hb.1.0.0 Still, we should strive for Let M : measurableType := [measurableType of {measurables (mu_ext mu)}]. for documentation purposes l.734, Let Hahn_mu [outer_measure of mstar] should work
    4. HB.instance Definition itvs_ringOfSets in a module (an alternative could have been to introduce an alias, say, itvs_measurables_of_R but anyway this is supposed to be internal) length might require typing information
  • memo: Definition gen_measurable is a copy of U on which we have a structure of measurableType
  • memo: l.313, Canonical caratheodory_measure, might become a problem
• TODO: create an issue about floor and ceil to remember to replace the code when the hierarchy in MathComp is refined
• About inf sums:
  • PYS reports progress but still needs a few weeks