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

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

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: Mar 02 2024 at 17:02 UTC