Module mathcomp.analysis.landau

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import ereal reals interval_inference topology normedtype.
From mathcomp Require Import prodnormedzmodule.

# Bachmann-Landau notations: $f=o(e)$, $f=O(e)$ 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 In this file, F is a filter and V W X Y Z are normed spaces over K. 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 ``` WARNING: The piece of syntax "=O_(" is only valid in the syntax "=O_(x \near F)", not in the syntax "=O_(x : U)". ## 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 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 is 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.

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope R_scope.

Import Order.TTheory GRing.Theory Num.Theory.

Reserved Notation "{o_ F f }" (F at level 0, format "{o_ F f }").
Reserved Notation "[littleo 'of' f 'for' fT ]" (f at level 10,
  format "[littleo 'of' f 'for' fT ]").
Reserved Notation "[littleo 'of' f ]" (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).
Reserved Notation "[o_ x e 'of' f ]" (at level 0, x at level 0, only parsing).
Reserved Notation "[o '_' x e 'of' f ]"
  (at level 0, x, e at level 0, format "[o '_' x e 'of' f ]").
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).
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 ]").
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 }" (F at level 0, format "{O_ F f }").
Reserved Notation "[bigO 'of' f 'for' fT ]"
  (format "[bigO 'of' f 'for' fT ]").
Reserved Notation "[bigO 'of' f ]"
  (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).
Reserved Notation "[O_ x e 'of' f ]" (at level 0, x, e at level 0, only parsing).
Reserved Notation "[O '_' x e 'of' f ]"
  (at level 0, x, e at level 0, format "[O '_' x e 'of' f ]").
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).
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 ]").
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, format "[bigOmega 'of' f 'for' fT ]").
Reserved Notation "[bigOmega 'of' 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).
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, format "[bigTheta 'of' f 'for' fT ]").
Reserved Notation "[bigTheta 'of' f ]"
  (at level 0, format "[bigTheta 'of' f ]").
Reserved Notation "[Theta_ x e 'of' f ]"
  (at level 0, x at level 0, only parsing).
Reserved Notation "[Theta '_' x e 'of' f ]"
  (at level 0, x 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.

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

Proof.

by []. Qed.

Section Domination.
Context { : numDomainType} { : Type} { : normedModType K}.

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  forall , 0 < eps -> \forall \near F, `|f x| <= eps * `|g x|.

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

. ( T) (g : T -> W) :=
  [isSub for @littleo_fun F g].

Lemma ( : set_system T) ( : T -> W) ( : {o_F g}) :
  `[< littleo_def F f g >].

Proof.

by case: f => ?. Qed.

Hint Resolve littleo_class : core.

Definition ( : set_system T) ( : T -> W) ( : T -> V) ( : {o_F g})
& phant_id (littleo_class fT) c := @Littleo F g f c.
Notation := (@littleo_clone _ _ f fT _ idfun).
Notation := (@littleo_clone _ _ f _ _ idfun).

Lemma ( : T -> W) :
Filter F -> littleo_def F (0 : T -> V) g.

Proof.

move=> FF _/posnumP[eps] /=; apply: filterE => x; rewrite normr0.
by rewrite mulr_ge0 // ltrW.
Qed.

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

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

Notation tag x := (the_littleo tag _ (PhantomF x)).
Notation := (mklittleo gen_tag x f e).
Notation := (the_littleo _ _ (PhantomF x) f e).
Notation := (the_littleo the_tag _ (PhantomF x) _ e).
Notation := (the_littleo a_tag _ (PhantomF x) _ e).
Notation := (the_littleo gen_tag _ (PhantomF x) _).

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

Notation :=
  (mklittleo gen_tag F (fun => f) (fun => ex) x).
Notation :=
  (the_littleo _ _ (PhantomF F) (fun => f) (fun => ex) x).
Notation :=
  (the_littleo the_tag _ (PhantomF F) _ (fun => ex) x).
Notation :=
  (the_littleo a_tag _ (PhantomF F) _ (fun => ex) x).
Notation :=
  (the_littleo gen_tag _ (PhantomF F) _ (fun => ex) x).

Notation :=
  (fx = gx + mklittleo the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx = (mklittleo the_tag F (fun => fx) (fun => hx) x)).
Notation :=
  (fx == gx + mklittleo the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx == (mklittleo the_tag F (fun => fx) (fun => hx) x)).

Lemma ( : set_system T) ( : T -> W) ( : {o_F g}) : littleo_def F f g.

Proof.

exact/asboolP. Qed.

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 ( : unit) ( : filter_on T)
( : phantom (set_system T) F) :
littleo_def F f h -> the_littleo tag F phF f h = f.

Proof.

by move=> /asboolP?; rewrite /the_littleo /insubd insubT. Qed.

Lemma ( : unit) ( : filter_on T)
( : phantom (set_system T) F) :
~ littleo_def F f h -> the_littleo tag F phF f h = 0.

Proof.

by move=> ?; rewrite /the_littleo /insubd insubN//; apply/asboolP. Qed.

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

Variant ( : set_system T) ( : T -> W) : (T -> V) -> Type :=
of littleo_def F f g : littleo_spec F g f.

Lemma ( : set_system T) ( : T -> W) ( : {o_F g}) : littleo_spec F g f.

Proof.

by constructor; apply/(@littleoP F). Qed.

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

Proof.

by move=> _/posnumP[eps]; near do rewrite normrN; apply: littleoP.
Unshelve. all: by end_near. Qed.

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

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

Proof.

by rewrite [RHS]littleoE. Qed.

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

Proof.

by move: x; rewrite -/(- _ =1 _) {1}oppo. Qed.

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

Proof.

rewrite /the_littleo /insubd=> ->.
case: insubP => /= [u /asboolP fg_o_e ->|_] eps /=.
by rewrite -addrA subrKC; apply: fg_o_e.
by rewrite addrC addKr; apply: littleoP.
Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(f = g +o_ F e) <-> (littleo_def F (f - g) e).

Proof.

by split=> [/eqadd_some_oP|fg_o_e]; rewrite ?littleoE // addrC addrNK.
Qed.

Lemma ( : filter_on T) ( : T -> W) ( : T -> V) :
(f =o_ F e) <-> (littleo_def F f e).

Proof.

by rewrite -[f]subr0 -eqaddoP -[f \- 0]/(f - 0) subr0 add0r. Qed.

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

Proof.

by have := @eqadd_some_oP F f 0 e h; rewrite add0r subr0. Qed.

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

Proof.

by move=> /eqadd_some_oP /eqaddoP. Qed.

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

Proof.

by move=> /eq_some_oP /eqoP. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(forall , f x = mklittleo a_tag F h e x) ->
(forall , f x =o_( \near F) e x).

Proof.

by have := @eqoE F f h e; rewrite !funeqE. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(forall , f x = g x + mklittleo a_tag F h e x) ->
(forall , f x = g x +o_( \near F) (e x)).

Proof.

by have := @eqaddoE F f g h e; rewrite !funeqE. Qed.

Lemma ( : filter_on T) ( : T -> W) ( : {o_F g}) :
(f : _ -> _) =o_F g.

Proof.

by apply/eqoP. Qed.

End Domination.

Section Domination_numFieldType.
Context { : numFieldType} { : Type} { : normedModType K}.

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  \forall \near +oo, \forall \near F, `|f x| <= k * `|g x|.

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  exists2 , k > 0 & \forall \near F, `|f x| <= k * `|g x|.

Lemma ( : set_system T) ( : T -> V) ( : T -> W) :
  Filter F -> bigO_ex_def F f g <-> bigO_def F f g.

Proof.

split=> [[k k0 fOg] | [k [kreal fOg]]].
  exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
  by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW.
exists (Num.max 1 `|k + 1|) => //.
apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
  by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD.
by rewrite comparable_le_max ?real_comparable// lexx orbT.
Unshelve. end_near. Qed.

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

. ( T) (g : T -> W) :=
  [isSub for @bigO_fun F g].

Lemma ( : set_system T) ( : T -> W) ( : {O_F g}) :
  `[< bigO_def F f g >].

Proof.

by case: f => ?. Qed.

Hint Resolve bigO_class : core.

Definition ( : set_system T) ( : T -> W) ( : T -> V) ( : {O_F g})
& phant_id (bigO_class fT) c := @BigO F g f c.
Notation := (@bigO_clone _ _ f fT _ idfun).
Notation := (@bigO_clone _ _ f _ _ idfun).

Lemma ( : T -> W) : Filter F -> bigO_def F (0 : T -> V) g.

Proof.

by move=> FF; near do [apply: filterE => x;
rewrite normr0 pmulr_rge0 ?normr_ge0//]; exists 0.
Unshelve. all: by end_near. Qed.

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

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

Notation := (Phantom (set_system T)).
Notation tag x := (the_bigO tag _ (PhantomF x)).
Notation := (mkbigO gen_tag x f e).
Notation := (the_bigO _ _ (PhantomF x) f e).
Notation := (the_bigO the_tag _ (PhantomF x) _ e).
Notation := (the_bigO a_tag _ (PhantomF x) _ e).
Notation := (the_bigO gen_tag _ (PhantomF x) _).

Notation :=
  (mkbigO gen_tag F (fun => f) (fun => e) x).
Notation :=
  (the_bigO _ _ (PhantomF F) (fun => f) (fun => e) x).
Notation :=
  (the_bigO the_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_bigO a_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_bigO gen_tag _ (PhantomF F) _ (fun => e) x).

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

Notation :=
  (fx = gx + mkbigO the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx = (mkbigO the_tag F (fun => fx) (fun => hx) x)).
Notation :=
  (fx == gx + mkbigO the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx == (mkbigO the_tag F (fun => fx) (fun => hx) x)).

Lemma ( : set_system T) ( : T -> W) ( : {O_F g}) : bigO_def F f g.

Proof.

exact/asboolP. Qed.

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 ( : unit) ( : filter_on T) ( : phantom (set_system T) F) :
bigO_def F f h -> the_bigO tag F phF f h = f.

Proof.

by move=> /asboolP?; rewrite /the_bigO /insubd insubT. Qed.

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

Variant ( : set_system T) ( : T -> W) : (T -> V) -> Prop :=
   ( : {posnum K})
    of (\forall \near F, `|f x| <= k%:num * `|g x|) :
      bigO_spec F g f.

Lemma ( : filter_on T) ( : T -> W) ( : {O_F g}) : bigO_spec F g f.

Proof.

by have /bigO_exP [_/posnumP[k] kP] := bigOP f; exists k. Qed.

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

Proof.

have := bigOP [bigO of df]; apply: filter_app; near=> k.
by apply: filter_app; near=> x; rewrite normrN.
Unshelve. all: by end_near. Qed.

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

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

Proof.

by rewrite [RHS]bigOE. Qed.

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

Proof.

by move: x; rewrite -/(- _ =1 _) {1}oppO. Qed.

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

Proof.

near=> k; near=> x; apply: le_trans (ler_normD _ _) _.
by rewrite (splitr k) mulrDl lerD //; near: x; near: k;
[apply: near_pinfty_div2 (bigOP df)|apply: near_pinfty_div2 (bigOP dg)].
Unshelve. all: by end_near. Qed.

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

Lemma ( : filter_on T) ( : T -> V) :
  [O_F e of f] + [O_F e of g] =O_F e.

Proof.

by rewrite [RHS]bigOE. Qed.

Lemma ( : filter_on T) ( : T -> V) :
[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.

Proof.

by move: x; rewrite -/(_ + _ =1 _) {1}addO. Qed.

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

Proof.

rewrite /the_bigO /insubd=> ->.
case: insubP => /= [u /asboolP fg_o_e ->|_].
by rewrite -addrA subrKC; apply: fg_o_e.
by rewrite addrC addKr; apply: bigOP.
Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(f = g +O_ F e) <-> (bigO_def F (f - g) e).

Proof.

by split=> [/eqadd_some_OP|fg_O_e]; rewrite ?bigOE // addrC addrNK. Qed.

Lemma ( : filter_on T) ( : T -> W) ( : T -> V) :
(f =O_ F e) <-> (bigO_def F f e).

Proof.

by rewrite -[f]subr0 -eqaddOP -[f \- 0]/(f - 0) subr0 add0r. Qed.

Lemma ( : filter_on T) ( : T -> W) ( : T -> V) :
(f =O_ F e) <-> (bigO_ex_def F f e).

Proof.

apply: iff_trans (iff_sym (bigO_exP _ _ _)); apply: eqOP. Qed.

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

Proof.

by have := @eqadd_some_OP F f 0 e h; rewrite add0r subr0. Qed.

Lemma ( : filter_on T) ( : T -> W) ( : {O_F g}) :
(f : _ -> _) =O_F g.

Proof.

by apply/eqOP; apply: bigOP. Qed.

Lemma ( : filter_on T) ( : T -> W) ( : T -> V) :
f =O_ F e -> bigO_def F f e.

Proof.

by rewrite eqOP. Qed.

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

Proof.

by move=> /eqadd_some_OP /eqaddOP. Qed.

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

Proof.

by move=> /eq_some_OP /eqOP. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(forall , f x = mkbigO a_tag F h e x) ->
(forall , f x =O_( \near F) e x).

Proof.

by have := @eqOE F f h e; rewrite !funeqE. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
(forall , f x = g x + mkbigO a_tag F h e x) ->
(forall , f x = g x +O_( \near F) (e x)).

Proof.

by have := @eqaddOE F f g h e; rewrite !funeqE. Qed.

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

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
[o_F e of f] =O_F e.

Proof.

by apply/eqOP; exists 0; split => // k kgt0; apply: littleoP. Qed.

Hint Resolve eqoO : core.

Notation := (littleo_type F f).

Lemma ( : filter_on T) ( : T -> W) ( : {o_F e}) :
(f : _ -> _) =O_F e.

Proof.

by apply: eqOE; rewrite littleo_eqo. Qed.

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

End Domination_numFieldType.

Notation := (@littleo_type _ _ _ _ F f).
Notation := (@bigO_type _ _ _ _ F f).

Notation :=
  (@littleo_clone _ _ _ _ _ _ f fT _ idfun).
Notation := (@littleo_clone _ _ _ _ _ _ f _ _ idfun).

Notation := (@bigO_clone _ _ _ _ _ _ f fT _ idfun).
Notation := (@bigO_clone _ _ _ _ _ _ f _ _ idfun).

Arguments the_littleo {_ _ _ _} _ _ _ _ _ : simpl never.
Arguments the_bigO {_ _ _ _} _ _ _ _ _ : simpl never.
Local Notation x := (Phantom _ (nbhs x)).

Notation tag x := (the_littleo tag _ (PhantomF x)).
Notation := (mklittleo gen_tag x f e).
Notation :=
  (mklittleo gen_tag F (fun => f) (fun => e) x).
Notation := (the_littleo _ _ (PhantomF x) _).
Notation := (the_littleo _ _ _ _).
Notation :=
  (the_littleo _ _ (PhantomF F) (fun => f) (fun => e) x).
Notation := (the_littleo _ _ (Phantom _ x) f e).
Notation := (the_littleo the_tag _ (Phantom _ x) _ e).
Notation := (the_littleo a_tag _ (Phantom _ x) _ e).
Notation := (the_littleo gen_tag _ (Phantom _ x) _).

Notation :=
  (the_littleo the_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_littleo a_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_littleo gen_tag _ (PhantomF F) _ (fun => e) x).

Notation tag x := (the_bigO tag _ (PhantomF x)).
Notation := (mkbigO gen_tag x f e).
Notation :=
  (mkbigO gen_tag F (fun => f) (fun => e) x).
Notation := (the_bigO _ _ (PhantomF x) _).
Notation := (the_bigO _ _ _ _).
Notation := (the_bigO _ _ (Phantom _ x) f e).
Notation :=
  (the_bigO _ _ (PhantomF F) (fun => f) (fun => e) x).
Notation := (the_bigO the_tag _ (Phantom _ x) _ e).
Notation := (the_bigO a_tag _ (Phantom _ x) _ e).
Notation := (the_bigO gen_tag _ (Phantom _ x) _).

Notation :=
  (the_bigO the_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_bigO a_tag _ (PhantomF F) _ (fun => e) x).
Notation :=
  (the_bigO gen_tag _ (PhantomF F) _ (fun => e) x).

Notation :=
  (f%function = g%function + mklittleo the_tag F (f \- g) h).
Notation := (f%function = (mklittleo the_tag F f h)).
Notation :=
  (f%function == g%function + mklittleo the_tag F (f \- g) h).
Notation := (f%function == (mklittleo the_tag F f h)).
Notation :=
  (fx = gx + mklittleo the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx = (mklittleo the_tag F (fun => fx) (fun => hx) x)).
Notation :=
  (fx == gx + mklittleo the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx == (mklittleo the_tag F (fun => fx) (fun => hx) x)).

Notation :=
  (f%function = g%function + mkbigO the_tag F (f \- g) h).
Notation := (f%function = mkbigO the_tag F f h).
Notation :=
  (f%function == g%function + mkbigO the_tag F (f \- g) h).
Notation := (f%function == mkbigO the_tag F f h).
Notation :=
  (fx = gx + mkbigO the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx = (mkbigO the_tag F (fun => fx) (fun => hx) x)).
Notation :=
  (fx == gx + mkbigO the_tag F
                  ((fun => fx) \- (fun => gx%R)) (fun => hx) x).
Notation :=
  (fx == (mkbigO the_tag F (fun => fx) (fun => hx) x)).

#[global] Hint Extern 0 (_ = the_littleo the_tag _ _ _ _) =>
  apply: eqoE; reflexivity : core.
#[global] Hint Extern 0 (_ = the_bigO the_tag _ _ _ _) =>
  apply: eqOE; reflexivity : core.
#[global] Hint Extern 0 (_ = the_bigO the_tag _ _ _ _) =>
  apply: eqoO; reflexivity : core.
#[global] Hint Extern 0 (_ = _ + the_littleo the_tag _ _ _ _) =>
  apply: eqaddoE; reflexivity : core.
#[global] Hint Extern 0 (_ = _ + the_bigO the_tag _ _ _ _) =>
  apply: eqaddOE; reflexivity : core.
#[global] Hint Extern 0 (\forall \near +oo, \forall \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 (forall , is_true (0 < e) -> \forall \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 { : numFieldType} { : Type} { : normedModType K}.

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  forall , 0 < eps -> \forall \near F, `|f x| <= eps * `|g x|.

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

Proof.

by move=> _/posnumP[eps]; near do [
rewrite [eps%:num]splitr mulrDl (le_trans (ler_normD _ _)) // lerD //];
apply: littleoP.
Unshelve. all: by end_near. Qed.

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

Lemma ( : filter_on T) ( : T -> V) ( : _ -> W) :
  [o_F e of f] + [o_F e of g] =o_F e.

Proof.

by rewrite [RHS]littleoE. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : _ -> W) :
[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.

Proof.

by move: x; rewrite -/(_ + _ =1 _) {1}addo. Qed.

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

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

Proof.

have [->|a0] := eqVneq a 0; first by rewrite scale0r.
move=> _ /posnumP[eps]; have aa := normr_eq0 a; near=> x => /=.
rewrite normrZ -ler_pdivlMl ?lt_def ?aa ?a0 //= mulrA; near: x.
by apply: littleoP; rewrite mulr_gt0 // invr_gt0 ?lt_def ?aa ?a0 /=.
Unshelve. all: by end_near. Qed.

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

Lemma ( : filter_on T) ( : T -> V) ( : _ -> W) :
a *: [o_F e of f] = [o_F e of a *: [o_F e of f]].

Proof.

by rewrite [RHS]littleoE. Qed.

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

Proof.

by move: x; rewrite -/(_ *: _ =1 _) {1}scaleo. Qed.

End Domination_numFieldType.

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

Proof.

rewrite [in RHS]littleoE //.
have [->|a0] := eqVneq a 0.
by move=> ??; apply: filterE => ?; rewrite scaler0 normr0 pmulr_rge0.
move=> _/posnumP[eps].
have ea : 0 < eps%:num / `| a | by rewrite divr_gt0 // normr_gt0.
have [g /(_ _ ea) ?] := littleo; near=> y.
rewrite normrZ -ler_pdivlMr; last by rewrite mulrAC; near: y.
by rewrite lt_def normr_eq0 a0 normr_ge0.
Unshelve. all: by end_near. Qed.

