proposition: Lemma derivable_pt_lim_finite_sum : forall (An:nat -> R) (x:R) (N:nat), derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x match N with | O => 0 | _ => sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N) end.
proof: Proof. intros. induction N as [| N HrecN]. - simpl. rewrite Rmult_1_r. replace (fun _:R => An 0%nat) with (fct_cte (An 0%nat)); [ apply derivable_pt_lim_const | reflexivity ]. - apply derivable_pt_lim_fs; apply Nat.lt_0_succ. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia