Library mathcomp.analysis.landau

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
Require Import ereal reals signed topology normedtype prodnormedzmodule.

BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O F is a filter, K is an absRingType and V W X Y Z are normed spaces over K alternatively, K can be equal to the reals R (from the standard library for now) This library is very asymmetric, in multiple respects:

most rewrite rules can only be rewritten from left to right. e.g. an equation 'o_F f = 'O_G g can be used only from LEFT TO RIGHT
conversely most small 'o_F f in your goal are very specific, only 'a_F f is mutable
most notations are either parse only or print only. Indeed all the 'O_F notations contain a function which is NOT displayed. This might be confusing as sometimes you might get 'O_F g = 'O_F g and not be able to solve by reflexivity.
- In order to have a look at the hidden function, rewrite showo.
- Do not use showo during a normal proof.
- All theorems should be stated so that when an impossible reflexivity is encountered, it is of the form 'O_F g = 'O_F g so that you know you should use eqOE in order to generalize your 'O_F g to an arbitrary 'O_F g

To prove that f is a bigO of g near F, you should go back to filter reasoning only as a last resort. To do so, use the view eqOP. Similarly, you can use eqaddOP to prove that f is equal to g plus a bigO of e near F using filter reasoning. Parsable notations: [bigO of f] == recovers the canonical structure of big-o of f expands to itself f =O_F h == f is a bigO of h near F, this is the preferred way for statements. expands to the equation (f = 'O_F h) rewrite from LEFT to RIGHT only f = g +O_F h == f is equal to g plus a bigO near F, this is the preferred way for statements. expands to the equation (f = g + 'O_F h) rewrite from LEFT to RIGHT only /!\ When you have to prove (f =O_F h) or (f = g +O_F h). you must (apply: eqOE) as soon as possible in a proof in order to turn it into 'a_O_F f with a shelved content /!\ under rare circumstances, a hint may do that for you [O_F h of f] == returns a function with a bigO canonical structure provably equal to f if f is indeed a bigO of h provably equal to 0 otherwise expands to ('O_F h) 'O_F == pattern to match a bigO with a specific F 'O == pattern to match a bigO with a generic F f x =O_(x \near F) e x == alternative way of stating f =O_F e (provably equal using the lemma eqOEx Printing only notations: {O_F f} == the type of functions that are a bigO of f near F 'a_O_F f == an existential bigO, must come from (apply: eqOE) 'O_F f == a generic bigO, with a function you should not rely on, but there is no way you can use eqOE on it. The former works exactly the same by with littleo instead of bigO. Asymptotic equivalence: f ~_ F g == function f is asymptotically equivalent to function g for filter F, i.e., f = g +o_ F g f ~~_ F g == f == g +o_ F g (i.e., as a boolean relation) --> asymptotic equivalence proved to be an equivalence relation Big-Omega and big-Theta notations on the model of bigO and littleo: {Omega_F f} == the type of functions that are a big Omega of f near F [bigOmega of f] == recovers the canonical structure of big-Omega of f [Omega_F e of f] == returns a function with a bigOmega canonical structure provably equal to f if f is indeed a bigOmega of e or e otherwise f \is 'Omega_F(e) == f : T -> V is a bigOmega of e : T -> W near F f =Omega_F h == f : T -> V is a bigOmega of h : T -> V near F --> lemmas: relation with big-O, transitivity, product of functions, etc. Similar notations available for big-Theta. --> lemmas: relations with big-O and big-Omega, reflexivity, symmetry, transitivity, product of functions, etc. WARNING: The piece of syntax "=O_(" is only valid in the syntax "=O_(x \near F)", not in the syntax "=O_(x : U)".

Set Implicit Arguments.

Declare Scope R_scope.

Import Order.TTheory GRing.Theory Num.Theory.

Reserved Notation "{o_ F f }" (at level 0, F at level 0, format "{o_ F f }").
Reserved Notation "[littleo 'of' f 'for' fT ]" (at level 0, f at level 0,
format "[littleo 'of' f 'for' fT ]").
Reserved Notation "[littleo 'of' f ]" (at level 0, f at level 0,
format "[littleo 'of' f ]").

Reserved Notation "'o_ x" (at level 200, x at level 0, only parsing).
Reserved Notation "'o" (at level 200, only parsing).

Parsing

Reserved Notation "[o_ x e 'of' f ]" (at level 0, x, e at level 0, only parsing).

Printing

Reserved Notation "[o '_' x e 'of' f ]"
(at level 0, x, e at level 0, format "[o '_' x e 'of' f ]").

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Reserved Notation "''o_' x e "
  (at level 0, x, e at level 0, format "''o_' x e ").
Reserved Notation "''a_o_' x e "
  (at level 0, x, e at level 0, format "''a_o_' x e ").
Reserved Notation "''o' '_' x"
  (at level 0, x at level 0, format "''o' '_' x").

Reserved Notation "f = g '+o_' F h"
  (at level 70, no associativity,
   g at next level, F at level 0, h at next level,
   format "f = g '+o_' F h").
Reserved Notation "f '=o_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '=o_' F h").
Reserved Notation "f == g '+o_' F h"
  (at level 70, no associativity,
   g at next level, F at level 0, h at next level,
   format "f == g '+o_' F h").
Reserved Notation "f '==o_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '==o_' F h").

Reserved Notation "[o_( x \near F ) ex 'of' fx ]"
  (at level 0, x, ex at level 0, only parsing).

Printing

Reserved Notation "[o '_(' x \near F ')' ex 'of' fx ]"
(at level 0, x, ex at level 0,
format "[o '_(' x \near F ')' ex 'of' fx ]").

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Reserved Notation "''o_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''o_(' x \near F ')' ex").
Reserved Notation "''a_o_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''a_o_(' x \near F ')' ex").
Reserved Notation "''o' '_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''o' '_(' x \near F ')' ex").

Reserved Notation "fx = gx '+o_(' x \near F ')' hx"
  (at level 70, no associativity,
   gx at next level, F at level 0, hx at next level,
   format "fx = gx '+o_(' x \near F ')' hx").
Reserved Notation "fx '=o_(' x \near F ')' hx"
  (at level 70, no associativity,
   F at level 0, hx at next level,
   format "fx '=o_(' x \near F ')' hx").
Reserved Notation "fx == gx '+o_(' x \near F ')' hx"
  (at level 70, no associativity,
   gx at next level, F at level 0, hx at next level,
   format "fx == gx '+o_(' x \near F ')' hx").
Reserved Notation "fx '==o_(' x \near F ')' hx"
  (at level 70, no associativity,
   F at level 0, hx at next level,
   format "fx '==o_(' x \near F ')' hx").

Reserved Notation "{O_ F f }" (at level 0, F at level 0, format "{O_ F f }").
Reserved Notation "[bigO 'of' f 'for' fT ]" (at level 0, f at level 0,
  format "[bigO 'of' f 'for' fT ]").
Reserved Notation "[bigO 'of' f ]" (at level 0, f at level 0,
  format "[bigO 'of' f ]").

Reserved Notation "'O_ x" (at level 200, x at level 0, only parsing).
Reserved Notation "'O" (at level 200, only parsing).

Parsing

Reserved Notation "[O_ x e 'of' f ]" (at level 0, x, e at level 0, only parsing).

