2023 07 27 Meeting

Participants: Reynald, Cyril, Pierre, Zachary, Takafumi

• naming convention for bigcup:
  • see comment https://github.com/math-comp/analysis/issues/988#issuecomment-1651515771
  • see also bigcup_set0 vs. bigcup0
  • \bigcup_(x in ~` P) F x, we write bigcup_setC
    • in general, in bigcup_xyz, xyz is about the in part
    • \bigcup_(A in P) ~` F A, we make a longer name, we may write something like bigcup_setCr
      • instead of, e.g., bigcupP_setC
      • also, try to swap the equality as in, e.g., setC_bigcup
• Discussion about the pending issues about renaming
  • do not rename ball to open_ball because balls are not necessarily open
  • we actually need a stronger notion of pseudometric space where there is a distance between any two points
  • more generally, there is a bunch of renaming about closed balls
  • TODO: we should have a notion of open balls
  • about scale_cball from the PR on Vitali's lemma:
    • introduce a predicate is_ball so that we the predicate is satisfied we have have a center and a radius function
    • or introduce a ball record with a coercion to a set?
    • anyway, we'd like to unify the various notions of balls
    • we should be aiming for scale_ball to be a function from balls to balls
• https://github.com/math-comp/analysis/pull/973 (Vitali's lemma)
  • change the lemma from B : I -> R * {posnum R} to two functions I -> R and I -> {posnum R}?
    • at least try not to expose the scale_cball by introducing alternative statements
  • as of now, many lemmas could be generalize to dimension n but they are still in dimention 1
• news about perf of HB branch: thanks to latest elpi (1.17.0) and master branches of coq-elpi and HB:
  • total analysis: 26:31 (used to be 40 min) (2.6 GB (used to be 10 GB))
  • loading elpi code (HB): 02:59 (used to be 16 min)
  • running elpi code (HB): 08:55
  • not all elpi code is released so MathComp-Analysis 1 can maybe wait a bit
• PR triaging:
  • merge https://github.com/math-comp/analysis/pull/985 ?
    • can be merged
    • putting the N <= i cond in the hypo or not? (maybe not)
  • merge https://github.com/math-comp/analysis/pull/971 ?
    • Cyril: isn't 1/3 automatically a posnum?
      • division by 2 gets thing automatically inferred by not division by 3 (!)
      • TODO: Pierre to investigate
        • work around: replace 3 with 3%:R
      • TODO: make the 1/3 disappear before merge if possible
    • NB: we can use lra for mathcomp-analysis from now
      • TOD0: add the dependency to algebra tactics
  • https://github.com/math-comp/analysis/pull/973
    • pending question about where to put lemmas about centered intervals
      • they appear in Lebesgue's differentiation theorem for continuous functions
      • we might need a more general approach to represent balls (see the discussion above)
      • we will hit the problem quickly when moving to higher dimensions anywau
  • https://github.com/math-comp/analysis/pull/984 (Vitali's theorem)
    • TODO: Zachary to review
  • https://github.com/math-comp/analysis/pull/995 (Hardy-Littlewood)
    • TODO: Zachary to get rid of the the boundeness hypo in the inner regular lemma
  • differentiation theorem is around the corner
    • for the easiest approach using Radon-Nikodym we need absolute continuity for functions (this should be the last piece)
    • Zachary spotted an appropriate proof on stack overflow
    • Takafumi: we might also need bounded variation
  • https://github.com/math-comp/analysis/pull/900 (Urysohn's Lemma)
    • TODO: Zachary to update following Cyril's comment
    • goal: merge it in the next days (as well as Tietze)
    • relies on a technical proof (see step_ball, Step 1, Step 2, Step 3 in topology.v)
    • uniform spaces with countable basis:
      • ref: https://krex.k-state.edu/bitstream/handle/2097/23276/LD2668R41963L638.pdf?sequence=1