Library Differential

Require Export BigO.
Open Local Scope nat_scope.
Open Local Scope R_scope.

Section Diff.

Variable xmin xmax:R.
Hypothesis xminLtxmax: xmin < xmax.

Definition my_proj (X:({x| Betw xmin xmax x}*R)): R*R := (projT1 (fst X), snd X).

Variable partial_derive_firstvar: (R * R -> R) -> (R * R -> R).
Variable partial_derive_secondvar: (R * R -> R) -> (R * R -> R).

Fixpoint partial_derive_firstvar_n (m : nat) (f : R * R -> R) : R * R -> R :=
  match m with
  | 0 => f
  | S m' => partial_derive_firstvar (partial_derive_firstvar_n m' f)
  end.

Fixpoint partial_derive_secondvar_n (k : nat) (f : R * R -> R) : R * R -> R :=
  match k with
  | 0 => f
  | S k' => partial_derive_secondvar (partial_derive_secondvar_n k' f)
  end.

Definition partial_derive (m k : nat) (f : R * R -> R) : R * R -> R :=
  partial_derive_firstvar_n m (partial_derive_secondvar_n k f).

Definition differential (p : nat) (f : R * R -> R) (X dX : R * R) : R :=
  sum_f_R0
    (fun m =>
      C p m *
      partial_derive m (p - m)%nat f X *
      fst dX ^ m * snd dX ^ (p - m)%nat)
    p.

Definition DL_pol (n : nat) (f : R * R -> R) (X dX : R * R) : R :=
  sum_f_R0
    (fun p =>
      differential p f X dX / INR (fact p))
    n.

Definition is_sufficiently_regular_n m f :=
  Ou (fun X:({x| Betw xmin xmax x}*R) =>
     subtract2_fun
      (fun dX => f (add2 (my_proj X) dX))
      (fun dX => DL_pol (m - 1)%nat f (my_proj X) dX))
    (fun dX => norm_l2 dX ^ m).

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

Lemma DL_discretization_eps_aux: forall f : R * R -> R, forall eps: R * R -> R * R -> R * R,
  (is_sufficiently_regular_n 4 f) ->
  { C : R |
     0 < C /\ (forall (X:({x| Betw xmin xmax x}*R)) (dX : R * R), norm_l2 (eps (my_proj X) dX) <= C * norm_l2 dX)} ->
  Ou ((fun (X:({x| Betw xmin xmax x}*R)) dX => f (add2 (my_proj X) (eps (my_proj X) dX)) - 2*f (my_proj X) + f (subtract2 (my_proj X) (eps (my_proj X) dX))
           - (fst (eps (my_proj X) dX))^2 * (partial_derive_firstvar_n 2 f (my_proj X))
           - (snd (eps (my_proj X) dX))^2 * (partial_derive_secondvar_n 2 f (my_proj X))
           - 2*(fst (eps (my_proj X) dX))*(snd (eps (my_proj X) dX)) * partial_derive_firstvar (partial_derive_secondvar f) (my_proj X)
            ))
     (fun dX => (norm_l2 dX)^4).

Lemma DL_discretization_eps_dx: forall f : R * R -> R,
  (is_sufficiently_regular_n 4 f) ->
  Ou ((fun (X:({x| Betw xmin xmax x}*R)) dX => f (add2 (my_proj X) (fst dX, 0)) - 2*f (my_proj X) + f (subtract2 (my_proj X) (fst dX,0))
           - (fst dX)^2 * (partial_derive_firstvar_n 2 f (my_proj X))))
     (fun dX => (fst dX)^4).

Lemma DL_discretization_eps_dt: forall f : R * R -> R,
  (is_sufficiently_regular_n 4 f) ->
  Ou ((fun (X:({x| Betw xmin xmax x}*R)) dX => f (add2 (my_proj X) (0, snd dX)) - 2*f (my_proj X) + f (subtract2 (my_proj X) (0, snd dX))
           - (snd dX)^2 * (partial_derive_secondvar_n 2 f (my_proj X))))
     (fun dX => (snd dX)^4).

End Diff.