Library BigO

Definition and properties of the mathematical O. f ={x -> 0} O(g) becomes O_P(f,g) with P being conditions on acceptable x

Require Export R_two.

Open Local Scope nat_scope.
Open Local Scope R_scope.

Section BigOuP.

Here is the definition of the O, where dX:R*R -> 0 and which is uniform for X in A (may be an interval, a box,...)

Variable A:Type.

Definition OuP (P: R *R-> Prop) (f: A -> R *R -> R) (g: R * R -> R) :=
  { alp : R & { C : R |
  0 < alp /\ 0 < C /\
  forall X:A, forall dX : R * R,
  norm_l2 dX < alp -> P dX ->
  Rabs (f X dX) <= C * Rabs (g dX)}}.

We then have a vector space

Lemma OuP_is_EV_zero :
  forall P, forall g : R * R -> R,
  OuP P (fun (X:A) dX => 0) g.

Lemma OuP_is_EV_plus :
  forall P f1 f2 g,
  OuP P f1 g -> OuP P f2 g ->
  OuP P (fun a => add2_fun (f1 a) (f2 a)) g.

Lemma OuP_is_EV_mult :
  forall P (f:A -> R *R -> R) g l,
  l <> 0 ->
  OuP P f g ->
  OuP P (fun a:A => scalar_multiplyA_fun _ l (f a)) g.

Lemma OuP_is_EV_mult_z :
  forall P (f:A -> R *R -> R) g l,
  OuP P f g ->
  OuP P (fun a:A => scalar_multiplyA_fun _ l (f a)) g.

Many other properties

Lemma OuP_multiplyAA :
  forall P (f:A-> R *R->R) g l,
  l<> 0 ->
  OuP P f g ->
  OuP P (scalar_multiplyAA_fun _ _ l f) g.

Lemma OuP_multiplyAA_z :
  forall P (f:A-> R *R->R) g l,
  OuP P f g ->
  OuP P (scalar_multiplyAA_fun _ _ l f) g.

Lemma OuP_maj:
  forall (P:R *R -> Prop) f1 f2 g,
  (forall (X:A) (dX : R * R), P dX -> Rabs (f1 X dX) <= Rabs (f2 X dX)) ->
  OuP P f2 g ->
  OuP P f1 g.

Lemma OuP_inclusion :
  forall (P:R *R -> Prop) f g1 g2,
  (forall X : R * R, norm_l2 X <= 1 -> P X -> Rabs (g1 X) <= Rabs (g2 X)) ->
  OuP P f g1 ->
  OuP P f g2.

Lemma OuP_sum_ortho :
  forall P f1 f2, forall m k : nat,
  OuP P f1 (fun X => Rabs (fst X) ^ m) ->
  OuP P f2 (fun X => Rabs (snd X) ^ k) ->
  OuP P (fun a => add2_fun (f1 a) (f2 a))
            (fun X => Rabs (fst X) ^ m + Rabs (snd X) ^ k).

Lemma OuP_division :
  forall P f g1 g2,
  OuP P f g1 ->
  OuP P (fun a => divide2_fun (f a) g2) (divide2_fun g1 g2).

Lemma OuP_eq_trans_l :
  forall P:R *R-> Prop, forall f1 f2 g,
  (forall a dX, P dX -> f1 a dX = f2 a dX) ->
  OuP P f1 g-> OuP P f2 g.

Lemma OuP_eq_trans_r :
  forall (P:R *R-> Prop) f g1 g2,
  (forall dX : R * R, P dX -> g1 dX = g2 dX) ->
  OuP P f g1-> OuP P f g2.

Lemma OuP_implies_OuP: forall P1 P2: R *R -> Prop, forall f g,
  (forall dX, P2 dX -> P1 dX ) ->
  OuP P1 f g -> OuP P2 f g.

Lemma OuP_implies_OuP1: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> P (fst dX,0)) ->
  OuP P f g -> OuP P (fun X dX => f X (fst dX,0)) (fun dX => g (fst dX,0)).

Lemma OuP_implies_OuP2: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> P (0, snd dX)) ->
  OuP P f g -> OuP P (fun X dX => f X (0, snd dX)) (fun dX => g (0,snd dX)).

Lemma OuP_implies_OuPMinus:
forall P:R *R-> Prop, forall f g,
  (forall dX, P dX -> P (-fst dX, -snd dX)) ->
  OuP P f g -> OuP P (fun X dX => f X (-fst dX, -snd dX)) (fun dX => g (-fst dX, -snd dX)).

Lemma OuP_multiply1: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> fst dX <> 0) ->
  OuP P (fun X dX => (fst dX) * f X dX)
      (fun dX => (fst dX) * g dX)
    -> OuP P f g.

Lemma OuP_multiply2: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> snd dX <> 0) ->
  OuP P (fun X dX => (snd dX) * f X dX)
      (fun dX => (snd dX) * g dX)
    -> OuP P f g.

Lemma OuP_divide1: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> fst dX <> 0) ->
  OuP P (fun X dX => / (fst dX) * f X dX)
      (fun dX => / (fst dX) * g dX)
    -> OuP P f g.

Lemma OuP_divide2: forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> snd dX <> 0) ->
  OuP P (fun X dX => / (snd dX) * f X dX)
      (fun dX => / (snd dX) * g dX)
    -> OuP P f g.

