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.
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
)thanks.
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.
Is this what you are looking for https://github.com/math-comp/analysis/blob/master/theories/landau.v#L416-L424 ?
Yes, exactly. Now I can't force eqaddop
to typecheck the filter on which 'o
acts, I'm giving up for now.
How to reunify o_[]
and o_()
?
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
One must use eqaddoE
to replace the fixed witness by the existential one.
Last updated: Feb 05 2023 at 08:28 UTC