(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)

include "ftc/Rolle.ma".

(* UNEXPORTED
Opaque Min.
*)

(* UNEXPORTED
Section Taylor_Defs
*)

(*#* *Taylor's Theorem

We now prove Taylor's theorem for the remainder of the Taylor
series.  This proof is done in two steps: first, we prove the lemma
for a proper compact interval; next we generalize the result to two
arbitrary (eventually equal) points in a proper interval.

** First case

We assume two different points [a] and [b] in the domain of [F] and
define the nth order derivative of [F] in the interval
[[Min(a,b),Max(a,b)]].
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var
*)

(* begin show *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__" as definition.

(* end show *)

(*#*
This last local definition is simply:
$f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con" as lemma.

(* end hide *)

(*#*
Now we can define the Taylor sequence around [a].  The auxiliary
definition gives, for any [i], the function expressed by the rule
%\[g(x)=\frac{f^{(i)}
(a)}{i!}*(x-a)^i.\]%#g(x)=f<sup>(i)</sup>(a)/i!*(x-a)<sup>i</sup>.#
We denote by [A] and [B] the elements of [[Min(a,b),Max(a,b)]]
corresponding to [a] and [b].
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__" as definition.

(* NOTATION
Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
*)

(* NOTATION
Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
*)

(* end hide *)

(* begin show *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__" as definition.

(* end show *)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con" as lemma.

(* end hide *)

(*#*
Adding the previous expressions up to a given bound [n] gives us the
Taylor sum of order [n].
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con" as definition.

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con" as lemma.

(* end hide *)

(*#*
It is easy to show that [b] is in the domain of this series, which allows us to write down the Taylor remainder around [b].
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con" as lemma.

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con" as lemma.

(* end hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con" as definition.

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__" as definition.

(* UNEXPORTED
Opaque Taylor_seq'_aux Taylor_rem.
*)

(* UNEXPORTED
Transparent Taylor_rem.
*)

(* UNEXPORTED
Opaque Taylor_seq'.
*)

(* UNEXPORTED
Transparent Taylor_seq' Taylor_seq'_aux.
*)

(* UNEXPORTED
Opaque funct_i'.
*)

(* UNEXPORTED
Opaque funct_i.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con" as lemma.

(* UNEXPORTED
Transparent funct_i funct_i'.
*)

(* UNEXPORTED
Opaque Taylor_seq'_aux.
*)

(* UNEXPORTED
Transparent Taylor_seq'_aux.
*)

(* UNEXPORTED
Opaque FSumx.
*)

(* UNEXPORTED
Opaque funct_i'.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con" as lemma.

(* UNEXPORTED
Transparent funct_i' FSumx.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__" as definition.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con" as lemma.

(* UNEXPORTED
Ltac Lazy_Included :=
  repeat first
   [ apply included_IR
   | apply included_FPlus
   | apply included_FInv
   | apply included_FMinus
   | apply included_FMult
   | apply included_FNth
   | apply included_refl ].
*)

(* UNEXPORTED
Ltac Lazy_Eq :=
  repeat first
   [ apply bin_op_wd_unfolded
   | apply un_op_wd_unfolded
   | apply cg_minus_wd
   | apply div_wd
   | apply csf_wd_unfolded ]; Algebra.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con" as lemma.

(* UNEXPORTED
Opaque funct_aux.
*)

(* UNEXPORTED
Transparent funct_aux.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con" as lemma.

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__" as definition.

(* UNEXPORTED
Opaque Taylor_rem funct_aux.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con" as lemma.

(* UNEXPORTED
Transparent Taylor_rem funct_aux.
*)

(* end hide *)

(*#*
Now Taylor's theorem.

%\begin{convention}% Let [e] be a positive real number.
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var
*)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con" as lemma.

(* end hide *)

(* begin show *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__" as definition.

(* end show *)

(* begin hide *)

inline procedural "cic:/CoRN/ftc/TaylorLemma/TLH.con" as lemma.

(* end hide *)

(* UNEXPORTED
Opaque funct_aux.
*)

(* UNEXPORTED
Opaque Taylor_rem.
*)

(* UNEXPORTED
Transparent Taylor_rem funct_aux.
*)

inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con" as lemma.

(* UNEXPORTED
End Taylor_Defs
*)