proposition: Lemma Cv_radius_weak_plus : forall An Bn r1 r2, Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> Cv_radius_weak (An + Bn)%Rseq (Rmin (Rabs r1) (Rabs r2)).
proof: Proof. intros An Bn r1 r2 RhoA RhoB. assert (r''_bd1 : Rabs (Rmin (Rabs r1) (Rabs r2)) <= Rabs r1). unfold Rmin ; case (Rle_dec (Rabs r1) (Rabs r2)) ; intro H ; rewrite Rabs_Rabsolu ; intuition (auto with real). assert (r''_bd2 : Rabs (Rmin (Rabs r1) (Rabs r2)) <= Rabs r2). unfold Rmin ; case (Rle_dec (Rabs r1) (Rabs r2)) ; intro H ; rewrite Rabs_Rabsolu ; intuition (auto with real). assert (Rho'A := Cv_radius_weak_le_compat An _ _ r''_bd1 RhoA). assert (Rho'B := Cv_radius_weak_le_compat Bn _ _ r''_bd2 RhoB). destruct Rho'A as (C, HC) ; destruct Rho'B as (C', HC') ; exists (C + C'). intros x [i Hi] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, Rseq_plus. rewrite Rmult_plus_distr_r ; apply Rle_trans with (Rabs (An i * Rmin (Rabs r1) (Rabs r2) ^ i) + Rabs (Bn i * Rmin (Rabs r1) (Rabs r2) ^ i)) ; [apply Rabs_triang |]. apply Rle_trans with (Rabs (An i * Rmin (Rabs r1) (Rabs r2) ^ i) + C') ; [apply Rplus_le_compat_l ; apply HC' | apply Rplus_le_compat_r ; apply HC] ; exists i ; intuition. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR