2021 05 27 Meeting - math-comp/analysis GitHub Wiki

Participants: Cyril, Kazuhiko, Marie, Pierre, Reynald, Tafumi, Zachary

PR 311:
- remove fer, keep patch which is more general
  - have a default argument (point in case of pointed types)
- specialize fer from patch
- rename to restrict
- MK: compatibilty with the notion of restriction to a family?
  - ZS: see family at the end of the PR
- CC: several notations for each kind of convergence
  - fct_uniformType default topology for function spaces
  - see restricted_uniformType
  - introduce symbol restricted A(*phantom variable*) := U -> V
  - Definition patch (A : pred U) (f g : U -> V) u : restriced A U V := if_expr (asbool (A u)) (g u) (f u).
- ZS: problem uniform topology does not depend on the domain
PR 318:
- prove that geometric series converge uniformly over Banach Algebra
- Banach Algebra: complete normed algebra with norm (A * B) <= norm A * norm B
- CC:
  - open to change how norm is defined (also MK)
  - does 318 use algebra over the complex numbers? over the reals only? real-valued norm over complex?
- ZS:
  - need real-normed over the complex
  - squeeze theorem only defined over real vector spaces, to generalize
  - there are other such theorems to be generalized
  - need scaling by complex numbers as in 1 - lambda * t
- CC:
  - squeeze could be extended to complex numbers
- MK:
  - wants canonical embedding of the real line in the complex
  - answer by CC: here is an example with the reals and algebraic numbers https://github.com/math-comp/Abel/blob/8d94e23f20c67516d94a1c7028147db2fd1db594/theories/xmathcomp/algR.v#L273
- CC:
  - normed vector spaces with real scalars
  - the value of the norm can be what you like
  - pbm: normed module have the scalar in the same type as the value of the norm that can be R or C
  - solution: introduce an intermediate step to say that the norm is valued in the base field of the base field
    - should wait for HB though
PR 180:
- MK to look at it next week
- move BigmaxrNonneg to nngnum.v
- filter_andb to be packported to MathComp
PR 380:
- use get instead of pselect (exists ...)
- expR instead of exp
- try to generalize to the complex numbers
CC: spectral theories for matrices: https://github.com/math-comp/math-comp/pull/207
PR: about lra for MathComp
- not possible yet because we need support from the Coq side
- no zify layer, this makes it more difficult
- CC: one can just unfold the symbols after instantiating with Rstruct and call lra...
RA: an example of nsatz usage
- grep nsatz in https://github.com/affeldt-aist/coq-robot/blob/master/rot.v
ST: status of sequences.v?
- TODO: task force on power series in R
release 0.3.8 asap
organize meeting by the end of june
- not too close to ITP (to start on June 29)
- around June 18?