Skip to content

2025‐02‐20 Meeting

Jump to bottom
affeldt-aist edited this page Feb 21, 2025 · 1 revision

Participants: Cyril, Kazuhiko, Marie, Quentin, Reynald, Takafumi, Yves

  • Question related to Lp spaces:

    • context: we need seminorms for Lp spaces:
    • question: should we extract setoid stuff and ess_sup related lemmas from Lp spaces?
      • everything does not need to wait for the next MathComp release!

  • About Splitting ssrnum and adding ordered zmodules on MathComp:

    • the plan is to split in:
      1. ssrnum. in several files with the namespaces preserved TODO: must be an independent MathComp PR (for 2.4.0)
      2. integrate interval_inference.v
        • include integratation of extended numfields (and then generalize to zmod)
        • will subsume MathComp-Analysis' extended reals TODO: can be an independent MathComp PR already (for 2.4.0)
      3. we want extended norms (with +oo as a value possible) (to have Minkowski w.o. integrability conditions and Lp spaces where the norm is finite) NB: might be difficult to achieve for MathComp 2.4.0
    • btw, what are exactly the axioms for seminorms?
      • what will become of -oo?
      • it is a matter of convention rather than a mathematical question
      • is -oo for non-measurable functions?
      • marie: for non-measurable functions, 0 would be weird, rather +oo for compat. with metric spaces
    • setoid_rewrite in MathComp-analysis (cyril: yes, quentin: no)
      • we do have ssr patterns for setoid rewrite
      • setoid_rewrite has no ssr patterns, it rewrites under binding providing the right morphisms (like under where the morphism is explicit)

  • Collecting ideas to split files:

    • Note that lebesgue_measure.v has been split recently
    • issue about lebesgue_integral.v
      • take out simple functions
      • put Rintegral aside
        • btw, we want Bochner integral instead, Rintegral is temporary
        • question: no Lebesgue-Stieltjes integral? needed for differential forms?
        • do we need euclidian spaces for Bochner? no (cyril)
        • use vector.v for euclidian spaces? yes (cyril)
        • cyril: we should be able to apply bocher to euclidian spaces
          • is the vector type a Banach space now?
      • should we have a file for Fubini? -> maybe
      • TODO: have a subdir with a metafile like topology.v
    • issue by marie about normedmodtype.v:
As far as I can see, I see five parts in this file, not well ordered:
1. PseudoMetricNormedZmodules depending on numDomains
2. PseudoMetricNormedZmod depending on numFieldType
3. NormedModules depending on numDomains
4. NormModules depending on numFieldTypes
5. Theorems about realFied, in the last sections.

In particular, some lemmas about PseudoMetricNormedZmod depending on
numFieldType (as add_continuous) are proved quite late, after the
introduction of NormedModules.

I am not sure yet normedmodtype.v can be separated in 5 files,
happy to discuss a better way to split it.

  • Discussion about "Collecting ideas to split files":

    • tvs appear between 2. and 3.
    • cyril knows how to reshuffle the file to solve marie's problem
    • cyril: pseudometriczmodtype needs to be better isolated
    • TODO for normedtype.v:
      • first we split
            1. can be separated but this is really to have smaller files
        • TODO: topological groups (with continuous addition) before 1. and 2.
          • question: order structure (in 1.)? no order structure in normedtype.v, numDomainType is for the distance
          • thinking of Haar measures? other applications?
      • second we reshuffle
      • question: tvs does depend on pseudometric? is that a mistake?
      • NB: cyril thinking of splitting normedtype.v after numext.v, won't happen before the end of march, marie might look at it before

  • Issue triaging:

    • about the %E notation scope
      • cyril: don't understand yet where it is comming from...
      • TODO: urgent
      • sakaguchi: did you try Print Visibility? there might be some Open Scope without Local somewhere, Print Visibility to debug this comment
    • about the naming of eq_exists2
      • eqrel_exists or eq2_exists

  • Observation (not discussed):

    • Many Warning: HB: no new instance is generated are generated at compilation time

  • Questions:

    • about notations for derivation
    • about interior notation
      • TODO: let's try to remove the hat
    • about naming:
      • cvgeMl/cvgeMr
        • M should be Z
        • cvgMl should be cvgZr
      • oppr/oppl, here is what we said in the previous meeting:
        • qualifying suffix only on the subject, thus it should be oppr_continuous
        • oppe_continuous is correct
    • about mathematical structures
      • close (old) issue 154 ?
        • not discussed
      • what we said about this issue in 2021:
    probably not done, we addressed for arbitrary numFieldTypes, we might need to several instantiations for the real closure
    TODO: Marie to push cauchetoile.v

  - not discussed either
  • PR triaging:
    • Upcoming consequences of Potentially zero rings on mathcomp analysis
      • so that functions are a ring at least
      • potentially issue to generalize polynomials
      • Sakaguchi observes LAlgType can be generalized
    • short PR: fiberwise
      • maybe we don't need it
      • statement larger than the proof
      • relation to finite_preimage? to generalize it?
      • TODO: try generalization, maybe close and do it another way
    • short PR: adapt to mc#1256
      • sakaguchi san can review PR 1256 next month
      • the one on MathComp-Analysis' side can be closed
    • put a milestone to https://github.com/math-comp/analysis/pull/337 ?
      • Sakaguchi will maybe not refactor
    • put a milestone to https://github.com/math-comp/analysis/pull/1399 ?
      • alessandro: no use right now, for multi-dimensional mean estimation
      • no rush, wait to see if it is really useful
    • close PR 1010?
      • not discussed for cyril had left the meeting by this time
Clone this wiki locally