Printing

Reserved Notation "[O '_' x e 'of' f ]"
(at level 0, x, e at level 0, format "[O '_' x e 'of' f ]").

These notations are printing only in order to display 'O without looking at the contents, use showo to display

Reserved Notation "''O_' x e "
  (at level 0, x, e at level 0, format "''O_' x e ").
Reserved Notation "''a_O_' x e "
  (at level 0, x, e at level 0, format "''a_O_' x e ").
Reserved Notation "''O' '_' x"
  (at level 0, x at level 0, format "''O' '_' x").

Reserved Notation "f = g '+O_' F h"
  (at level 70, no associativity,
   g at next level, F at level 0, h at next level,
   format "f = g '+O_' F h").
Reserved Notation "f '=O_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '=O_' F h").
Reserved Notation "f == g '+O_' F h"
  (at level 70, no associativity,
   g at next level, F at level 0, h at next level,
   format "f == g '+O_' F h").
Reserved Notation "f '==O_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '==O_' F h").

Reserved Notation "[O_( x \near F ) ex 'of' fx ]"
  (at level 0, x, ex at level 0, only parsing).

Printing

Reserved Notation "[O '_(' x \near F ')' ex 'of' fx ]"
(at level 0, x, ex at level 0,
format "[O '_(' x \near F ')' ex 'of' fx ]").

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Reserved Notation "''O_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''O_(' x \near F ')' ex").
Reserved Notation "''a_O_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''a_O_(' x \near F ')' ex").
Reserved Notation "''O' '_(' x \near F ')' ex"
  (at level 0, x, ex at level 0, format "''O' '_(' x \near F ')' ex").

Reserved Notation "fx = gx '+O_(' x \near F ')' hx"
  (at level 70, no associativity,
   gx at next level, F at level 0, hx at next level,
   format "fx = gx '+O_(' x \near F ')' hx").
Reserved Notation "fx '=O_(' x \near F ')' hx"
  (at level 70, no associativity,
   F at level 0, hx at next level,
   format "fx '=O_(' x \near F ')' hx").
Reserved Notation "fx == gx '+O_(' x \near F ')' hx"
  (at level 70, no associativity,
   gx at next level, F at level 0, hx at next level,
   format "fx == gx '+O_(' x \near F ')' hx").
Reserved Notation "fx '==O_(' x \near F ')' hx"
  (at level 70, no associativity,
   F at level 0, hx at next level,
   format "fx '==O_(' x \near F ')' hx").

Reserved Notation "f '~_' F g"
  (at level 70, F at level 0, g at next level, format "f '~_' F g").
Reserved Notation "f '~~_' F g"
  (at level 70, F at level 0, g at next level, format "f '~~_' F g").

Reserved Notation "{Omega_ F f }"
  (at level 0, F at level 0, format "{Omega_ F f }").
Reserved Notation "[bigOmega 'of' f 'for' fT ]"
  (at level 0, f at level 0, format "[bigOmega 'of' f 'for' fT ]").
Reserved Notation "[bigOmega 'of' f ]"
  (at level 0, f at level 0, format "[bigOmega 'of' f ]").
Reserved Notation "[Omega_ x e 'of' f ]"
  (at level 0, x, e at level 0, only parsing).

Printing

Reserved Notation "[Omega '_' x e 'of' f ]"
  (at level 0, x, e at level 0, format "[Omega '_' x e 'of' f ]").
Reserved Notation "'Omega_ F g"
  (at level 0, F at level 0, format "''Omega_' F g").
Reserved Notation "f '=Omega_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '=Omega_' F h").

Reserved Notation "{Theta_ F g }"
  (at level 0, F at level 0, format "{Theta_ F g }").
Reserved Notation "[bigTheta 'of' f 'for' fT ]"
  (at level 0, f at level 0, format "[bigTheta 'of' f 'for' fT ]").
Reserved Notation "[bigTheta 'of' f ]"
  (at level 0, f at level 0, format "[bigTheta 'of' f ]").
Reserved Notation "[Theta_ x e 'of' f ]"
  (at level 0, x, e at level 0, only parsing).

Printing

Reserved Notation "[Theta '_' x e 'of' f ]"
  (at level 0, x, e at level 0, format "[Theta '_' x e 'of' f ]").
Reserved Notation "'Theta_ F g"
  (at level 0, F at level 0, format "''Theta_' F g").
Reserved Notation "f '=Theta_' F h"
  (at level 70, no associativity,
   F at level 0, h at next level,
   format "f '=Theta_' F h").

Delimit Scope R_scope with coqR.
Local Open Scope ring_scope.
Local Open Scope classical_set_scope.

tags for littleo and bigO notations

Definition the_tag : unit := tt.
Definition gen_tag : unit := tt.
Definition a_tag : unit := tt.
Lemma showo : (gen_tag = tt ) × (the_tag = tt ) × (a_tag = tt ).

Tentative to handle small o and big O notations

Section Domination.
Context {K : numDomainType} {T : Type} {V W : normedModType K}.

Let littleo_def (F : set (set T)) (f : T → V) (g : T → W) :=
  ∀ eps, 0 < eps → \∀ x \near F , `|f x| ≤ eps × `|g x|.

Structure littleo_type (F : set (set T)) (g : T → W) := Littleo {
  littleo_fun :> T → V;
  _ : `[< littleo_def F littleo_fun g >]
}.
Notation "{o_ F f }" := (littleo_type F f).

Canonical littleo_subtype (F : set (set T)) (g : T → W) :=
  [subType for (@littleo_fun F g)].

Lemma littleo_class (F : set (set T)) (g : T → W) (f : {o_F g }) :
  `[< littleo_def F f g >].
Hint Resolve littleo_class : core.

Definition littleo_clone (F : set (set T)) (g : T → W) (f : T → V) (fT : {o_F g }) c
  of phant_id (littleo_class fT) c := @Littleo F g f c.
Notation "[littleo 'of' f 'for' fT ]" := (@littleo_clone _ _ f fT _ idfun).
Notation "[littleo 'of' f ]" := (@littleo_clone _ _ f _ _ idfun).

Lemma littleo0_subproof F (g : T → W) :
  Filter F → littleo_def F (0 : T → V) g.

Canonical littleo0 (F : filter_on T) g :=
  Littleo (asboolT (@littleo0_subproof F g _)).

Definition the_littleo (_ : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := littleo_fun (insubd (littleo0 F h) f).
Notation PhantomF := (Phantom (set (set T))).
Arguments the_littleo : simpl never, clear implicits.

Notation mklittleo tag x := (the_littleo tag _ (PhantomF x)).

Parsing

Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).

Printing

Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e).

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Notation "''o_' x e " := (the_littleo the_tag _ (PhantomF x) _ e).
Notation "''a_o_' x e " := (the_littleo a_tag _ (PhantomF x) _ e).
Notation "''o' '_' x" := (the_littleo gen_tag _ (PhantomF x) _).

Notation "f = g '+o_' F h" :=
  (f%function = g%function + mklittleo the_tag F (f \- g) h).
Notation "f '=o_' F h" := (f%function = (mklittleo the_tag F f h)).
Notation "f == g '+o_' F h" :=
  (f%function == g%function + mklittleo the_tag F (f \- g) h).
