proposition: Lemma continuity_finite_sum : forall (An:nat -> R) (N:nat), continuity (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).
proof: Proof. intros; unfold continuity; intro. induction N as [| N HrecN]. - simpl. apply continuity_pt_const. unfold constant; intros; reflexivity. - replace (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. + apply continuity_pt_plus. * apply HrecN. * replace (fun y:R => An (S N) * y ^ S N) with (mult_real_fct (An (S N)) (fun y:R => y ^ S N)). -- apply continuity_pt_scal. apply derivable_continuous_pt. apply derivable_pt_pow. -- reflexivity. + reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia