General case
The generalization to arbitrary intervals just needs a few more definitions.
Let I be a proper interval, F:PartIR and a,b:IR be points of I.
Variable I : interval.
Hypothesis pI : proper I.
Variable F : PartIR.
Let deriv_Sn b n Hf :=
N_Deriv _ pI (S n) F Hf{*} [-C-] (1[/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]b{-}FId) {^}n.
Variables a b : IR.
Hypothesis Ha : I a.
Hypothesis Hb : I b.
Let fi n Hf i Hi :=
N_Deriv _ pI _ _ (le_imp_Diffble_n _ _ _ _ (lt_n_Sm_le i n Hi) F Hf).
Let funct_i n Hf i Hi :=
[-C-] (fi n Hf i Hi a Ha[/] _[//]nring_fac_ap_zero _ i) {*} (FId{-} [-C-]a) {^}i.
Definition Taylor_Seq' n Hf := FSumx _ (funct_i n Hf).
Definition Taylor_Rem n Hf := F b (Diffble_n_imp_inc _ _ _ _ Hf b Hb) [-]
Taylor_Seq' n Hf b (TaylorB n Hf).
Theorem Taylor' : forall n Hf Hf' e, 0 [<] e -> {c : IR | Compact (Min_leEq_Max a b) c |
forall Hc, AbsIR (Taylor_Rem n Hf'[-]deriv_Sn b n Hf c Hc[*] (b[-]a)) [<=] e}.
Included.
Qed.
End More_Taylor_Defs.
Section Taylor_Theorem.
And finally the ``nice'' version, when we know the expression of the
derivatives of F.
Let f be the sequence of derivatives of F of order up to n and F' be the nth-derivative of F.
Let f be the sequence of derivatives of F of order up to n and F' be the nth-derivative of F.
Variable I : interval.
Hypothesis pI : proper I.
Variable F : PartIR.
Variable n : N.
Variable f : forall i : N, i < S n -> PartIR.
Hypothesis goodF : ext_fun_seq f.
Hypothesis goodF' : ext_fun_seq' f.
Hypothesis derF : forall i Hi, Derivative_n i I pI F (f i Hi).
Variable F' : PartIR.
Hypothesis derF' : Derivative_n (S n) I pI F F'.
Variables a b : IR.
Hypothesis Ha : I a.
Hypothesis Hb : I b.
Let funct_i i Hi := let HX := (Derivative_n_imp_inc' _ _ _ _ _ (derF i Hi) a Ha) in
[-C-] (f i Hi a HX [/] _[//] nring_fac_ap_zero _ i) {*} (FId{-} [-C-]a) {^}i.
Definition Taylor_Seq := FSumx _ funct_i.
Let deriv_Sn := F'{*} [-C-] (1[/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]b{-}FId) {^}n.
Lemma Taylor_aux : Dom Taylor_Seq b.
Theorem Taylor : forall e, 0 [<] e -> forall Hb', {c : IR | Compact (Min_leEq_Max a b) c |
forall Hc, AbsIR (F b Hb'[-]Part _ _ Taylor_aux[-]deriv_Sn c Hc[*] (b[-]a)) [<=] e}.
End Taylor_Theorem.