Library Interval.Real.Taylor

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq:
Copyright (C) 2010-2012, ENS de Lyon. Copyright (C) 2010-2016, Inria. Copyright (C) 2014-2016, IRIT.
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:
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.

From Coq Require Import Reals Psatz.
From Coquelicot Require Import Coquelicot.

Require Import Stdlib.

Local Open Scope R_scope.

Lemma Rolle_lim (f : R R) (a b : R) (h : R R) :
  ( x : R, a < x < b b < x < a derivable_pt_lim f x (h x))
  ( x : R, a x b b x a continuity_pt f x)
  a b
  f a = f b
   c : R, (a < c < b b < c < a) derivable_pt_lim f c 0.

Section TaylorLagrange.

Variables a b : R.
Variable n : nat.

Notation Cab x := (a x b) (only parsing).
Notation Oab x := (a < x < b) (only parsing).

Variable D : nat R R.

Notation Tcoeff n x0 := (D n x0 / (INR (fact n))) (only parsing).

Notation Tterm n x0 x := (Tcoeff n x0 × (x - x0)^n) (only parsing).

Notation Tsum n x0 x := (sum_f_R0 (fun iTterm i x0 x) n) (only parsing).

Lemma continuity_pt_sum (f : nat R R) (x : R) :
  ( k, (k n)%nat continuity_pt (f k) x)
  (fun y ⇒ (sum_f_R0 (fun nf n y) n)) x.

Lemma derivable_pt_lim_sum (f : nat R R) (x : R) (lf : nat R) :
  ( i, (i n)%nat derivable_pt_lim (f i) x (lf i))
  (fun y ⇒ (sum_f_R0 (fun nf n y) n)) x
  (sum_f_R0 lf n).

Section TL.

Hypothesis derivable_pt_lim_Dp :
   k x, (k n)%nat Oab x
  derivable_pt_lim (D k) x (D (S k) x).

Hypothesis continuity_pt_Dp :
   k x, (k n)%nat Cab x
  continuity_pt (D k) x.

Variables x0 x : R.

Define c : R so that the function g : R R below satisfies g(x0)=0.
Let c := (D 0 x - Tsum n x0 x) / (x - x0)^(S n).
Let g := fun yD 0 x - Tsum n y x - c × (x - y)^(S n).

Hypotheses (Hx0 : Cab x0) (Hx : Cab x).

Lemma derivable_pt_lim_aux (y : R) :
  Oab y
  derivable_pt_lim g y (- ((D (S n) y) / (INR (fact n)) × (x - y)^n)
                        + c × (INR (S n)) × (x - y)^n).

Theorem Taylor_Lagrange :
   xi : R,
  D 0 x - Tsum n x0 x =
  Tcoeff (S n) xi × (x - x0)^(S n)
   (x0 x x0 < xi < x x < xi < x0).

End TL.

Section CorTL.

Hypothesis derivable_pt_lim_Dp :
   k x, (k n)%nat Cab x
  derivable_pt_lim (D k) x (D (S k) x).

Theorem Cor_Taylor_Lagrange (x0 x : R) :
  Cab x0 Cab x
  D 0 x - Tsum n x0 x =
  Tcoeff (S n) c × (x - x0)^(S n)
   (x0 x x0 < c < x x < c < x0).

End CorTL.

End TaylorLagrange.