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)].

Variables a b : IR.
Hypothesis Hap : a [#] b.

Variable F : PartIR.
Hypothesis Ha : Dom F a.
Hypothesis Hb : Dom F b.

Let fi n (Hf : Diffble_I_n Hab' n F) i Hi := ProjT1 (Diffble_I_n_imp_deriv_n _ _ _
i F (le_imp_Diffble_I _ _ _ _ _ (lt_n_Sm_le i n Hi) _ Hf)).

This last local definition is simply: f_i=f⁽ⁱ⁾.

Now we can define the Taylor sequence around a. The auxiliary definition gives, for any i, the function expressed by the rule g(x)=f⁽ⁱ⁾(a)/i!*(x-a)ⁱ. We denote by A and B the elements of [Min(a,b),Max(a,b)] corresponding to a and b.

Let funct_i n Hf i Hi := [-C-] (fi n Hf i Hi A [/] _[//] nring_fac_ap_zero _ i) {*} (FId{-} [-C-]a) {^}i.

Adding the previous expressions up to a given bound n gives us the Taylor sum of order n.

Definition Taylor_seq' n Hf := FSumx _ (funct_i n Hf).

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.

Lemma TL_lemma_b : forall n Hf, Dom (Taylor_seq' n Hf) b.

Definition Taylor_rem n Hf := F b Hb[-]Taylor_seq' n Hf b (TL_lemma_b n Hf).

Now Taylor's theorem.

Let e be a positive real number.

Variable e : IR.
Hypothesis He : 0 [<] e.

Let deriv_Sn' n Hf' :=
n_deriv_I _ _ Hab' (S n) F Hf'{*} [-C-] (1[/] _[//]nring_fac_ap_zero _ n) {*} ( [-C-]b{-}FId) {^}n.

Lemma Taylor_lemma : forall n Hf Hf', {c : IR | I c |
forall Hc, AbsIR (Taylor_rem n Hf[-]deriv_Sn' n Hf' c Hc[*] (b[-]a)) [<=] e}.

End Taylor_Defs.