proposition: Lemma arct_cv_radius : finite_cv_radius arct_seq 1.
proof: Proof. rewrite <- Rinv_1 ; apply Rpser_alembert_finite. apply Rgt_not_eq ; lra. intro n ; apply Rinv_neq_0_compat, not_0_INR ; lia. assert (Hf : is_extractor (fun n => S (2 * n))) by (intro ; lia) ; pose (phi := exist _ _ Hf) ; rewrite Rseq_cv_eq_compat with (Vn := (Rseq_poly 1 ⋅ phi / (Rseq_shifts (Rseq_poly 1) 2 ⋅ phi))%Rseq). apply Rseq_equiv_cv_div. eapply Rseq_equiv_subseq_compat, Rseq_poly_shifts_equiv. intro ; apply Rseq_shifts_poly_neq ; lia. intro n ; unfold Rseq_shift, Rseq_shifts, Rseq_abs, Rseq_div, Rseq_poly, extracted, arct_seq, Rdiv ; do 2 rewrite pow_1 ; rewrite Rinv_involutive, Rabs_right. simpl proj1_sig ; simpl mult ; simpl plus ; rewrite <- plus_n_Sm ; apply Rmult_comm. rewrite Rmult_comm ; apply Rle_ge, Rle_mult_inv_pos. apply pos_INR. apply lt_0_INR ; lia. apply not_0_INR ; lia. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity