Stream: math-comp analysis

Topic: can we express bigO claims for n-->\oo ?


view this post on Zulip Erik Martin-Dorel (May 26 2023 at 14:35):

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

view this post on Zulip Cyril Cohen (May 26 2023 at 14:38):

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.

view this post on Zulip Erik Martin-Dorel (May 26 2023 at 16:39):

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?

view this post on Zulip Cyril Cohen (May 29 2023 at 13:44):

what do you mean by "more standard" ?

view this post on Zulip Erik Martin-Dorel (May 29 2023 at 16:00):

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