proposition: Lemma infinite_cv_radius_derivable_compat : forall An, infinite_cv_radius An <-> infinite_cv_radius (An_deriv An).
proof: Proof. intro An ; split. intros Rho r ; apply Cv_radius_weak_derivable_compat with (r := (Rabs r) + 1). apply Rho. replace (Rabs (Rabs r + 1)) with (Rabs r + 1). lra. symmetry ; apply Rabs_right. apply Rle_ge ; apply Rle_trans with (Rabs r) ; [apply Rabs_pos | lra]. intros Rho r ; apply Cv_radius_weak_derivable_compat_rev ; apply Rho. 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