proposition: Lemma infinite_cv_radius_prod_compat: forall (An Bn : Rseq), infinite_cv_radius An -> infinite_cv_radius Bn -> infinite_cv_radius (An # Bn).
proof: Proof. intros An Bn rAn rBn r ; apply Cv_radius_weak_prod_compat with (Rabs r + 1) (Rabs r + 1). apply rAn. apply rBn. apply Rlt_le_trans with (Rabs r + 1) ; [lra |]. right ; rewrite Rmin_diag ; symmetry ; apply Rabs_pos_eq ; rewrite Rplus_comm ; apply Rle_zero_pos_plus1, Rabs_pos. Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR