Stream: math-comp analysis

Topic: landau


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Marie Kerjean (May 29 2020 at 16:03):

thanks.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Marie Kerjean (May 29 2020 at 16:34):

How to reunify o_[] and o_() ?

view this post on Zulip 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

view this post on Zulip 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