-
Notifications
You must be signed in to change notification settings - Fork 43
2021 05 27 Meeting
affeldt-aist edited this page May 27, 2021
·
1 revision
Participants: Cyril, Kazuhiko, Marie, Pierre, Reynald, Tafumi, Zachary
-
PR 311:
- remove
fer
, keeppatch
which is more general- have a default argument (
point
in case of pointed types)
- have a default argument (
- specialize
fer
frompatch
- rename to
restrict
- MK: compatibilty with the notion of restriction to a family?
- ZS: see
family
at the end of the PR
- ZS: see
- 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
- remove
-
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
tonngnum.v
-
filter_andb
to be packported to MathComp
-
PR 380:
- use
get
instead ofpselect (exists ...)
-
expR
instead ofexp
- try to generalize to the complex numbers
- use
- 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 calllra
...
- RA: an example of nsatz usage
- 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?