2023 02 06 Meeting - math-comp/analysis GitHub Wiki

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
    • 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