Lemma OuP_dX_to_eps: forall P:R *R -> Prop, forall f g eps,
{ C:R | 0 < C /\ (forall X dX, norm_l2 (eps X dX) <= C * norm_l2 dX)} ->
{ C:R | 0 < C /\ (forall X dX, Rabs (g (eps X dX)) <= C * Rabs (g dX))} ->
(forall X dX, P dX -> P (eps X dX)) ->
OuP P f g -> OuP P (fun X dX => f X (eps X dX)) g.

Lemma OuP_X_to_appr: forall P:R *R -> Prop, forall f g appr,
OuP P f g -> OuP P (fun X dX => f (appr X dX) dX) g.

Lemma OuP_snddX_to_dX: forall P:R *R -> Prop, forall h g,
    (forall dX, P dX -> P (0, snd dX))
   -> OuP P h g
   -> OuP P (fun X dX => h X (0,snd dX)) (fun dX => g (0,snd dX)).

Lemma OuP_sqrt : forall P:R *R -> Prop, forall f g,
  (forall X dX, P dX -> 0 <= f X dX) ->
  OuP P f (fun X => Rsqr (g X)) -> OuP P (fun X dX => sqrt (f X dX)) g.

Lemma OuP_Rsqr : forall P:R *R -> Prop, forall f g,
  (forall dX, P dX -> 0 <= g dX) ->
  OuP P f (fun dX => sqrt (g dX)) -> OuP P (fun X dX => Rsqr (f X dX)) g.

Lemma OuP_match : forall P i f0 f1 g,
  OuP P f0 g ->
  OuP P (fun X dX => f1 (S (pred (i X dX))) X dX) g ->
  OuP P (fun X dX => match (i X dX) with
     | 0%nat => f0 X dX
     | (S n) => f1 (S n) X dX
    end)
  g.

Lemma OuP_Rabs: forall P f g,
  OuP P f g -> OuP P (fun x dx => Rabs (f x dx)) g.

Lemma OuP_case: forall (P:R *R-> Prop) f f1 f2 g,
(forall X dX, (P dX) -> (f X dX = f1 X dX) \/ (f X dX = f2 X dX)) ->
  OuP P f1 g -> OuP P f2 g ->
  OuP P f g.

End BigOuP.

Section BigOuP2.

Lemma OuP_X_to_appr_fst: forall A, forall P:R *R -> Prop, forall h g (appr: A*R -> R *R-> A*R),
  (forall x dX, snd (appr (x,0) dX) = 0)
   -> OuP P (fun (x:A) dX => h (x,0) dX) g
   -> OuP P (fun (X:A*R) dX => h (appr (fst X, 0) dX) dX) g.

Lemma OuP_X_to_x: forall A, forall P:R *R -> Prop, forall h g,
      OuP P (fun (X:A*R) dX => h (fst X) dX) g
   -> OuP P (fun x dX => h x dX) g.

End BigOuP2.

Now, we consider for A the interval between 0 and T

Definition Under (T:R) := fun (r:R) => (0 <= r <= T)%R.

Lemma OuP_sum_f: forall (P:R *R-> Prop) (T:R) f g,
   0 < T
-> (forall dX, P dX -> (0 < snd dX)%R)
-> OuP P (fun (t: {t| Under T t}) dX => f dX (kt (projT1 t) (snd dX))) g
-> OuP P (fun (t: {t | Under T t}) dX => snd dX *
            sum_f 1 (kt (projT1 t) (snd dX)) (fun n : nat => f dX n)) g.

Lemma OuP_sum_f_minus1_bis: forall (P:R *R-> Prop) (T:R) f g,
   0 < T
-> (forall dX, P dX -> (0 < snd dX)%R)
-> OuP P (fun (t: {t| Under T t}) dX => f dX (kt (projT1 t) (snd dX))) g
-> OuP P (fun (t: {t | Under T t}) dX => snd dX *
            sum_f 1 (kt (projT1 t) (snd dX)-1) (fun n : nat => f dX (S n))) g.

Lemma OuP_every_implies_OuP_here:
     forall P Q f g,
      OuP P (fun (t:R) (dX:R *R) => f t dX) g
  -> OuP P (fun (t:{t | Q t}) (dX:R *R) => f (projT1 t) dX) g.

Lemma OuP_every_implies_OuP_here_2:
     forall P Q f g,
      OuP P (fun (t:R *R) (dX:R *R) => f t dX) g
  -> OuP P (fun (t:(({x:R | Q x})*R)) (dX:R *R) => f (projT1 (fst t),snd t) dX) g.

Lemma OuP_unit: forall P T f g,
     OuP P (fun (_:unit) dX => f dX) g
  -> OuP P (fun (_:T) dX => f dX) g.

Now, we consider the interval between xmin and xmax

Definition Betw (xmin xmax:R) := fun (r:R) => (xmin <= r <= xmax)%R.

A few notations

Notation Ou := (OuP (fun _ => True)).
Notation Oup := (OuP (fun dX => 0 <= fst dX /\ 0 <= snd dX)).
Notation Oups := (OuP (fun dX => 0 < fst dX /\ 0 < snd dX)).