proposition: 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).
proof: Proof. intros. destruct (Req_dec x0 x) as [Heq|Hdif]. rewrite Heq. exists x. split; [|now intros H'; case H']. rewrite Rminus_diag_eq; [|trivial]. now rewrite Rminus_diag_eq; [simpl|easy]; rewrite Rmult_0_l, Rmult_0_r. elim n. simpl; field. intros k Hk; simpl. now rewrite Hk, Rminus_diag_eq; [simpl|easy]; rewrite Rmult_0_l, Rmult_0_r, Rplus_0_r. case (Rolle_lim g x0 x (fun d => (- ((D (S n) d) / (INR (fact n)) * (x - d)^n) + c * (INR (S n)) * (x - d)^n))). - intros y Hy; apply derivable_pt_lim_aux. split; destruct Hy as [H|H]; case Hx0; case Hx; case H; psatzl R. - intros y Hy. apply continuity_pt_minus; [|reg]. apply continuity_pt_minus; [reg|]. apply continuity_pt_sum. intros n' hn'; apply continuity_pt_mult. + unfold Rdiv; apply continuity_pt_mult. apply continuity_pt_Dp; [easy|]. split; destruct Hy as [H|H]; case Hx0; case Hx; case H; psatzl R. now reg. + now reg. - easy. - assert (Hgx0 : g x0 = 0). unfold g, c, Rdiv. rewrite Rmult_assoc, <-Rinv_l_sym; [ring|]. now apply pow_nonzero; apply Rminus_eq_contra; intros H; case Hdif. assert (Hgx : g x = 0). unfold g, c, Rminus. rewrite Rplus_opp_r, pow_ne_zero; [|easy]. ring_simplify. assert (Htsum : forall p, D 0 x - Tsum p x x = 0). induction p as [|n' IHn]. simpl; field. unfold Rminus in IHn |-*; simpl. rewrite Ropp_plus_distr, <- Rplus_assoc, IHn; ring_simplify; trivial. now rewrite Rminus_diag_eq in Htsum. now rewrite Hgx0, Hgx. - intros d [Hd1 Hd2]. exists d. split. + assert (Hk : Oab d). destruct Hd1 as [Hy|Hy]; split; case Hy; case Hx0; case Hx; psatzl R. assert (H1 := derivable_pt_lim_aux d Hk). assert ((- (D (S n) d / INR (fact n) * (x - d) ^ n) + c * INR (S n) * (x - d) ^ n) = 0). now apply uniqueness_limite with g d. assert (Hc : c = D (S n) d / INR (fact (S n))). assert (Hc1 := Rplus_opp_r_uniq _ _ H). rewrite Ropp_involutive in Hc1. assert (Hc2 : c * INR (S n) = D (S n) d / INR (fact n)). apply Rmult_eq_reg_r with ((x-d)^n); [easy|]. apply pow_nonzero. destruct Hd1 as [H0|H0]; apply Rminus_eq_contra. now apply Rgt_not_eq; case H0. now apply Rlt_not_eq; case H0. apply Rmult_eq_reg_r with (INR (S n)); [|now apply not_0_INR]. rewrite Hc2. replace (fact (S n)) with (fact n * (S n))%nat by (simpl; ring). rewrite mult_INR; field. split; apply not_0_INR; [easy|apply fact_neq_0]. unfold c in Hc. apply Rmult_eq_reg_r with (/(x - x0) ^ S n). unfold Rdiv in Hc at 1; rewrite Hc; field. split; [|apply not_0_INR; apply fact_neq_0]. apply pow_nonzero; apply Rminus_eq_contra; trivial. now intros H'; case Hdif. apply Rinv_neq_0_compat; apply pow_nonzero; apply Rminus_eq_contra. now intros H'; case Hdif. + now case Hd1. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib