Hi, I'm interested to experiment with mathcomp.analysis' formalization of landau notations,

but https://github.com/math-comp/analysis/blob/master/theories/landau.v does not seem to have dedicated lemmas about the \oo filter;

so I tried composing with the injection from nat to R to overcome this, but I was stuck as well.

Here is a minimal (non)working example (using FTR, `coq-mathcomp-analysis.0.5.3`

and `coq-mathcomp-ssreflect.1.15.0`

and `coq.8.16.1`

):

```
From mathcomp Require Import all_ssreflect ssralg ssrnum.
From mathcomp.analysis Require Import boolp classical_sets functions.
From mathcomp.analysis Require Import mathcomp_extra.
From mathcomp.analysis Require Import ereal reals signed topology normedtype prodnormedzmodule landau sequences.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section test.
Variable R : realFieldType.
Definition f n := (2 * n)%:R : R.
Definition g n := n%:R : R.
Fail Lemma test : f =O_[filter of \oo] g.
(* The command has indeed failed with message: *)
(* In environment *)
(* R : realFieldType *)
(* The term "f" has type "forall _ : nat, Num.RealField.sort R" *)
(* while it is expected to have type *)
(* "forall _ : nat, *)
(* @NormedModule.sort (Num.NumField.numDomainType ?K) *)
(* (Phant (Num.NumField.sort ?K)) ?V". *)
End test.
```

Would you have suggestions?

Cc @Cyril Cohen @Reynald Affeldt

Ah yes, we should really document that... You need to add

```
Import numFieldTopology.Exports.
```

If you want to work with an abstract `realFieldType`

... this puts the trivial normed module canonical instance on it.

Ah OK, thanks for the tip!

And BTW, what would be the alternative, more standard way to deal with O(u(n))?

Embed nats in `R`

from `Require Import Reals`

, right?

what do you mean by "more standard" ?

Hi! I just mean, without the constraint that you mentioned "If you want to work with an abstract realFieldType".

Last updated: Jun 25 2024 at 19:01 UTC