Notation "f '==o_' F h" := (f%function == (mklittleo the_tag F f h)).

Notation "[o_( x \near F ) ex 'of' f ]" :=
  (mklittleo gen_tag F (fun x ⇒ f) (fun x ⇒ ex) x).
Notation "[o '_(' x \near F ')' ex 'of' f ]" :=
  (the_littleo _ _ (PhantomF F) (fun x ⇒ f) (fun x ⇒ ex) x).
Notation "''o_(' x \near F ')' ex" :=
  (the_littleo the_tag _ (PhantomF F) _ (fun x ⇒ ex) x).
Notation "''a_o_(' x \near F ')' ex" :=
  (the_littleo a_tag _ (PhantomF F) _ (fun x ⇒ ex) x).
Notation "''o' '_(' x \near F ')' ex" :=
  (the_littleo gen_tag _ (PhantomF F) _ (fun x ⇒ ex) x).

Notation "fx = gx '+o_(' x \near F ')' hx" :=
  (fx = gx + mklittleo the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '=o_(' x \near F ')' hx" :=
  (fx = (mklittleo the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).
Notation "fx == gx '+o_(' x \near F ')' hx" :=
  (fx == gx + mklittleo the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '==o_(' x \near F ')' hx" :=
  (fx == (mklittleo the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).

Lemma littleoP (F : set (set T)) (g : T → W) (f : {o_F g }) : littleo_def F f g.
Hint Extern 0 (littleo_def _ _ _) ⇒ solve[apply: littleoP] : core.
Hint Extern 0 (nbhs _ _) ⇒ solve[apply: littleoP] : core.
Hint Extern 0 (prop_near1 _) ⇒ solve[apply: littleoP] : core.
Hint Extern 0 (prop_near2 _) ⇒ solve[apply: littleoP] : core.

Lemma littleoE (tag : unit) (F : filter_on T)
   (phF : phantom (set (set T)) F) f h :
   littleo_def F f h → the_littleo tag F phF f h = f.

Canonical the_littleo_littleo (tag : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := [littleo of the_littleo tag F phF f h ].

Variant littleo_spec (F : set (set T)) (g : T → W) : (T → V ) → Type :=
  LittleoSpec f of littleo_def F f g : littleo_spec F g f.

Lemma littleo (F : set (set T)) (g : T → W) (f : {o_F g }) : littleo_spec F g f.

Lemma opp_littleo_subproof (F : filter_on T) e (df : {o_F e }) :
   littleo_def F (- (df : _ → _)) e.

Canonical opp_littleo (F : filter_on T) e (df : {o_F e }) :=
  Littleo (asboolT (opp_littleo_subproof df)).

Lemma oppo (F : filter_on T) (f : T → V) e : - [o_F e of f ] =o_F e.

Lemma oppox (F : filter_on T) (f : T → V) e x :
  - [o_F e of f ] x = [o_F e of - [o_F e of f ]] x.

Lemma eqadd_some_oP (F : filter_on T) (f g : T → V) (e : T → W) h :
  f = g + [o_F e of h ] → littleo_def F (f - g) e.

Lemma eqaddoP (F : filter_on T) (f g : T → V) (e : T → W) :
   (f = g +o_ F e ) ↔ (littleo_def F (f - g) e ).

Lemma eqoP (F : filter_on T) (e : T → W) (f : T → V) :
   (f =o_ F e ) ↔ (littleo_def F f e ).

Lemma eq_some_oP (F : filter_on T) (e : T → W) (f : T → V) h :
   f = [o_F e of h ] → littleo_def F f e.

replaces a 'o_F e by a "canonical one" mostly to prevent problems with dependent types

Lemma eqaddoE (F : filter_on T) (f g : T → V) h (e : T → W) :
  f = g + mklittleo a_tag F h e → f = g +o_ F e.

Lemma eqoE (F : filter_on T) (f : T → V) h (e : T → W) :
  f = mklittleo a_tag F h e → f =o_F e.

Lemma eqoEx (F : filter_on T) (f : T → V) h (e : T → W) :
  (∀ x, f x = mklittleo a_tag F h e x ) →
  (∀ x, f x =o_(x \near F ) e x ).

Lemma eqaddoEx (F : filter_on T) (f g : T → V) h (e : T → W) :
  (∀ x, f x = g x + mklittleo a_tag F h e x ) →
  (∀ x, f x = g x +o_(x \near F ) (e x )).

Lemma littleo_eqo (F : filter_on T) (g : T → W) (f : {o_F g }) :
   (f : _ → _) =o_F g.

End Domination.

Section Domination_numFieldType.
Context {K : numFieldType} {T : Type} {V W : normedModType K}.

Let bigO_def (F : set (set T)) (f : T → V) (g : T → W) :=
  \∀ k \near +oo , \∀ x \near F , `|f x| ≤ k × `|g x|.

Let bigO_ex_def (F : set (set T)) (f : T → V) (g : T → W) :=
  exists2 k , k > 0 & \∀ x \near F , `|f x| ≤ k × `|g x|.

Lemma bigO_exP (F : set (set T)) (f : T → V) (g : T → W) :
  Filter F → bigO_ex_def F f g ↔ bigO_def F f g.

Structure bigO_type (F : set (set T)) (g : T → W) := BigO {
  bigO_fun :> T → V;
  _ : `[< bigO_def F bigO_fun g >]
}.
Notation "{O_ F f }" := (bigO_type F f).

Canonical bigO_subtype (F : set (set T)) (g : T → W) :=
  [subType for (@bigO_fun F g)].

Lemma bigO_class (F : set (set T)) (g : T → W) (f : {O_F g }) :
  `[< bigO_def F f g >].
Hint Resolve bigO_class : core.

Definition bigO_clone (F : set (set T)) (g : T → W) (f : T → V) (fT : {O_F g }) c
  of phant_id (bigO_class fT) c := @BigO F g f c.
Notation "[bigO 'of' f 'for' fT ]" := (@bigO_clone _ _ f fT _ idfun).
Notation "[bigO 'of' f ]" := (@bigO_clone _ _ f _ _ idfun).

Lemma bigO0_subproof F (g : T → W) : Filter F → bigO_def F (0 : T → V) g.

Canonical bigO0 (F : filter_on T) g := BigO (asboolT (@bigO0_subproof F g _)).

Definition the_bigO (u : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := bigO_fun (insubd (bigO0 F h) f).
Arguments the_bigO : simpl never, clear implicits.

Notation PhantomF := (Phantom (set (set T))).
Notation mkbigO tag x := (the_bigO tag _ (PhantomF x)).

Notation "[O_ x e 'of' f ]" := (mkbigO gen_tag x f e).

Notation "[O '_' x e 'of' f ]" := (the_bigO _ _ (PhantomF x) f e).

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Notation "''O_' x e " := (the_bigO the_tag _ (PhantomF x) _ e).
Notation "''a_O_' x e " := (the_bigO a_tag _ (PhantomF x) _ e).
Notation "''O' '_' x" := (the_bigO gen_tag _ (PhantomF x) _).

Notation "[O_( x \near F ) e 'of' f ]" :=
  (mkbigO gen_tag F (fun x ⇒ f) (fun x ⇒ e) x).
Notation "[O '_(' x \near F ')' e 'of' f ]" :=
  (the_bigO _ _ (PhantomF F) (fun x ⇒ f) (fun x ⇒ e) x).
Notation "''O_(' x \near F ')' e" :=
  (the_bigO the_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''a_O_(' x \near F ')' e" :=
  (the_bigO a_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''O' '_(' x \near F ')' e" :=
  (the_bigO gen_tag _ (PhantomF F) _ (fun x ⇒ e) x).

Notation "f = g '+O_' F h" :=
  (f%function = g%function + mkbigO the_tag F (f \- g) h).
Notation "f '=O_' F h" := (f%function = mkbigO the_tag F f h).
Notation "f == g '+O_' F h" :=
  (f%function == g%function + mkbigO the_tag F (f \- g) h).
Notation "f '==O_' F h" := (f%function == mkbigO the_tag F f h).

Notation "fx = gx '+O_(' x \near F ')' hx" :=
  (fx = gx + mkbigO the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '=O_(' x \near F ')' hx" :=
  (fx = (mkbigO the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).
Notation "fx == gx '+O_(' x \near F ')' hx" :=
  (fx == gx + mkbigO the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '==O_(' x \near F ')' hx" :=
  (fx == (mkbigO the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).

Lemma bigOP (F : set (set T)) (g : T → W) (f : {O_F g }) : bigO_def F f g.
Hint Extern 0 (bigO_def _ _ _) ⇒ solve[apply: bigOP] : core.
Hint Extern 0 (nbhs _ _) ⇒ solve[apply: bigOP] : core.
Hint Extern 0 (prop_near1 _) ⇒ solve[apply: bigOP] : core.
Hint Extern 0 (prop_near2 _) ⇒ solve[apply: bigOP] : core.

Lemma bigOE (tag : unit) (F : filter_on T) (phF : phantom (set (set T)) F) f h :
   bigO_def F f h → the_bigO tag F phF f h = f.

Canonical the_bigO_bigO (tag : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := [bigO of the_bigO tag F phF f h ].

Variant bigO_spec (F : set (set T)) (g : T → W) : (T → V ) → Prop :=
  BigOSpec f (k : {posnum K })
    of (\∀ x \near F , `|f x| ≤ k %:num × `|g x|) :
      bigO_spec F g f.

Lemma bigO (F : filter_on T) (g : T → W) (f : {O_F g }) : bigO_spec F g f.

Lemma opp_bigO_subproof (F : filter_on T) e (df : {O_F e }) :
   bigO_def F (- (df : _ → _)) e.

Canonical Opp_bigO (F : filter_on T) e (df : {O_F e }) :=
  BigO (asboolT (opp_bigO_subproof df)).

Lemma oppO (F : filter_on T) (f : T → V) e : - [O_F e of f ] =O_F e.

Lemma oppOx (F : filter_on T) (f : T → V) e x :
  - [O_F e of f ] x = [O_F e of - [O_F e of f ]] x.

Lemma add_bigO_subproof (F : filter_on T) e (df dg : {O_F e }) :
  bigO_def F (df \+ dg) e.

Canonical add_bigO (F : filter_on T) e (df dg : {O_F e }) :=
  @BigO _ _ (_ + _) (asboolT (add_bigO_subproof df dg)).
Canonical addfun_bigO (F : filter_on T) e (df dg : {O_F e }) :=
  BigO (asboolT (add_bigO_subproof df dg)).

Lemma addO (F : filter_on T) (f g: T → V) e :
  [O_F e of f ] + [O_F e of g ] =O_F e.

Lemma addOx (F : filter_on T) (f g: T → V) e x :
  [O_F e of f ] x + [O_F e of g ] x =
  [O_F e of [O_F e of f ] + [O_F e of g ]] x.

Lemma eqadd_some_OP (F : filter_on T) (f g : T → V) (e : T → W) h :
  f = g + [O_F e of h ] → bigO_def F (f - g) e.

Lemma eqaddOP (F : filter_on T) (f g : T → V) (e : T → W) :
   (f = g +O_ F e ) ↔ (bigO_def F (f - g) e ).

Lemma eqOP (F : filter_on T) (e : T → W) (f : T → V) :
   (f =O_ F e ) ↔ (bigO_def F f e ).

Lemma eqO_exP (F : filter_on T) (e : T → W) (f : T → V) :
   (f =O_ F e ) ↔ (bigO_ex_def F f e ).

Lemma eq_some_OP (F : filter_on T) (e : T → W) (f : T → V) h :
   f = [O_F e of h ] → bigO_def F f e.

Lemma bigO_eqO (F : filter_on T) (g : T → W) (f : {O_F g }) :
   (f : _ → _) =O_F g.

Lemma eqO_bigO (F : filter_on T) (e : T → W) (f : T → V) :
   f =O_ F e → bigO_def F f e.

replaces a 'O_F e by a "canonical one" mostly to prevent problems with dependent types

Lemma eqaddOE (F : filter_on T) (f g : T → V) h (e : T → W) :
  f = g + mkbigO a_tag F h e → f = g +O_ F e.

Lemma eqOE (F : filter_on T) (f : T → V) h (e : T → W) :
  f = mkbigO a_tag F h e → f =O_F e.

Lemma eqOEx (F : filter_on T) (f : T → V) h (e : T → W) :
  (∀ x, f x = mkbigO a_tag F h e x ) →
  (∀ x, f x =O_(x \near F ) e x ).

Lemma eqaddOEx (F : filter_on T) (f g : T → V) h (e : T → W) :
  (∀ x, f x = g x + mkbigO a_tag F h e x ) →
  (∀ x, f x = g x +O_(x \near F ) (e x )).

duplicate from Section Domination

Notation mklittleo tag x := (the_littleo tag (PhantomF x)).

Parsing

Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).

Printing

Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e).

Lemma eqoO (F : filter_on T) (f : T → V) (e : T → W) :
[o_F e of f ] =O_F e.
Hint Resolve eqoO : core.

NB: duplicate from Section Domination

Notation "{o_ F f }" := (littleo_type F f).

Lemma littleo_eqO (F : filter_on T) (e : T → W) (f : {o_F e }) :
   (f : _ → _) =O_F e.

Canonical littleo_is_bigO (F : filter_on T) (e : T → W) (f : {o_F e }) :=
  BigO (asboolT (eqO_bigO (littleo_eqO f))).
Canonical the_littleo_bigO (tag : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := [bigO of the_littleo tag phF f h ].

End Domination_numFieldType.

Notation "{o_ F f }" := (@littleo_type _ _ _ _ F f).
Notation "{O_ F f }" := (@bigO_type _ _ _ _ F f).

Notation "[littleo 'of' f 'for' fT ]" :=
  (@littleo_clone _ _ _ _ _ _ f fT _ idfun).
Notation "[littleo 'of' f ]" := (@littleo_clone _ _ _ _ _ _ f _ _ idfun).

Notation "[bigO 'of' f 'for' fT ]" := (@bigO_clone _ _ _ _ _ _ f fT _ idfun).
Notation "[bigO 'of' f ]" := (@bigO_clone _ _ _ _ _ _ f _ _ idfun).

Arguments the_littleo {_ _ _ _} _ _ _ _ _ : simpl never.
Arguments the_bigO {_ _ _ _} _ _ _ _ _ : simpl never.

Notation mklittleo tag x := (the_littleo tag _ (PhantomF x)).

Parsing

Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).
Notation "[o_( x \near F ) e 'of' f ]" :=
(mklittleo gen_tag F (fun x ⇒ f) (fun x ⇒ e) x).
Notation "'o_ x" := (the_littleo _ _ (PhantomF x) _).
Notation "'o" := (the_littleo _ _ _ _).

Printing

Notation "[o '_(' x \near F ')' e 'of' f ]" :=
(the_littleo _ _ (PhantomF F) (fun x ⇒ f) (fun x ⇒ e) x).
Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (Phantom _ x) f e).

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Notation "''o_' x e " := (the_littleo the_tag _ (Phantom _ x) _ e).
Notation "''a_o_' x e " := (the_littleo a_tag _ (Phantom _ x) _ e).
Notation "''o' '_' x" := (the_littleo gen_tag _ (Phantom _ x) _).

Notation "''o_(' x \near F ')' e" :=
  (the_littleo the_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''a_o_(' x \near F ')' e" :=
  (the_littleo a_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''o' '_(' x \near F ')' e" :=
  (the_littleo gen_tag _ (PhantomF F) _ (fun x ⇒ e) x).

Notation mkbigO tag x := (the_bigO tag _ (PhantomF x)).

Parsing

Notation "[O_ x e 'of' f ]" := (mkbigO gen_tag x f e).
Notation "[O_( x \near F ) e 'of' f ]" :=
(mkbigO gen_tag F (fun x ⇒ f) (fun x ⇒ e) x).
Notation "'O_ x" := (the_bigO _ _ (PhantomF x) _).
Notation "'O" := (the_bigO _ _ _ _).

Printing

Notation "[O '_' x e 'of' f ]" := (the_bigO _ _ (Phantom _ x) f e).
Notation "[O '_(' x \near F ')' e 'of' f ]" :=
(the_bigO _ _ (PhantomF F) (fun x ⇒ f) (fun x ⇒ e) x).

These notations are printing only in order to display 'o without looking at the contents, use showo to display

Notation "''O_' x e " := (the_bigO the_tag _ (Phantom _ x) _ e).
Notation "''a_O_' x e " := (the_bigO a_tag _ (Phantom _ x) _ e).
Notation "''O' '_' x" := (the_bigO gen_tag _ (Phantom _ x) _).

Notation "''O_(' x \near F ')' e" :=
  (the_bigO the_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''a_O_(' x \near F ')' e" :=
  (the_bigO a_tag _ (PhantomF F) _ (fun x ⇒ e) x).
Notation "''O' '_(' x \near F ')' e" :=
  (the_bigO gen_tag _ (PhantomF F) _ (fun x ⇒ e) x).

Notation "f = g '+o_' F h" :=
  (f%function = g%function + mklittleo the_tag F (f \- g) h).
Notation "f '=o_' F h" := (f%function = (mklittleo the_tag F f h)).
Notation "f == g '+o_' F h" :=
  (f%function == g%function + mklittleo the_tag F (f \- g) h).
Notation "f '==o_' F h" := (f%function == (mklittleo the_tag F f h)).
Notation "fx = gx '+o_(' x \near F ')' hx" :=
  (fx = gx + mklittleo the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '=o_(' x \near F ')' hx" :=
  (fx = (mklittleo the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).
Notation "fx == gx '+o_(' x \near F ')' hx" :=
  (fx == gx + mklittleo the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '==o_(' x \near F ')' hx" :=
  (fx == (mklittleo the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).

Notation "f = g '+O_' F h" :=
  (f%function = g%function + mkbigO the_tag F (f \- g) h).
Notation "f '=O_' F h" := (f%function = mkbigO the_tag F f h).
Notation "f == g '+O_' F h" :=
  (f%function == g%function + mkbigO the_tag F (f \- g) h).
Notation "f '==O_' F h" := (f%function == mkbigO the_tag F f h).
Notation "fx = gx '+O_(' x \near F ')' hx" :=
  (fx = gx + mkbigO the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '=O_(' x \near F ')' hx" :=
  (fx = (mkbigO the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).
Notation "fx == gx '+O_(' x \near F ')' hx" :=
  (fx == gx + mkbigO the_tag F
                  ((fun x ⇒ fx) \- (fun x ⇒ gx%R)) (fun x ⇒ hx) x).
Notation "fx '==O_(' x \near F ')' hx" :=
  (fx == (mkbigO the_tag F (fun x ⇒ fx) (fun x ⇒ hx) x)).

#[global] Hint Extern 0 (_ = 'o__ _) ⇒ apply: eqoE; reflexivity : core.
#[global] Hint Extern 0 (_ = 'O__ _) ⇒ apply: eqOE; reflexivity : core.
#[global] Hint Extern 0 (_ = 'O__ _) ⇒ apply: eqoO; reflexivity : core.
#[global] Hint Extern 0 (_ = _ + 'o__ _) ⇒ apply: eqaddoE; reflexivity : core.
#[global] Hint Extern 0 (_ = _ + 'O__ _) ⇒ apply: eqaddOE; reflexivity : core.
#[global] Hint Extern 0 (\∀ k \near +oo , \∀ x \near _,
  is_true (`|_ x| ≤ k × `|_ x|)) ⇒ solve[apply: bigOP] : core.
#[global] Hint Extern 0 (nbhs _ _) ⇒ solve[apply: bigOP] : core.
#[global] Hint Extern 0 (prop_near1 _) ⇒ solve[apply: bigOP] : core.
#[global] Hint Extern 0 (prop_near2 _) ⇒ solve[apply: bigOP] : core.
#[global] Hint Extern 0 (∀ e, is_true (0 < e) → \∀ x \near _,
  is_true (`|_ x| ≤ e × `|_ x|)) ⇒ solve[apply: littleoP] : core.
#[global] Hint Extern 0 (nbhs _ _) ⇒ solve[apply: littleoP] : core.
#[global] Hint Extern 0 (prop_near1 _) ⇒ solve[apply: littleoP] : core.
#[global] Hint Extern 0 (prop_near2 _) ⇒ solve[apply: littleoP] : core.
#[global] Hint Resolve littleo_class : core.
#[global] Hint Resolve bigO_class : core.
#[global] Hint Resolve littleo_eqO : core.

Arguments bigO {_ _ _ _}.

Section Domination_numFieldType.
Context {K : numFieldType} {T : Type} {V W : normedModType K}.

duplicate from Section Domination

Let littleo_def (F : set (set T)) (f : T → V) (g : T → W) :=
  ∀ eps, 0 < eps → \∀ x \near F , `|f x| ≤ eps × `|g x|.

Lemma add_littleo_subproof (F : filter_on T) e (df dg : {o_F e }) :
  littleo_def F (df \+ dg) e.

Canonical add_littleo (F : filter_on T) e (df dg : {o_F e }) :=
  @Littleo _ _ _ _ _ _ (_ + _) (asboolT (add_littleo_subproof df dg)).
Canonical addfun_littleo (F : filter_on T) e (df dg : {o_F e }) :=
  @Littleo _ _ _ _ _ _ (_ \+ _) (asboolT (add_littleo_subproof df dg)).

Lemma addo (F : filter_on T) (f g: T → V) (e : _ → W) :
  [o_F e of f ] + [o_F e of g ] =o_F e.

Lemma addox (F : filter_on T) (f g: T → V) (e : _ → W) x :
  [o_F e of f ] x + [o_F e of g ] x =
  [o_F e of [o_F e of f ] + [o_F e of g ]] x.

Hint Extern 0 (littleo_def _ _ _) ⇒ solve[apply: littleoP] : core.

Lemma scale_littleo_subproof (F : filter_on T) e (df : {o_F e }) a :
  littleo_def F (a *: (df : _ → _)) e.

Canonical scale_littleo (F : filter_on T) e a (df : {o_F e }) :=
  Littleo (asboolT (scale_littleo_subproof df a)).

Lemma scaleo (F : filter_on T) a (f : T → V) (e : _ → W) :
  a *: [o_F e of f ] = [o_F e of a *: [o_F e of f ]].

Lemma scaleox (F : filter_on T) a (f : T → V) (e : _ → W) x :
  a *: ([o_F e of f ] x) = [o_F e of a *: [o_F e of f ]] x.

End Domination_numFieldType.

Lemma scaleolx (K : numFieldType) (V W : normedModType K) {T : Type}
  (F : filter_on T) (a : W) (k : T → K^o) (e : T → V) (x : T) :
  ([o_F e of k ] x) *: a = [o_F e of (fun y ⇒ [o_F e of k ] y *: a )] x.

Section Limit.
Context {K : numFieldType} {T : Type} {V W X : normedModType K}.

Lemma eqolimP (F : filter_on T) (f : T → V) (l : V) :
  f @ F --> l ↔ f = cst l +o_F (cst (1 : K^o)).

Lemma eqolim (F : filter_on T) (f : T → V) (l : V) e :
  f = cst l + [o_F (cst (1 : K^o)) of e ] → f @ F --> l.

Lemma eqolim0P (F : filter_on T) (f : T → V) :
  f @ F --> (0 : V ) ↔ f =o_F (cst (1 : K^o)).

Lemma eqolim0 (F : filter_on T) (f : T → V) :
  f =o_F (cst (1 : K^o)) → f @ F --> (0 : V ).

Lemma littleo_bigO_eqo {F : filter_on T}
  (g : T → W) (f : T → V) (h : T → X) :
  f =O_F g → [o_F f of h ] =o_F g.
Arguments littleo_bigO_eqo {F}.

Lemma bigO_littleo_eqo {F : filter_on T} (g : T → W) (f : T → V) (h : T → X) :
  f =o_F g → [O_F f of h ] =o_F g.
Arguments bigO_littleo_eqo {F}.

Lemma add2o (F : filter_on T) (f g : T → V) (e : T → W) :
  f =o_F e → g =o_F e → f + g =o_F e.

Lemma addfo (F : filter_on T) (h f : T → V) (e : T → W) :
  f =o_F e → f + [o_F e of h ] =o_F e.

Lemma oppfo (F : filter_on T) (h f : T → V) (e : T → W) :
  f =o_F e → - f =o_F e.

Lemma add2O (F : filter_on T) (f g : T → V) (e : T → W) :
  f =O_F e → g =O_F e → f + g =O_F e.

Lemma addfO (F : filter_on T) (h f : T → V) (e : T → W) :
  f =O_F e → f + [O_F e of h ] =O_F e.

Lemma oppfO (F : filter_on T) (h f : T → V) (e : T → W) :
  f =O_F e → - f =O_F e.

Lemma idO (F : filter_on T) (e : T → W) : e =O_F e.

Lemma littleo_littleo (F : filter_on T) (f : T → V) (g : T → W) (h : T → X) :
  f =o_F g → [o_F f of h ] =o_F g.

End Limit.
Arguments littleo_bigO_eqo {K T V W X F}.
Arguments bigO_littleo_eqo {K T V W X F}.

Section Limit_realFieldType.
Context {K : realFieldType}
  {T : Type} {V W X : normedModType K}.

Lemma bigO_bigO_eqO {F : filter_on T} (g : T → W) (f : T → V) (h : T → X) :
  f =O_F g → ([O_F f of h ] : _ → _) =O_F g.
Arguments bigO_bigO_eqO {F}.

End Limit_realFieldType.
Arguments littleo_bigO_eqo {K T V W X F}.
Arguments bigO_littleo_eqo {K T V W X F}.
Arguments bigO_bigO_eqO {K T V W X F}.

Section littleo_bigO_transitivity.

Context {K : numFieldType} {T : Type} {V W Z : normedModType K}.

Lemma eqaddo_trans (F : filter_on T) (f g h : T → V) fg gh (e : T → W):
  f = g + [o_ F e of fg ] → g = h + [o_F e of gh ] → f = h +o_F e.

End littleo_bigO_transitivity.

Section littleo_bigO_transitivity.
Context {K : numFieldType} {T : Type} {V W Z : normedModType K}.

Lemma eqaddO_trans (F : filter_on T) (f g h : T → V) fg gh (e : T → W):
  f = g + [O_ F e of fg ] → g = h + [O_F e of gh ] → f = h +O_F e.

Lemma eqaddoO_trans (F : filter_on T) (f g h : T → V) fg gh (e : T → W):
  f = g + [o_ F e of fg ] → g = h + [O_F e of gh ] → f = h +O_F e.

Lemma eqaddOo_trans (F : filter_on T) (f g h : T → V) fg gh (e : T → W):
  f = g + [O_ F e of fg ] → g = h + [o_F e of gh ] → f = h +O_F e.

Lemma eqo_trans (F : filter_on T) (f : T → V) f' (g : T → W) g' (h : T → Z) :
  f = [o_F g of f'] → g = [o_F h of g'] → f =o_F h.

Lemma eqOo_trans (F : filter_on T) (f : T → V) f' (g : T → W) g' (h : T → Z) :
  f = [O_F g of f'] → g = [o_F h of g'] → f =o_F h.

Lemma eqoO_trans (F : filter_on T) (f : T → V) f' (g : T → W) g' (h : T → Z) :
  f = [o_F g of f'] → g = [O_F h of g'] → f =o_F h.
End littleo_bigO_transitivity.

Section littleo_bigO_transitivity_realFieldType.
Context {K : realFieldType} {T : Type}
  {V W Z : normedModType K}.

Lemma eqO_trans (F : filter_on T) (f : T → V) f' (g : T → W) g' (h : T → Z) :
  f = [O_F g of f'] → g = [O_F h of g'] → f =O_F h.
End littleo_bigO_transitivity_realFieldType.

Section rule_of_products_rcfType.

Variables (R : rcfType) (pT : pointedType).

Lemma mulo (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [o_F h1 of f ] × [o_F h2 of g ] =o_F (h1 × h2 ).

Lemma mulO (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [O_F h1 of f ] × [O_F h2 of g ] =O_F (h1 × h2 ).

End rule_of_products_rcfType.

Section rule_of_products_numClosedFieldType.

Variables (R : numClosedFieldType) (pT : pointedType).

Lemma mulo_numClosedFieldType (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [o_F h1 of f ] × [o_F h2 of g ] =o_F (h1 × h2 ).

Lemma mulO_numClosedFieldType (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [O_F h1 of f ] × [O_F h2 of g ] =O_F (h1 × h2 ).

End rule_of_products_numClosedFieldType.

Section Linear3.
Context (R : realFieldType) (U : normedModType R) (V : normedModType R)
        (s : R → V → V) (s_law : GRing.Scale.law s).
Hypothesis (normm_s : ∀ k x, `|s k x| = `|k| × `|x|).

Lemma linear_for_continuous (f : {linear U → V | GRing.Scale.op s_law}) :
  (f : _ → _) =O_ (0 : U ) (cst (1 : R^o)) → continuous f.

End Linear3.

Arguments linear_for_continuous {R U V s s_law normm_s} f _.

Lemma linear_continuous (R : realFieldType) (U : normedModType R)
  (V : normedModType R) (f : {linear U → V}) :
  (f : _ → _) =O_ (0 : U ) (cst (1 : R^o)) → continuous f.

Lemma linear_for_mul_continuous (R : realFieldType) (U : normedModType R)
  (f : {linear U → R | (@GRing.mul [ringType of R^o])}) :
  (f : _ → _) =O_ (0 : U ) (cst (1 : R^o)) → continuous f.

Notation "f '~_' F g" := (f = g +o_ F g).
Notation "f '~~_' F g" := (f == g +o_ F g).

Section asymptotic_equivalence.

Context {K : realFieldType} {T : Type} {V W : normedModType K}.
Implicit Types F : filter_on T.

Lemma equivOLR F (f g : T → V) : f ¬_F g → f =O_F g.

Lemma equiv_refl F (f : T → V) : f ¬_F f.

Lemma equivoRL (W' : normedModType K) F (f g : T → V) (h : T → W') :
  f ¬_F g → [o_F g of h ] =o_F f.

Lemma equiv_sym F (f g : T → V) : f ¬_F g → g ¬_F f.

Lemma equivoLR (W' : normedModType K) F (f g : T → V) (h : T → W') :
  f ¬_F g → [o_F f of h ] =o_F g.

Lemma equivORL F (f g : T → V) : f ¬_F g → g =O_F f.

Lemma eqoaddo (W' : normedModType K) F (f g : T → V) (h : T → W') :
  [o_F f + [o_F f of g ] of h ] =o_F f.

Lemma equiv_trans F (f g h : T → V) : f ¬_F g → g ¬_F h → f ¬_F h.

Lemma equivalence_rel_equiv F :
  equivalence_rel [rel f g : T → V | f ~~_F g ].

End asymptotic_equivalence.

Section big_omega.

Context {K : realFieldType} {T : Type} {V : normedModType K}.
Implicit Types W : normedModType K.

Let bigOmega_def W (F : set (set T)) (f : T → V) (g : T → W) :=
  exists2 k , k > 0 & \∀ x \near F , `|f x| ≥ k × `|g x|.

Structure bigOmega_type {W} (F : set (set T)) (g : T → W) := BigOmega {
  bigOmega_fun :> T → V;
  _ : `[< bigOmega_def F bigOmega_fun g >]
}.

Notation "{Omega_ F g }" := (@bigOmega_type _ F g).

Canonical bigOmega_subtype {W} (F : set (set T)) (g : T → W) :=
  [subType for (@bigOmega_fun W F g)].

Lemma bigOmega_class {W} (F : set (set T)) (g : T → W) (f : {Omega_F g }) :
  `[< bigOmega_def F f g >].
Hint Resolve bigOmega_class : core.

Definition bigOmega_clone {W} (F : set (set T)) (g : T → W) (f : T → V)
  (fT : {Omega_F g }) c of phant_id (bigOmega_class fT) c := @BigOmega W F g f c.
Notation "[bigOmega 'of' f 'for' fT ]" := (@bigOmega_clone _ _ _ f fT _ idfun).
Notation "[bigOmega 'of' f ]" := (@bigOmega_clone _ _ _ f _ _ idfun).

Lemma bigOmega_refl_subproof F (g : T → V) : Filter F → bigOmega_def F g g.

Definition bigOmega_refl (F : filter_on T) g :=
  BigOmega (asboolT (@bigOmega_refl_subproof F g _)).

Definition the_bigOmega (u : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f g :=
  bigOmega_fun (insubd (bigOmega_refl F g) f).
Arguments the_bigOmega : simpl never, clear implicits.

Notation mkbigOmega tag x := (the_bigOmega tag _ (PhantomF x)).
Notation "[Omega_ x e 'of' f ]" := (mkbigOmega gen_tag x f e).
Notation "[Omega '_' x e 'of' f ]" := (the_bigOmega _ _ (PhantomF x) f e).

Definition is_bigOmega {W} (F : set (set T)) (g : T → W) :=
  [qualify f : T → V | `[< bigOmega_def F f g >] ].
Fact is_bigOmega_key {W} (F : set (set T)) (g : T → W) : pred_key (is_bigOmega F g).
Canonical is_bigOmega_keyed {W} (F : set (set T)) (g : T → W) :=
  KeyedQualifier (is_bigOmega_key F g).
Notation "'Omega_ F g" := (is_bigOmega F g).

Lemma bigOmegaP {W} (F : set (set T)) (g : T → W) (f : {Omega_F g }) :
  bigOmega_def F f g.
Hint Extern 0 (bigOmega_def _ _ _) ⇒ solve[apply: bigOmegaP] : core.
Hint Extern 0 (nbhs _ _) ⇒ solve[apply: bigOmegaP] : core.
Hint Extern 0 (prop_near1 _) ⇒ solve[apply: bigOmegaP] : core.
Hint Extern 0 (prop_near2 _) ⇒ solve[apply: bigOmegaP] : core.

Notation "f '=Omega_' F h" := (f%function = mkbigOmega the_tag F f h).

Canonical the_bigOmega_bigOmega (tag : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := [bigOmega of the_bigOmega tag F phF f h ].

Variant bigOmega_spec {W} (F : set (set T)) (g : T → W) : (T → V ) → Prop :=
  BigOmegaSpec f (k : {posnum K }) of
    (\∀ x \near F , `|f x| ≥ k %:num × `|g x|) :
  bigOmega_spec F g f.

Lemma bigOmega {W} (F : filter_on T) (g : T → W) (f : {Omega_F g }) :
  bigOmega_spec F g f.

Lemma eqOmegaO {W} (F : filter_on T) (f : T → V) (e : T → W) :
  (f \is 'Omega_F (e )) = (e =O_F f ) :> Prop.

Lemma eqOmegaE (F : filter_on T) (f e : T → V) :
  (f =Omega_F (e )) = (f \is 'Omega_F (e )).

Lemma eqOmega_trans (F : filter_on T) (f g h : T → V) :
  f =Omega_F (g ) → g =Omega_F (h ) → f =Omega_F (h ).

End big_omega.

Notation "{Omega_ F f }" := (@bigOmega_type _ _ _ _ F f).
Notation "[bigOmega 'of' f ]" := (@bigOmega_clone _ _ _ _ _ _ f _ _ idfun).
Notation mkbigOmega tag x := (the_bigOmega tag (PhantomF x)).
Notation "[Omega_ x e 'of' f ]" := (mkbigOmega gen_tag x f e).
Notation "[Omega '_' x e 'of' f ]" := (the_bigOmega _ _ (PhantomF x) f e).
Notation "'Omega_ F g" := (is_bigOmega F g).
Notation "f '=Omega_' F h" := (f%function = mkbigOmega the_tag F f h).
Arguments bigOmega {_ _ _ _}.

Section big_omega_in_R.

Variable pT : pointedType.

Lemma addOmega (R : realFieldType) (F : filter_on pT) (f g h : _ → R^o)
  (f_nonneg : ∀ x, 0 ≤ f x) (g_nonneg : ∀ x, 0 ≤ g x) :
  f =Omega_F h → f + g =Omega_F h.

Lemma mulOmega (R : realFieldType) (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [Omega_F h1 of f ] × [Omega_F h2 of g ] =Omega_F (h1 × h2 ).

End big_omega_in_R.

Section big_theta.

Context {K : realFieldType} {T : Type} {V : normedModType K}.
Implicit Types W : normedModType K.

Let bigTheta_def W (F : set (set T)) (f : T → V) (g : T → W) :=
  exists2 k , (k .1 > 0) && (k .2 > 0) &
  \∀ x \near F , k .1 × `|g x| ≤ `|f x| ∧ `|f x| ≤ k .2 × `|g x|.

Structure bigTheta_type {W} (F : set (set T)) (g : T → W) := BigTheta {
  bigTheta_fun :> T → V;
  _ : `[< bigTheta_def F bigTheta_fun g >]
}.

Notation "{Theta_ F g }" := (@bigTheta_type _ F g).

Canonical bigTheta_subtype {W} (F : set (set T)) (g : T → W) :=
  [subType for (@bigTheta_fun W F g)].

Lemma bigTheta_class {W} (F : set (set T)) (g : T → W) (f : {Theta_F g }) :
  `[< bigTheta_def F f g >].
Hint Resolve bigTheta_class : core.

Definition bigTheta_clone {W} (F : set (set T)) (g : T → W) (f : T → V)
  (fT : {Theta_F g }) c of phant_id (bigTheta_class fT) c := @BigTheta W F g f c.
Notation "[bigTheta 'of' f 'for' fT ]" := (@bigTheta_clone _ _ _ f fT _ idfun).
Notation "[bigTheta 'of' f ]" := (@bigTheta_clone _ _ _ f _ _ idfun).

Lemma bigTheta_refl_subproof F (g : T → V) : Filter F → bigTheta_def F g g.

Definition bigTheta_refl (F : filter_on T) g :=
  BigTheta (asboolT (@bigTheta_refl_subproof F g _)).

Definition the_bigTheta (u : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f g :=
  bigTheta_fun (insubd (bigTheta_refl F g) f).
Arguments the_bigOmega : simpl never, clear implicits.

Notation mkbigTheta tag x := (@the_bigTheta tag _ (PhantomF x)).
Notation "[Theta_ x e 'of' f ]" := (mkbigTheta gen_tag x f e).
Notation "[Theta '_' x e 'of' f ]" := (the_bigTheta _ _ (PhantomF x) f e).

Definition is_bigTheta {W} (F : set (set T)) (g : T → W) :=
  [qualify f : T → V | `[< bigTheta_def F f g >] ].
Fact is_bigTheta_key {W} (F : set (set T)) (g : T → W) : pred_key (is_bigTheta F g).
Canonical is_bigTheta_keyed {W} (F : set (set T)) (g : T → W) :=
  KeyedQualifier (is_bigTheta_key F g).
Notation "'Theta_ F g" := (@is_bigTheta _ F g).

Lemma bigThetaP {W} (F : set (set T)) (g : T → W) (f : {Theta_F g }) :
  bigTheta_def F f g.
Hint Extern 0 (bigTheta_def _ _ _) ⇒ solve[apply: bigThetaP] : core.
Hint Extern 0 (nbhs _ _) ⇒ solve[apply: bigThetaP] : core.
Hint Extern 0 (prop_near1 _) ⇒ solve[apply: bigThetaP] : core.
Hint Extern 0 (prop_near2 _) ⇒ solve[apply: bigThetaP] : core.

Canonical the_bigTheta_bigTheta (tag : unit) (F : filter_on T)
  (phF : phantom (set (set T)) F) f h := [bigTheta of @the_bigTheta tag F phF f h ].

Variant bigTheta_spec {W} (F : set (set T)) (g : T → W) : (T → V ) → Prop :=
    BigThetaSpec f (k1 : {posnum K }) (k2 : {posnum K }) of
      (\∀ x \near F , k1 %:num × `|g x| ≤ `|f x|) &
      (\∀ x \near F , `|f x| ≤ k2 %:num × `|g x|) :
  bigTheta_spec F g f.

Lemma bigTheta {W} (F : filter_on T) (g : T → W) (f : {Theta_F g }) :
  bigTheta_spec F g f.

Notation "f '=Theta_' F h" := (f%function = mkbigTheta the_tag F f h).

Lemma bigThetaE {W} (F : filter_on T) (f : T → V) (g : T → W) :
  (f \is 'Theta_F (g )) = (f =O_F g ∧ f \is 'Omega_F (g )) :> Prop.

Lemma eqThetaE (F : filter_on T) (f e : T → V) :
  (f =Theta_F (e )) = (f \is 'Theta_F (e )).

Lemma eqThetaO (F : filter_on T) (f g : T → V) : [Theta_F g of f ] =O_F g.

Lemma idTheta (F : filter_on T) (f : T → V) : f =Theta_F f.

Lemma Theta_sym (F : filter_on T) (f g : T → V) :
  (f =Theta_F g ) = (g =Theta_F f ).

Lemma eqTheta_trans (F : filter_on T) (f g h : T → V) :
  f =Theta_F g → g =Theta_F h → f =Theta_F h.

End big_theta.

Notation "{Theta_ F g }" := (@bigTheta_type _ F g).
Notation "[bigTheta 'of' f ]" := (@bigTheta_clone _ _ _ _ _ _ f _ _ idfun).
Notation mkbigTheta tag x := (the_bigTheta tag (PhantomF x)).
Notation "[Theta_ x e 'of' f ]" := (mkbigTheta gen_tag x f e).
Notation "[Theta '_' x e 'of' f ]" := (the_bigTheta _ _ (PhantomF x) f e).
Notation "'Theta_ F g" := (is_bigTheta F g).
Notation "f '=Theta_' F h" := (f%function = mkbigTheta the_tag F f h).

Section big_theta_in_R.

Variables (R : rcfType (*realType*)) (pT : pointedType).

Lemma addTheta (F : filter_on pT) (f g h : _ → R^o)
  (f0 : ∀ x, 0 ≤ f x) (g0 : ∀ x, 0 ≤ g x) (h0 : ∀ x, 0 ≤ h x) :
  [Theta_F h of f ] + [O_F h of g ] =Theta_F h.

Lemma mulTheta (F : filter_on pT) (h1 h2 f g : pT → R^o) :
  [Theta_F h1 of f ] × [Theta_F h2 of g ] =Theta_F h1 × h2.

End big_theta_in_R.