Skip to content

2024 10 10 Meeting

Jump to bottom
affeldt-aist edited this page Oct 11, 2024 · 1 revision

Participants: Alessandro, Cyril, Marie, Pierre, Reynald, Takafumi, Zachary

  • splitting of normedmodule.v (issue 1339, on zulip also)

    • technical lemmas about pseudometric spaces are too late in the file
      • this causes problems for the TVS PR
    • one file per structure of interest?
    • Marie to open a channel on zulip to split the file
    • Reynald: I would advocate for an incremental split that spans at least one release like we did for topology.v because there was unexpected (minor) problems (with the CI) and because the smaller eviews proved useful to fix and improve the doc (and also for the changelog)
    • Zachary: Urysohn and uniform separator do not belong here (IDEA #1)
    • Cyril: change the organization of the repo?
      • too many structures in the same file, too many instances in the same file
      • one mixin per file? instances in another file? what are the consequences? look at mathlib?
      • e.g., one file for topology makes sense
      • original reason for having huge files: do not fragment modules
      • potential issue: some factories rely on instances
    • Zachary: most instances can be split out, in general splitting might not scale
    • Cyril:
      • one file for a dedicated structure when it makes sense, one file for family of instances
      • orphan instance problem (instance defined neither with the structure nor with the theory)
        • a problem in Haskell
        • counter measure: split the file but reimport (and export) in one main file
    • Zachary: problems with importing too much? (besides notations)
      • Cyril: inefficiency? problem with user importing "subfiles" only
    • Zachary: stuff specific to real numbers could be separated out (IDEA #2)
    • Plan?
      1. extract Uryshon and friends
      2. rearrange so that lemmas about pseudometric spaces are not too late in the file
      3. do a first split

  • about the splitting of topology.v (issue 1167)

  • splitting lebesgue_measure.v

    • issue 1315
    • the Lebesgue measure appears in the middle of the file, the first half is rather about measurable functions over the real numbers or the extended real numbers
    • TODO(reynald): create measurable_realfun.v with what is not Lebesgue measure

  • create issues for the following topics?

    • coq-mathcomp-real package (discussed during https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
      • with signed.v, constructive_ereal.v, reals.v, Rstruct.v, real_interval.v
        • Zachary: real_interval.v partly depends on normedtype.v!
      • Reynald: it might be good to have a version of the packager of MathComp for MathComp-Analysis

  • changing the convention in convex.v to fit Infotheo (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)

    • the sooner the better
    • related to issue 860
    • Takafumi:
      • this is wip
      • problem finding good names for the many associativity lemmas
      • let's PR and ask for input!

  • PR triaging:

    • PR 1300 on topological vector spaces

      • should it be reviewed and merged as is (just the addition of a structure) or should we wait for more theorems to be included ?
      • one admit left (NB: proved on the next day)
      • this PR adds a structure right now, not theory yet
      • maybe undraft next week
      • Zachary: dual space to extend integrals beyond reals such as the Bochner integral
      • Marie:
        • weak-* topology
        • basic objects to be pairs as mathematicians think of it
      • Zachary willing to review

    • PR 1340 on continuous functions

      • pointed no longer required by a topology
      • using set_type from set to types (coercion in classical_sets.v)
      • we can now add a topology to things that are more than functions
      • subspace topology has been useful, we also need subtype topology,
      • conversion between subspace and subtype (which comes from the set_type construct)
      • ready to be reviewed
      • TODO(marie): review maybe by next week

    • PR 912 on probabilistic programming languages

      • this PR relies on lra and the CI fails because of that, what can we do? (very soon we will start using lra in master probably)
      • lra is expected to work with inequality, one needs to add extra facts to the context
      • it is just a matter of fixing nix
      • Kazuhiko: lra is still experimental!
      • Takafumi: in which way experimental?
        • not used enough, not enough resource for maintenance
      • Alessandro: how huge the effort to fix lra?
        • needs a bit of knowledge about internals
        • adding a structure in mathcomp could break it
      • TODO:
        • update the package with nix
        • add an overlay (we can do that online (with Pierre) just not right now)
        • NB: Pierre suggested this commit after the meeting but need to investigate more

  • issue triaging:

    • naming issues:
      • issue 1269 (naming of set_mem))
        • TODO: try to change it as a view, named set_memP
      • issue 1292 (about the opp prefix/suffix)
        • nobody knows whether we should use opp or oppr
        • relation with continuousN?
          • this is for the use of opp individually, when composed with a function f, we use a prefix
          • TODO: ask online
    • questions:
      • shall we close issue 759 now that relations have found a place in classical_sets.v?
        • Zachary: let's close and build the theory latter
      • issue 1268 (about at_point and principal_filter)
        • remove one for the other, which one do you keep?
        • principal_filter
        • TODO(rei): do a PR that remove at_point
      • issue 1077 (about measure_addE)
        • the functional version has more issues
        • Zachary: now using more functional equality for the interaction between neighbohoods, entourages, etc. but this is contaminating and sometimes need to be reverted
        • Takafumi: naming convention to keep both?
        • Zachary: what functions with multiple arguments? several lemmas for them?
        • Reynald: E1 for suffix for extensionnality with only one argument?
        • to be continued
    • issue 271 (about landau and Banach-Steinhaus)
      • can be closed
    • issue 1320 (near message error)
      • (not discussed, too late)

  • PRs for which reviews have more or less started (feel free to jump in):

    • PR 1256 on the {mfun _ >-> _} type for measurable functions
    • PR 1331 on completely regular spaces
Clone this wiki locally