Library CoqApprox.derive_compl

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and Inria.
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

Require Import Reals.
Require Import Interval_xreal.
Require Import Interval_xreal_derive.
Require Import Interval_missing.
Require Import Interval_generic_proof.
Require Import Rstruct.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop.
Require Import xreal_ssr_compat.
Require Import seq_compl.

Describe the n-th derivatives for several basic functions

Set Implicit Arguments.

Section generic.

Definition nth_derivable_pt (f : R ->R) (Df : nat -> R -> R) x :=
  (forall y, f y = Df 0%nat y) /\
  forall k, derivable_pt_lim (Df k) x (Df (S k) x).

Definition nth_Xderive_pt Xf XDf x :=
  (forall y, Xf y = XDf 0%nat y) /\
  forall k: nat, Xderive_pt (XDf k) x (XDf (S k) x).

End generic.

Section nth_exp.

Lemma nth_derivable_pt_exp x : nth_derivable_pt exp (fun _ => exp) x.

Lemma nth_Xderive_pt_exp x : nth_Xderive_pt Xexp (fun _ => Xexp) x.

End nth_exp.

Section nth_pow.

Lemma nth_derivable_pt_pow n x :
  nth_derivable_pt (fun x => x ^ n)%Re
  (fun k x => \big[Rmult/1]_(i < k) INR (n - i) * x^(n - k))%Re x.

Lemma nth_Xderive_pt_pow n x :
  nth_Xderive_pt (fun x => x ^ n)%XR
  (fun k x => \big[Xmul/Xreal 1]_(i < k) Xreal (INR (n - i)) * x^(n - k))%XR x.

Lemma nth_derivable_pt_inv_pow n x :
  x <> R0 ->
  nth_derivable_pt (fun x => / x ^ n)%Re
  (fun k x => \big[Rmult/1%Re]_(i < k) - INR (n + i) * /x^(n + k))%Re x.

End nth_pow.

Section inverse.

Lemma nth_derivable_pt_inv x :
  x <> R0 ->
  nth_derivable_pt (fun x => / x)%Re
  (fun k x => \big[Rmult/1]_(i < k) - INR (i.+1) * /x^(k.+1))%Re x.

Lemma nth_Xderive_pt_inv x :
  nth_Xderive_pt (fun x => Xinv x)
  (fun k x => ((- Xreal 1) ^ k * Xreal (INR (fact k)) * Xmask (Xreal 1) x /
    x ^ k.+1)%XR) x.

End inverse.

Section power.

Lemma nth_derivable_pt_power a x :
  (0 < x)%Re ->
  nth_derivable_pt (fun x => Rpower x a)
  (fun k x =>
    \big[Rmult/1%Re]_(i < k) (a - INR i) * Rpower x (a - INR k))%Re x.

End power.

Section square_root.


Lemma nth_derivable_pt_sqrt x :
  (0 < x)%Re ->
  nth_derivable_pt sqrt
  (fun k x => match k with 0 => sqrt x | _ =>
  \big[Rmult/1]_(i < k) (/2 - INR i) * Rpower x (/2 - INR k) end)%Re x.

Lemma nth_Xderive_pt_sqrt (x : ExtendedR) :
  nth_Xderive_pt (fun x => Xsqrt x)
  (fun k x => \big[Xmul/Xreal 1]_(i < k) Xreal (/2 - INR i) * ((Xsqrt x)/ x ^ k))%XR x.

Lemma nth_Xderive_pt_invsqrt (x : ExtendedR) :
  nth_Xderive_pt (fun x => Xinv (Xsqrt x))
  (fun k x => \big[Xmul/Xreal 1]_(i < k) Xreal (- / 2 - INR i) *
    (Xinv (Xsqrt x) / x ^ k))%XR x.

End square_root.

Section sin_cos.

Lemma nth_derivable_pt_sin x :
  nth_derivable_pt sin
  (fix dersin k x := match k with 0 => sin x
     | 1 => cos x
     | S (S k') => (-1 * (dersin k' x))%Re
   end) x.

Fixpoint nth_Xsin (k : nat) x :=
  match k with
    | 0 => Xsin x
    | 1 => Xcos x
    | S (S k') => (Xreal (-1) * (nth_Xsin k' x))%XR
  end.

Fixpoint nth_Xcos (k: nat) x :=
  match k with
    | 0 => Xcos x
    | 1 => (- Xsin x)%XR
    | S (S k') => (Xreal (-1) * (nth_Xcos k' x))%XR
  end.

Lemma Xderive_pt_mul_const a f f' x :
  Xderive_pt f x f' ->
  Xderive_pt (fun y => a * f y)%XR x (a * f')%XR.

Lemma nth_Xderive_pt_sin x : nth_Xderive_pt Xsin nth_Xsin x.

Lemma nth_derivable_pt_cos x :
  nth_derivable_pt cos
  (fix dercos k x := match k with 0 => cos x
     | 1 => - sin x
     | S (S k') => -1 * (dercos k' x)
   end)%Re x.

Lemma nth_Xderive_pt_cos x : nth_Xderive_pt Xcos nth_Xcos x.

End sin_cos.

Section cst_var.

Lemma nth_Xderive_pt_cst (cst : ExtendedR) x :
  nth_Xderive_pt (Xmask cst) (fun (n : nat) (y : ExtendedR) =>
    match n with
      | 0 => Xmask cst y
      | n'.+1 => Xmask (Xmask (Xreal 0) cst) y
    end) x.

Lemma nth_Xderive_pt_var x :
  nth_Xderive_pt (fun x => x) (fun (n : nat) (y : ExtendedR) =>
    if n == O then y else
    if n == 1%N then Xmask (Xreal 1) y else
    Xmask (Xreal 0) y) x.

End cst_var.