proposition: Lemma Ccauchy_product : forall An Bn la lb lna, Cser_cv An la -> Cser_cv Bn lb -> Cser_abs_cv An lna -> Cser_cv ((fun k:nat => sum_f_C0 (fun p:nat => An p * Bn (k - p)%nat) k)%C) (la * lb)%C.
proof: Proof. intros An Bn la lb lna HA HB HNA. assert (HNAre : {lnare | Rser_abs_cv (fun n => Cre (An n)) lnare}). apply Rser_pos_maj_cv with (fun n => Cnorm (An n)). intro; apply Rabs_pos. intro; apply Cnorm_pos. intro; unfold Rseq_abs; apply Cre_le_Cnorm. exists lna; apply HNA. destruct HNAre as [lnare HNAre]. assert (HNAim : {lnaim | Rser_abs_cv (fun n => Cim (An n)) lnaim}). apply Rser_pos_maj_cv with (fun n => Cnorm (An n)). intro; apply Rabs_pos. intro; apply Cnorm_pos. intro; unfold Rseq_abs; apply Cim_le_Cnorm. exists lna; apply HNA. destruct HNAim as [lnaim HNAim]. apply Cser_cv_re_im_compat. rewrite Cre_mul. apply Rser_cv_ext with (fun k => sum_f_R0 (fun p => ((Cre (An p) * Cre (Bn (k - p)%nat)))%R) k - sum_f_R0 (fun p => ((Cim (An p) * Cim (Bn (k - p)%nat)))%R) k )%R. repeat (intro; rewrite <- sum_f_C0_Cre_compat; rewrite <- minus_sum; apply Rseq_sum_ext). intro; rewrite <- Cre_mul; trivial. apply Rser_cv_minus_compat. eapply (Rser_cv_prod_compat (fun n => Cre (An n)) (fun n => Cre (Bn n))); try (apply Cser_cv_re_compat; auto). apply HNAre. eapply (Rser_cv_prod_compat (fun n => Cim (An n)) (fun n => Cim (Bn n))); try (apply Cser_cv_im_compat; auto). apply HNAim. rewrite Cim_mul. apply Rser_cv_ext with (fun k => sum_f_R0 (fun p => ((Cre (An p) * Cim (Bn (k - p)%nat)))%R) k + sum_f_R0 (fun p => ((Cim (An p) * Cre (Bn (k - p)%nat)))%R) k )%R. intro; rewrite <- sum_f_C0_Cim_compat ; rewrite <- plus_sum ; apply Rseq_sum_ext. intro; rewrite Cim_mul; ring. apply Rser_cv_plus_compat. eapply (Rser_cv_prod_compat (fun n => Cre (An n)) (fun n => Cim (Bn n))). apply Cser_cv_re_compat; auto. apply Cser_cv_im_compat; auto. apply HNAre. rewrite Rmult_comm. eapply (Rser_cv_prod_compat (fun n => Cim (An n)) (fun n => Cre (Bn n))). apply Cser_cv_im_compat; auto. apply Cser_cv_re_compat; auto. apply HNAim. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Lia Lra Complex Csequence_facts Cseries