proposition: Lemma exp_infinite_cv_radius : infinite_cv_radius exp_seq.
proof: Proof. intros r. pose (M := (/ (Rabs r + 1))%R) ; assert (M_pos : 0 < M). unfold M ; apply Rinv_0_lt_compat ; apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1]. apply (Rpser_alembert_prelim2 exp_seq M M_pos exp_seq_neq). assert (t : (1 > 0)%nat) by constructor ; assert (H := Rseq_poly_cv 1 t) ; assert (H2 := Rseq_cv_pos_infty_shift_compat_reciprocal _ H) ; assert (H3 := Rseq_cv_pos_infty_inv_compat _ H2) ; clear t H H2 ; destruct (H3 _ M_pos) as [N HN] ; exists N ; intro n ; unfold Rseq_shifts. rewrite Rdiv_exp_seq_simpl ; apply Rle_trans with (R_dist ((/ Rseq_shift (Rseq_poly 1))%Rseq (N + n)%nat) 0). right ; unfold R_dist, Rseq_shift, Rseq_poly, pow ; apply Rabs_eq_compat ; rewrite Rminus_0_r, <- (Rmult_1_r (INR (S (N + n)))) ; reflexivity. left ; apply HN ; intuition. unfold M ; rewrite Rinv_involutive ; [| apply Rgt_not_eq ; apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1]] ; intuition. 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