proposition: Lemma Cv_radius_weak_derivable_compat_rev : forall An r, Cv_radius_weak (An_deriv An) r -> Cv_radius_weak An r.
proof: Proof. intros An r [B HB] ; exists (Rmax (B * Rabs r) (Rabs (An O))) ; intros x [i Hi] ; subst. destruct i. apply Rle_trans with (Rabs (An O)) ; [apply gt_abs_pser_0_ub | apply Rmax_r]. rewrite gt_abs_pser_S ; apply Rle_trans with (B * Rabs r) ; [| apply Rmax_l]. apply Rmult_le_compat_r ; [apply Rabs_pos |]. apply Rle_trans with (gt_abs_pser (An_deriv An) r i) ; [| apply HB ; exists i ; reflexivity]. rewrite <- (Rmult_1_l (gt_abs_pser (Rseq_shift An) r i)). unfold gt_abs_pser, gt_pser, An_deriv, Rseq_shift, Rseq_abs, Rseq_mult. rewrite Rmult_assoc, (Rabs_mult (INR (S i))) ; apply Rmult_le_compat_r ; [apply Rabs_pos |] ; rewrite <- INR_1, Rabs_INR ; apply le_INR ; lia. 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