proposition: Lemma is_pseries_mult (a b : nat -> R) (x la lb : R) : is_pseries a x la -> is_pseries b x lb -> Rbar_lt (Rabs x) (CV_radius a) -> Rbar_lt (Rabs x) (CV_radius b) -> is_pseries (PS_mult a b) x (la * lb).
proof: Proof. move => Hla Hlb Ha Hb. apply is_series_ext with (fun n => sum_f_R0 (fun k => (fun l => a l * x ^ l) k * (fun l => b l * x ^ l) (n - k)%nat) n). move => n. rewrite /PS_mult /scal /= /mult /= scal_sum. apply sum_eq => i Hi. rewrite -{4}(MyNat.sub_add _ _ Hi). rewrite pow_n_pow pow_add. ring. apply (is_series_mult (fun l => a l * x ^ l) (fun l => b l * x ^ l)). now apply (is_pseries_R a x la). now apply (is_pseries_R b x lb). by apply CV_disk_inside. by apply CV_disk_inside. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series