proposition: Lemma Cv_radius_weak_plus : forall (An Bn : nat -> C) (r1 r2 : R), Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> Cv_radius_weak (fun n => An n + Bn n) (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')%R. intros x Hx ; destruct Hx as (u, Hu) ; rewrite Hu ; unfold_gt. rewrite Cmult_add_distr_r ; apply Rle_trans with (Cnorm (An u * IRC (Rmin (Rabs r1) (Rabs r2)) ^ u) + Cnorm (Bn u * IRC (Rmin (Rabs r1) (Rabs r2)) ^ u))%R ; [apply Cnorm_triang |]. apply Rle_trans with (Cnorm (An u * IRC (Rmin (Rabs r1) (Rabs r2)) ^ u) + C')%R ; [apply Rplus_le_compat_l ; apply HC' | apply Rplus_le_compat_r ; apply HC] ; exists u ; intuition. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia