proposition: Lemma derivable_pt_lim_fs : forall (An:nat -> R) (x:R) (N:nat), (0 < N)%nat -> derivable_pt_lim (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N) x (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N)).
proof: Proof. intros; induction N as [| N HrecN]. { elim (Nat.lt_irrefl _ H). } assert (N = 0%nat \/ (0 < N)%nat) by nia. elim H0; intro. { rewrite H1. simpl. change (fun y:R => An 0%nat * 1 + An 1%nat * (y * 1)) with (fct_cte (An 0%nat * 1) + mult_real_fct (An 1%nat) (id * fct_cte 1))%F. replace (1 * An 1%nat * 1) with (0 + An 1%nat * (1 * fct_cte 1 x + id x * 0)) by (unfold fct_cte, id; ring). apply derivable_pt_lim_plus. - apply derivable_pt_lim_const. - apply derivable_pt_lim_scal. apply derivable_pt_lim_mult. + apply derivable_pt_lim_id. + apply derivable_pt_lim_const. } change (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) (S N)) with ((fun y:R => sum_f_R0 (fun k:nat => (An k * y ^ k)%R) N) + (fun y:R => (An (S N) * y ^ S N)%R))%F. replace (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N))) with (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred N) + An (S N) * (INR (S (pred (S N))) * x ^ pred (S N))). 2:{ assert (pred (S N) = S (pred N)) by lia. rewrite H2. rewrite tech5. apply Rplus_eq_compat_l. rewrite <- H2. change (pred (S N)) with N. ring. } apply derivable_pt_lim_plus. { apply HrecN. assumption. } change (fun y:R => An (S N) * y ^ S N) with (mult_real_fct (An (S N)) (fun y:R => y ^ S N)). apply derivable_pt_lim_scal. apply derivable_pt_lim_pow. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia