2023 02 06 Meeting

Participants: Reynald, Zachary, Pierre, Takafumi

• merge PR 832 on doc of finSubCover ?
  • equality is too restrictive
• What to do about casts in patterns? PR 804
  • This PR has been closed by the author
  • warnings were scheduled to be errors but this has changed
    • see Coq PR 16798
  • TODO: test if the casts are effective
• release 0.6.1
  • no docker for MathComp 1.16 yet, Pierre to meet Erik in a few hours
• merge PR 786 on quotient topology
  • TODO(ZS): rebase and merge
  • TODO: generic quotient to define Lp spaces in the probability PR Advantages:
    1. Hausdorff spaces are preserved
    2. We retain the norm structure
• review of PR 516 on probability
  • TODO(RA/TS): use generic quotient to define Lp space module ae_eq
  • the properties about discrete random variables require indexing and we seem to lack generic infrastructure to deal with them
  • TODO(RA/TS): notations for random variables should not be necessary, instead show that random variables form a comUnitAlgebra over R to use its notations
    • TS referring to notation problems when producing a ring of functions
    • ZS recommends to locally define notation and build the canonical structure
    • TODO on Thursday
• merge PR 768 on Product embedding
  • every compact space is embeddable in a product, we'd like to build this embedding and show that it is continuous
  • joint_product : T -> product_topologicalType U_ which is continuous, open, injective
• PR 763
  • countable_uniformity = metrizability
  • the sup uniform space of metrizable uniform spaces is metrizable
  • topology.v:4265: supremum of uniform spaces is uniform
  • Problem: the definition of the supremum entourage is not human friendly because of dependent pairs. need to keep track on which space the entourage comes from
  • TODO(RA): review, goal: look for some local improvements and merge
• PR 833
  • mark these lemmas as deprecated might be good bu undeprecated deprecated might be awkward
  • TODO(RA): show that these lemmas can indeed be superseded by the new theory
• PR 794
  • current theorems do not apply to the characteristic function which is not differentiable at the endpoints
  • for reference see realfun.v, more precisely https://github.com/math-comp/analysis/pull/752
    • continuous within some subspace is ad-hoc in the sense that the notation is ad-hoc
    • first step: differentiable within a subspace (solution 3.)
    • condition for acceptance: make a claim that the characteristic function is convex
• PR 777 on Hahn decomposition
  • could be mergeable
    • relies on PR 836 which introduce a type for finite measures but is incomplete
    • maybe need to split mixins and show that they compose
• PR 818 on Radon-Nikodym
  • current version augment measure_ge0 with a measurability hypothesis that shouldn't be necessary in principle
  • TODO(RA): investigate and report
• TS: thinking about absolute convergence
  • relation with the summable predicate
  • ZS: foresees applications of the Ascali theorem to prove theory of power series