## Stream: math-comp analysis

### Topic: landau

#### 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

• either binary
• `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))
• or `forall x, E1 =o_(x \near F)` (where `E1` and `E2` may dependent in `x`)
• or ternary
• `E1 = E2 + o_F E3` (same whitespace problem)
• or `forall x, E1 = E2 + o_(x \near F) E3` (where `E1` and `E2` may dependent in `x`)

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: Feb 05 2023 at 08:28 UTC