CoRN.ftc.TaylorLemma

Require Export Rolle.

Opaque Min.

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 : ∀ n Hf, Dom (Taylor_seq' n Hf) b.
Proof.
intros.
repeat split.
apply FSumx_pred'.
repeat split.
repeat split.
Qed.

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 : ∀ n Hf Hf', {c : IR | I c |
∀ Hc, AbsIR (Taylor_rem n Hf [-]deriv_Sn' n Hf' c Hc [*] (b [-]a )) [<=] e }.
Proof.
intros.
assert (H := TLH).
cut {c : IR | I c | ∀ Hc, AbsIR (g' n Hf Hf' H c Hc) [<=] e [*]AbsIR ([1][/] _[//]H)};
   [ intro H0 | apply Taylor_lemma11; assumption ].
elim H0; intros c Hc' Hc; clear H0; ∃ c.
  auto.
intro.
cut (Dom (funct_aux n Hf' n (lt_n_Sn n)) c). intro H0.
  apply leEq_wdl with (AbsIR (((Taylor_rem n Hf[/] _[//]H) [-]Part _ _ H0) [*] (b [-]a ))).
   eapply leEq_wdl.
    2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
   apply shift_mult_leEq with (AbsIR_resp_ap_zero _ H).
    apply AbsIR_pos; apply H.
   rstepr (e [*] ([1][/] _[//]AbsIR_resp_ap_zero _ H)).
   apply leEq_wdr with (e [*]AbsIR ([1][/] _[//]H)).
    Opaque funct_aux.
    cut (Dom (g' n Hf Hf' H) c). intro H1.
     eapply leEq_wdl.
      apply (Hc H1).
     apply AbsIR_wd; unfold g' in |- ×.
     Opaque Taylor_rem.
     simpl in |- *; rational.
    repeat (split; auto).
   apply mult_wdr.
   apply AbsIR_recip.
  apply eq_symmetric_unfolded.
  apply eq_transitive_unfolded
    with (AbsIR ((Taylor_rem n Hf[/] _[//]H) [-]Part _ _ H0) [*]AbsIR (b [-]a)).
   eapply eq_transitive_unfolded.
    2: apply AbsIR_resp_mult.
   apply AbsIR_wd.
   rstepr (Taylor_rem n Hf[-]Part _ _ H0[*] (b [-]a )).
   apply cg_minus_wd.
    algebra.
   apply mult_wdl.
   Transparent Taylor_rem funct_aux.
   unfold deriv_Sn', funct_aux in |- ×.
   cut (Dom (n_deriv_I _ _ Hab' (S n) F Hf') c). intro H1.
    simpl in |- *; apply eq_transitive_unfolded with (n_deriv_I _ _ Hab' (S n) F Hf' c H1[*]
      ([1][/] _[//]nring_fac_ap_zero _ n) [*] (b [-]c) [^]n).
     repeat apply mult_wdl; apply pfwdef; algebra.
    repeat apply mult_wdl.
    apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S n) (lt_n_S _ _ (lt_n_Sn _))) c Hc').
     2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra.
    apply Feq_imp_eq with (Compact Hab).
     unfold Hab in |- *; apply Derivative_I_n_unique with (S n) F.
      apply n_deriv_lemma.
     apply Taylor_lemma1.
    auto.
   apply n_deriv_inc; auto.
  apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
repeat (split; auto).
Qed.

End Taylor_Defs.