Section Limit.
Context { : numFieldType} { : Type} { : normedModType K}.

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

Proof.

split=> fFl.
  apply/eqaddoP => _/posnumP[eps]; near do rewrite /cst ltW//.
  by apply: cvgr_distC_lt; rewrite // mulr_gt0 // normr1.
apply/cvgrPdist_lt=> _/posnumP[eps].
have lt_eps x : x <= (eps%:num / 2%:R) * `|1 : K^o|%real -> x < eps%:num.
  rewrite normr1 mulr1 => /le_lt_trans; apply.
  by rewrite ltr_pdivrMr // ltr_pMr // ltr1n.
near=> x do rewrite [X in X x]fFl opprD addNKr normrN lt_eps //.
by apply: littleoP; rewrite divr_gt0.
Unshelve. all: by end_near. Qed.

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

Proof.

by move=> /eqaddoE /eqolimP. Qed.

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

Proof.

by rewrite eqolimP add0r -[f \- cst 0]/(f - 0) subr0. Qed.

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

Proof.

by move=> /eqoE /eqolim0P. Qed.

Lemma { : filter_on T}
( : T -> W) ( : T -> V) ( : T -> X) :
f =O_F g -> [o_F f of h] =o_F g.

Proof.

move->; apply/eqoP => _/posnumP[e]; have [k c] := bigO _ g.
apply: filter_app; near=> x do [
rewrite -!ler_pdivrMl//; apply: le_trans; rewrite ler_pdivrMl// mulrA].
exact: littleoP.
Unshelve. all: by end_near. Qed.

Arguments littleo_bigO_eqo {F}.

Lemma { : filter_on T} ( : T -> W) ( : T -> V) ( : T -> X) :
f =o_F g -> [O_F f of h] =o_F g.

Proof.

move->; apply/eqoP => _/posnumP[e]; have [k c] := bigO.
apply: filter_app; near=> x => /le_trans; apply.
by rewrite -ler_pdivlMl // mulrA; near: x; apply: littleoP.
Unshelve. all: by end_near. Qed.

Arguments bigO_littleo_eqo {F}.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =o_F e -> g =o_F e -> f + g =o_F e.

Proof.

by move=> -> ->; rewrite addo. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =o_F e -> f + [o_F e of h] =o_F e.

Proof.

by move->; rewrite addo. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =o_F e -> - f =o_F e.

Proof.

by move->; rewrite oppo. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =O_F e -> g =O_F e -> f + g =O_F e.

Proof.

by move=> -> ->; rewrite addO. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =O_F e -> f + [O_F e of h] =O_F e.

Proof.

by move->; rewrite addO. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) :
f =O_F e -> - f =O_F e.

Proof.

by move->; rewrite oppO. Qed.

Lemma ( : filter_on T) ( : T -> W) : e =O_F e.

Proof.

by apply/eqO_exP; exists 1 => //; apply: filterE=> x; rewrite mul1r. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) ( : T -> X) :
f =o_F g -> [o_F f of h] =o_F g.

Proof.

by move=> ->; apply: eqoE; rewrite (littleo_bigO_eqo g). Qed.

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 { : realFieldType}
{ : Type} { : normedModType K}.

Lemma { : filter_on T} ( : T -> W) ( : T -> V) ( : T -> X) :
f =O_F g -> ([O_F f of h] : _ -> _) =O_F g.

Proof.

move->; apply/eqOP; have [k c1 kOg] := bigO _ g. have [k' c2 k'Ok] := bigO _ k.
near=> c; move: k'Ok kOg; apply: filter_app2; near=> x => lek'c2k.
rewrite -(@ler_pM2l _ c2%:num) // mulrA => /(le_trans lek'c2k) /le_trans.
by apply; rewrite ler_pM//; near: c; exact: nbhs_pinfty_ge.
Unshelve. all: by end_near. Qed.

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 { : numFieldType} { : Type} { : normedModType K}.

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

Proof.

by move=> -> ->; rewrite -addrA addo. Qed.

End littleo_bigO_transitivity.

Section littleo_bigO_transitivity.
Context { : numFieldType} { : Type} { : normedModType K}.

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

Proof.

by move=> -> ->; rewrite -addrA addO. Qed.

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

Proof.

by move=> -> ->; rewrite addrAC -addrA addfO. Qed.

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

Proof.

by move=> -> ->; rewrite -addrA addfO. Qed.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) ( : T -> Z) :
f = [o_F g of f'] -> g = [o_F h of g'] -> f =o_F h.

Proof.

by move=> -> ->; rewrite (littleo_bigO_eqo h). Qed.

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

Proof.

by move=> -> ->; rewrite (bigO_littleo_eqo h). Qed.

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

Proof.

by move=> -> ->; rewrite (littleo_bigO_eqo h). Qed.

End littleo_bigO_transitivity.

Section littleo_bigO_transitivity_realFieldType.
Context { : realFieldType} { : Type}
{ : normedModType K}.

Lemma ( : filter_on T) ( : T -> V) ( : T -> W) ( : T -> Z) :
f = [O_F g of f'] -> g = [O_F h of g'] -> f =O_F h.

Proof.

by move=> -> ->; rewrite (bigO_bigO_eqO h). Qed.

End littleo_bigO_transitivity_realFieldType.

Section rule_of_products_rcfType.

Variables ( : rcfType) ( : pointedType).

Lemma ( : filter_on pT) ( : pT -> R^o) :
[o_F h1 of f] * [o_F h2 of g] =o_F (h1 * h2).

Proof.

rewrite [in RHS]littleoE // => _/posnumP[e]; near=> x.
rewrite [`|_|]normrM -(sqr_sqrtr (ge0 e)) expr2.
rewrite (@normrM _ (h1 x) (h2 x)) mulrACA ler_pM //; near: x;
by have [/= h] := littleo; apply.
Unshelve. all: by end_near. Qed.

