2024 02 09 Meeting - math-comp/analysis GitHub Wiki

Participants: Reynald, Quentin, Takafumi, Alessandro, Pierre, Zachary

  • Announcements:

    • Mathcomp-Analysis 0.7.0 has been released
      • btw, any clue about issue #1169 ?
      • 0.7.0 seems to be not compatible with HB 1.6.0/Coq 8.17.1
        • how did this escape our testings?
        • might be broken with 1.6.0
      • TODO(rei): try HB 1.6.0 with Coq 8.19.0 to confirm
    • MathComp-Analysis 1.0.0 has been released
    • feedback is welcome

  • issue triaging:

    • about exports and contra.v issue #1157
      • Pierre wanted to remove canonicals to avoid us failing to add new ones when needed
      • Pierre failed to use contra and didn't open the PR
      • Quentin: Zorn to be PRed has a use-case
        • it is a more general version that the already available one
        • no problem if it is a duplicate for now because we will surely come back to it
      • follow-up by Pierre just after the meeting: https://github.com/math-comp/analysis/pull/1172
    • about the infamous monotonous issue #1133
      • monotonic in US English
      • monotonic with mono is strict
        • pbms: this is contrary to Zachary's intuition, the constant function is not monotonic
        • => the definition should be homo
        • in some cases only should we need mono
      • homo would be large according to wikipedia
      • TODO: Reynald to try a PR
      • move nondecreasing*, etc. in realfun.v earlier in the hierarchy of files
      • introduce nondecreasing_on, nonincreasing_on, etc.
        • see also order_morphism and le_mono in order.v
    • progress on issue #1126 ?
      • Takafumi in charge
      • idea: use https://mathscinet.ams.org/msnhtml/msc2020.pdf
        • list the library of MathComp with links to the classification (next to the opam packages)
        • TODO: PR to put them at the top of the headers?
        • opam info should also display this information
    • time to address the simplification of the filter layer from the long-standing issues?

  • PR triaging:

    • splitting topology.v PR #1166
      • does it call for version 1.1.0?
      • yes because it is a breaking change (new file and removal the canonical topology on functions)
    • mulr_rev PR #1122
      • already discussed during the last meeting
      • failed to figure out how to take advantage of R^c from MathComp
        • i.e., couldn't get rid of the identifier mulr_rev in favor of GRing.mul R^c
      • TODO(rei): try again with MathComp 2 and then discuss it again
      • Pierre: ask Kazuhiko because it looks like the dual order experiment
    • report on issue #965
      • recently merged: total_variation PR #1118
      • to be merged: LDT PR #1065
        • Reynald asking for external input
        • in particular, is it ok to use locally_integrable, integrable w.r.t. setT and not care about generic versions?
        • Zachary: yes for lemmas about integrability since we can always recast by multiplying with a characteristic function
        • e.g.: FTC1 : patchable by multiplying f by a characteristic function
        • same for locally_integrable
        • for continuity it matters more

  • Questions from issues:

    • sigma_finiteP issue #1080
      • prove the reverse direction and then the suffix will make sense!
    • expRMm issue #1094
      • M is multiplication
      • should it be n? maybe just a typo?
      • TODO: ask Laurent
    • about patch issue #1100
      • Zachary: it depends on the lemma, this is case by case
      • in a textbook specialized for the real it would be the same
      • but patch is bit more general
      • to prove a bound `patchP might be nicer
    • + vs. \+ issue #1077
      • the first one is useful to write from right to left
      • the second one looks more generic
      • TODO: Alessandro will try again
      • looking like caddE for charges that we got rid of (but here the proof is less trivial)

  • Zachary: why do we need pointed on topology?