Marie Kerjean (May 29 2020 at 15:49): Marie Kerjean (May 29 2020 at 15:49):What is the difference between [o_[filter of 0] id of ?s] and 'o_[filter of locally 0] id ? I'm trying to prove an expression using the second one while having an expression using the first at hand here.
Cyril Cohen (May 29 2020 at 15:57):f (c + h) = f c + h * 'D_1 f c +
(('o_ (0 : [filteredType C^o of C^o]) id ) : _
is a wrongly stated.
The four only right ways to state a Bachmann - Landau statement are using the
E1 =o_F E2 (with a whitespace between (o_ and F if F starts with a parenthesis (this is a parser problem I wish to get rid of))forall x, E1 =o_(x \near F) (where E1 and E2 may dependent in x)E1 = E2 + o_F E3 (same whitespace problem)forall x, E1 = E2 + o_(x \near F) E3 (where E1 and E2 may dependent in x) Marie Kerjean (May 29 2020 at 16:03):thanks.
Marie Kerjean (May 29 2020 at 16:07):Is there a lemma stating the equivalence between o and its definition with a function converging to zero ? I would need to use the machinary of derive.v but unification in landau notations is quite complex.
Cyril Cohen (May 29 2020 at 16:12):Is this what you are looking for https://github.com/math-comp/analysis/blob/master/theories/landau.v#L416-L424 ?
Marie Kerjean (May 29 2020 at 16:26):Yes, exactly. Now I can't force eqaddop to typecheck the filter on which 'o acts, I'm giving up for now.
Marie Kerjean (May 29 2020 at 16:34):How to reunify o_[] and o_() ?
Cyril Cohen (Jun 17 2020 at 09:47):Cyril Cohen said:
f (c + h) = f c + h * 'D_1 f c + (('o_ (0 : [filteredType C^o of C^o]) id ) : _is a wrongly stated. [...]
https://hal.inria.fr/hal-01719918v3
Definition 4.2.1
Cyril Cohen (Jun 17 2020 at 09:57):One must use eqaddoE to replace the fixed witness by the existential one.
Last updated: Aug 11 2022 at 03:02 UTC