# Library CoqApprox.taylor_thm

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 Psatz.
Require Import Interval_missing.

Local Open Scope R_scope.

Lemma Rolle_lim (f : R -> R) (a b : R) (h : R -> R) :
(forall x : R, a < x < b \/ b < x < a -> derivable_pt_lim f x (h x)) ->
(forall x : R, a <= x <= b \/ b <= x <= a -> continuity_pt f x) ->
a <> b ->
f a = f b ->
exists 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 i => Tterm i x0 x) n) (only parsing).

Lemma continuity_pt_eq (f g : R -> R) :
(forall x : R, f x = g x) ->
forall x, continuity_pt f x -> continuity_pt g x.

Lemma continuity_pt_sum (f : nat -> R -> R) (x : R) :
(forall k, (k <= n)%nat -> continuity_pt (f k) x) ->
continuity_pt
(fun y => (sum_f_R0 (fun n => f n y) n)) x.

Lemma derivable_pt_lim_sum (f : nat -> R -> R) (x : R) (lf : nat -> R) :
(forall i, (i <= n)%nat -> derivable_pt_lim (f i) x (lf i)) ->
derivable_pt_lim
(fun y => (sum_f_R0 (fun n => f n y) n)) x
(sum_f_R0 lf n).

Section TL.

Hypothesis derivable_pt_lim_Dp :
forall k x, (k <= n)%nat -> Oab x ->
derivable_pt_lim (D k) x (D (S k) x).

Hypothesis continuity_pt_Dp :
forall 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 y => D 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 :
exists 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 :
forall 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 ->
exists c,
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.