Lemma ( : filter_on pT) ( : pT -> R^o) :
[O_F h1 of f] * [O_F h2 of g] =O_F (h1 * h2).

Proof.

rewrite [RHS]bigOE//; have [ O1 k1 Oh1] := bigO; have [ O2 k2 Oh2] := bigO.
near=> k; move: Oh1 Oh2; apply: filter_app2; near=> x => leOh1 leOh2.
rewrite [`|_|]normrM (le_trans (ler_pM _ _ leOh1 leOh2)) //.
by rewrite mulrACA [`|_| in leRHS]normrM ler_wpM2r // ?mulr_ge0.
Unshelve. all: by end_near. Qed.

End rule_of_products_rcfType.

Section rule_of_products_numClosedFieldType.

Variables ( : numClosedFieldType) ( : pointedType).

Lemma ( : filter_on pT) ( : pT -> R^o) :
[o_F h1 of f] * [o_F h2 of g] =o_F (h1 * h2).

Proof.

rewrite [in RHS]littleoE // => _/posnumP[e]; near=> x.
rewrite [`|_|]normrM -(sqrCK (ge0 e)) expr2 sqrtCM ?qualifE//=.
rewrite (@normrM _ (h1 x) (h2 x)) mulrACA ler_pM //; near: x;
by have [/= h] := littleo; apply.
Unshelve. all: by end_near. Qed.

Lemma ( : filter_on pT) ( : pT -> R^o) :
[O_F h1 of f] * [O_F h2 of g] =O_F (h1 * h2).

Proof.

End rule_of_products_numClosedFieldType.

Section Linear3.
Context ( : realFieldType) ( : normedModType R) ( : normedModType R)
( : GRing.Scale.law R V).
Hypothesis ( : forall , `|s k x| = `|k| * `|x|).

