2023 07 27 Meeting - math-comp/analysis GitHub Wiki

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