Local Notation := (@pinfty_nbhs R).

Lemma ( : {linear U -> V | GRing.Scale.Law.sort s}) :
(f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.

Proof.

move=> /eqO_exP [_/posnumP[k0] Of1] x.
apply/cvgrPdist_lt => _/posnumP[e]; rewrite !near_simpl.
rewrite (near_shift 0) /= subr0; near=> y => /=.
rewrite -linearB opprD addrC addrNK linearN normrN; near: y.
suff flip : \forall \near +oo, forall , `|f x| <= k * `|x|.
  near +oo => k; near=> y.
  rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivlMl.
    by near: k; exists 0.
  near: y; apply/nbhs_normP.
  eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
  by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0.
have /nbhs_normP [_/posnumP[d]] := Of1.
rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
case: (ler0P `|y|) => [|y0].
  by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
have ky0 : 0 <= k0%:num / (k * `|y|).
  by rewrite pmulr_rge0 // invr_ge0 mulr_ge0 // ltW //; near: k; exists 0.
rewrite -[leRHS]mulr1 -ler_pdivrMl ?pmulr_rgt0 //.
rewrite -(ler_pM2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
rewrite -normm_s.
rewrite -linearZ fk //= /= distrC subr0 normrZ ger0_norm //.
rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivrMr //.
by rewrite -ltr_pdivrMl//.
Unshelve. all: by end_near. Qed.

End Linear3.

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

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

Proof.

by apply: linear_for_continuous => ? ?; rewrite normrZ. Qed.

Lemma ( : realFieldType) ( : normedModType R)
( : {linear U -> R^o | @GRing.mul R^o}) :
(f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.

Proof.

by apply: linear_for_continuous => ? ?; rewrite normrZ. Qed.

Notation := (f = g +o_ F g).
Notation := (f == g +o_ F g).

Section asymptotic_equivalence.

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

Lemma ( : T -> V) : f ~_F g -> f =O_F g.

Proof.

by move=> ->; apply: eqOE; rewrite {1}[g](idO F) addrC addfO. Qed.

Lemma ( : T -> V) : f ~_F f.

Proof.

by apply/eqaddoP; rewrite subrr. Qed.

Lemma ( : normedModType K) ( : T -> V) ( : T -> W') :
f ~_F g -> [o_F g of h] =o_F f.

Proof.

move=> ->; apply/eqoP; move=> _/posnumP[eps]; near=> x.
rewrite -ler_pdivrMl // -[X in g + X]opprK oppo.
rewrite (le_trans _ (ler_dist_dist _ _)) //.
rewrite [leRHS]ger0_norm ?lerBrDr ?add0r.
by rewrite -[leRHS]mul1r; near: x; apply: littleoP.
rewrite [leRHS]splitr [_ / 2]mulrC.
by rewrite lerD ?ler_pdivrMl ?mulrA //; near: x; apply: littleoP.
Unshelve. all: by end_near. Qed.

Lemma ( : T -> V) : f ~_F g -> g ~_F f.

Proof.

move=> fg; have /(canLR (addrK _))<- := fg.
by apply:eqaddoE; rewrite oppo (equivoRL _ fg).
Qed.

Lemma ( : normedModType K) ( : T -> V) ( : T -> W') :
f ~_F g -> [o_F f of h] =o_F g.

Proof.

by move/equiv_sym/equivoRL. Qed.

Lemma ( : T -> V) : f ~_F g -> g =O_F f.

Proof.

by move/equiv_sym/equivOLR. Qed.

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

Proof.

by apply: equivoLR. Qed.

Lemma ( : T -> V) : f ~_F g -> g ~_F h -> f ~_F h.

Proof.

by move=> -> ->; apply: eqaddoE; rewrite eqoaddo -addrA addo. Qed.

Lemma :
equivalence_rel [rel : T -> V | f ~~_F g].

Proof.

move=> f g h; split; first by apply/eqP/equiv_refl.
by move=> /eqP fg /=; apply/eqP/eqP; apply/equiv_trans => //; apply/equiv_sym.
Qed.

End asymptotic_equivalence.

Section big_omega.

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

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  exists2 , k > 0 & \forall \near F, `|f x| >= k * `|g x|.

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

Notation := (@bigOmega_type _ F g).

. ( T) (g : T -> W) :=
  [isSub for @bigOmega_fun W F g].

Lemma {} ( : set_system T) ( : T -> W) ( : {Omega_F g}) :
  `[< bigOmega_def F f g >].

Proof.

by case: f => ?. Qed.

Hint Resolve bigOmega_class : core.

Definition {} ( : set_system T) ( : T -> W) ( : T -> V)
( : {Omega_F g}) & phant_id (bigOmega_class fT) c := @BigOmega W F g f c.
Notation := (@bigOmega_clone _ _ _ f fT _ idfun).
Notation := (@bigOmega_clone _ _ _ f _ _ idfun).

Lemma ( : T -> V) : Filter F -> bigOmega_def F g g.

Proof.

by move=> FF; exists 1 => //; near=> x; rewrite mul1r.
Unshelve. all: by end_near. Qed.

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

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

Notation tag x := (the_bigOmega tag _ (PhantomF x)).
Notation := (mkbigOmega gen_tag x f e).
Notation := (the_bigOmega _ _ (PhantomF x) f e).

Definition {} ( : set_system T) ( : T -> W) :=
  [qualify : T -> V | `[< bigOmega_def F f g >] ].
Fact {} ( : set_system T) ( : T -> W) : pred_key (is_bigOmega F g).

Proof.

by []. Qed.

Canonical {} ( : set_system T) ( : T -> W) :=
KeyedQualifier (is_bigOmega_key F g).
Notation := (is_bigOmega F g).

Lemma {} ( : set_system T) ( : T -> W) ( : {Omega_F g}) :
bigOmega_def F f g.

Proof.

exact/asboolP. Qed.

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%function = mkbigOmega the_tag F f h).

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

Variant {} ( : set_system T) ( : T -> W) : (T -> V) -> Prop :=
   ( : {posnum K}) of
    (\forall \near F, `|f x| >= k%:num * `|g x|) :
  bigOmega_spec F g f.

Lemma {} ( : filter_on T) ( : T -> W) ( : {Omega_F g}) :
  bigOmega_spec F g f.

Proof.

by have [_/posnumP[k]] := bigOmegaP f; exists k. Qed.

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

Proof.

rewrite propeqE; split => [| /eqO_exP[x x0 Hx] ];
[rewrite qualifE => /asboolP[x x0 Hx]; apply/eqO_exP |
rewrite qualifE; apply/asboolP];
exists x^-1; rewrite ?invr_gt0 //; near=> y.
by rewrite ler_pdivlMl //; near: y.
by rewrite ler_pdivrMl //; near: y.
Unshelve. all: by end_near. Qed.

Lemma ( : filter_on T) ( : T -> V) :
(f =Omega_F(e)) = (f \is 'Omega_F(e)).

Proof.

rewrite propeqE; split=> [->|]; rewrite qualifE; last first.
by move=> H; rewrite /the_bigOmega val_insubd H.
by apply/asboolP; rewrite /the_bigOmega val_insubd; case: ifPn => // /asboolP.
Qed.

Lemma ( : filter_on T) ( : T -> V) :
f =Omega_F(g) -> g =Omega_F(h) -> f =Omega_F(h).

Proof.

rewrite !eqOmegaE !eqOmegaO => fg gh; exact: (eqO_trans gh fg). Qed.

End big_omega.

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

Section big_omega_in_R.

Variable : pointedType.

Lemma ( : realFieldType) ( : filter_on pT) ( : _ -> R^o)
( : forall , 0 <= f x) ( : forall , 0 <= g x) :
f =Omega_F h -> f + g =Omega_F h.

Proof.

rewrite 2!eqOmegaE !eqOmegaO => /eqOP hOf; apply/eqOP.
apply: filter_app hOf; near=> k; apply: filter_app; near=> x => /le_trans.
by apply; rewrite ler_pM2l // !ger0_norm // ?addr_ge0 // lerDl.
Unshelve. all: by end_near. Qed.

Lemma ( : realFieldType) ( : filter_on pT) ( : pT -> R^o) :
[Omega_F h1 of f] * [Omega_F h2 of g] =Omega_F (h1 * h2).

Proof.

rewrite eqOmegaE eqOmegaO [in RHS]bigOE //.
have [W1 k1 ?] := bigOmega; have [W2 k2 ?] := bigOmega.
near=> k; near=> x; rewrite [`|_|]normrM.
rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //.
  rewrite invfM -mulrA ler_pdivlMl// ler_pdivlMl//.
  rewrite (mulrCA k2%:num) (mulrA k1%:num) (@normrM _ (W1 x)).
  by rewrite ler_pM ?mulr_ge0 //; near: x.
by rewrite ler_wpM2r // ltW //.
Unshelve. all: by end_near. Qed.

End big_omega_in_R.

Section big_theta.

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

Let ( : set_system T) ( : T -> V) ( : T -> W) :=
  exists2 , (k.1 > 0) && (k.2 > 0) &
  \forall \near F, k.1 * `|g x| <= `|f x| /\ `|f x| <= k.2 * `|g x|.

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

Notation := (@bigTheta_type _ F g).

. ( T) (g : T -> W) :=
  [isSub for @bigTheta_fun W F g].

Lemma {} ( : set_system T) ( : T -> W) ( : {Theta_F g}) :
  `[< bigTheta_def F f g >].

Proof.

by case: f => ?. Qed.

Hint Resolve bigTheta_class : core.

Definition {} ( : set_system T) ( : T -> W) ( : T -> V)
( : {Theta_F g}) & phant_id (bigTheta_class fT) c := @BigTheta W F g f c.
Notation := (@bigTheta_clone _ _ _ f fT _ idfun).
Notation := (@bigTheta_clone _ _ _ f _ _ idfun).

Lemma ( : T -> V) : Filter F -> bigTheta_def F g g.

Proof.

by move=> FF; exists 1 => /=; rewrite ?ltr01 //; near=> x; by rewrite mul1r.
Unshelve. all: by end_near. Qed.

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

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

Notation tag x := (@the_bigTheta tag _ (PhantomF x)).
Notation := (mkbigTheta gen_tag x f e).
Notation := (the_bigTheta _ _ (PhantomF x) f e).

Definition {} ( : set_system T) ( : T -> W) :=
  [qualify : T -> V | `[< bigTheta_def F f g >] ].
Fact {} ( : set_system T) ( : T -> W) : pred_key (is_bigTheta F g).

Proof.

by []. Qed.

Canonical {} ( : set_system T) ( : T -> W) :=
KeyedQualifier (is_bigTheta_key F g).
Notation := (@is_bigTheta _ F g).

Lemma {} ( : set_system T) ( : T -> W) ( : {Theta_F g}) :
bigTheta_def F f g.

Proof.

exact/asboolP. Qed.

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 ( : unit) ( : filter_on T)
  ( : phantom (set_system T) F) := [bigTheta of @the_bigTheta tag F phF f h].

Variant {} ( : set_system T) ( : T -> W) : (T -> V) -> Prop :=
     ( : {posnum K}) ( : {posnum K}) of
      (\forall \near F, k1%:num * `|g x| <= `|f x|) &
      (\forall \near F, `|f x| <= k2%:num * `|g x|) :
  bigTheta_spec F g f.

Lemma {} ( : filter_on T) ( : T -> W) ( : {Theta_F g}) :
  bigTheta_spec F g f.

Proof.

have [[_ _] /andP[/posnumP[k] /posnumP[k']]] := bigThetaP f.
by move=> /near_andP[]; exists k k'.
Qed.

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

Lemma {} ( : filter_on T) ( : T -> V) ( : T -> W) :
(f \is 'Theta_F(g)) = (f =O_F g /\ f \is 'Omega_F(g)) :> Prop.

Proof.

rewrite propeqE; split.
- rewrite qualifE => /asboolP[[/= k1 k2] /andP[k10 k20]] /near_andP[Hx1 Hx2].
  by split; [rewrite eqO_exP; exists k2|
    rewrite qualifE; apply/asboolP; exists k1].
- case; rewrite eqO_exP qualifE => -[k1 k10 H1] /asboolP[k2 k20 H2].
  rewrite qualifE; apply/asboolP; exists (k2, k1) => /=; first by rewrite k20.
  by apply/near_andP; split.
Qed.

Lemma ( : filter_on T) ( : T -> V) :
(f =Theta_F(e)) = (f \is 'Theta_F(e)).

Proof.

rewrite propeqE; split=> [->|]; rewrite qualifE; last first.
by move=> H; rewrite /the_bigTheta val_insubd H.
by apply/asboolP; rewrite /the_bigTheta val_insubd; case: ifPn => // /asboolP.
Qed.

Lemma ( : filter_on T) ( : T -> V) : [Theta_F g of f] =O_F g.

Proof.

by have [T1 k1 k2 ? ?] := bigTheta; apply/eqO_exP; exists k2%:num. Qed.

Lemma ( : filter_on T) ( : T -> V) : f =Theta_F f.

Proof.

rewrite eqThetaE bigThetaE eqOmegaO; split; exact/idO. Qed.

Lemma ( : filter_on T) ( : T -> V) :
(f =Theta_F g) = (g =Theta_F f).

Proof.

by rewrite !eqThetaE propeqE !bigThetaE !eqOmegaO; split => -[]. Qed.

Lemma ( : filter_on T) ( : T -> V) :
f =Theta_F g -> g =Theta_F h -> f =Theta_F h.

Proof.

rewrite !eqThetaE !bigThetaE -!eqOmegaE => -[fg gf] [gh hg]; split.
by rewrite fg (bigO_bigO_eqO _ _ _ gh).
exact: (eqOmega_trans gf hg).
Qed.

End big_theta.

Notation := (@bigTheta_type _ F g).
Notation := (@bigTheta_clone _ _ _ _ _ _ f _ _ idfun).
Notation tag x := (the_bigTheta tag (PhantomF x)).
Notation := (mkbigTheta gen_tag x f e).
Notation := (the_bigTheta _ _ (PhantomF x) f e).
Notation := (is_bigTheta F g).
Notation := (f%function = mkbigTheta the_tag F f h).

Section big_theta_in_R.

Variables ( : rcfType ) ( : pointedType).

Lemma ( : filter_on pT) ( : _ -> R^o)
( : forall , 0 <= f x) ( : forall , 0 <= g x) ( : forall , 0 <= h x) :
[Theta_F h of f] + [O_F h of g] =Theta_F h.

Proof.

rewrite eqThetaE bigThetaE; split; first by rewrite eqThetaO addO.
rewrite -eqOmegaE; apply: addOmega.
- by move=> ?; rewrite /the_bigTheta val_insubd /=; case: ifP.
- by move=> ?; rewrite /the_bigO val_insubd /=; case: ifP.
- rewrite eqOmegaE eqOmegaO; have [T1 k1 k2 ? ?] := bigTheta.
rewrite bigOE //; apply/bigO_exP; exists k1%:num^-1 => //.
by near do rewrite ler_pdivlMl //.
Unshelve. all: by end_near. Qed.

Lemma ( : filter_on pT) ( : pT -> R^o) :
[Theta_F h1 of f] * [Theta_F h2 of g] =Theta_F h1 * h2.

Proof.

rewrite eqThetaE bigThetaE; split.
  by rewrite (eqThetaO _ f) (eqThetaO _ g) mulO.
rewrite eqOmegaO [in RHS]bigOE //.
have [T1 k1 l1 P1 ?] := bigTheta; have [T2 k2 l2 P2 ?] := bigTheta.
near=> k; first near=> x.
rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) //.
  rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
  rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pM //;
  by [rewrite mulr_ge0 //|near: x].
by rewrite ler_wpM2r // ltW //.
Unshelve. all: by end_near. Qed.

End big_theta_in_R.

Files

Module mathcomp.analysis.landau