proposition: Lemma Cv_radius_weak_le_compat : forall (An : nat -> C) (r r' : R), Rabs r' <= Rabs r -> Cv_radius_weak An r -> Cv_radius_weak An r'.
proof: Proof. intros An r r' r'_bd Rho. case (Req_or_neq r') ; intro r_eq. rewrite r_eq ; exists (Cnorm (An 0%nat)) ; intros x Hx ; destruct Hx as (u, Hu) ; rewrite Hu ; unfold_gt ; clear ; induction u. apply Req_le ; apply Cnorm_eq_compat ; rewrite Cpow_0. apply Cmult_1_r. rewrite C0_pow ; [| intuition (auto with arith)] ; rewrite Cmult_0_r ; rewrite Cnorm_C0 ; apply Cnorm_pos. assert (r_pos : 0 < Rabs r). apply Rlt_le_trans with (Rabs r') ; [apply Rabs_pos_lt |] ; assumption. assert (r_neq : r <> 0%R). case (Req_or_neq r) ; intro s ; [| assumption] ; apply False_ind ; rewrite s in r_pos ; rewrite Rabs_R0 in r_pos ; lra. destruct Rho as (C, HC) ; exists C ; intros x Hx ; destruct Hx as (u,Hu) ; rewrite Hu ; unfold_gt. replace (IRC r' ^ u) with ((IRC r' ^ u * /IRC r ^ u) * (IRC r ^ u)). repeat (rewrite Cnorm_Cmult) ; rewrite Rmult_comm ; rewrite <- Cnorm_Cmult at 1 ; rewrite Rmult_assoc ; rewrite <- Cnorm_Cmult. apply Rle_trans with (1 * Cnorm (IRC r ^ u * An u))%R. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. rewrite Cpow_inv. rewrite <- Cpow_mul_distr_l. rewrite Cnorm_pow. replace 1%R with (1 ^ u)%R. apply pow_le_compat. apply Cnorm_pos. rewrite Cnorm_Cmult ; replace (IZR 1) with (Cnorm (IRC r) * / Cnorm (IRC r))%R. rewrite Cnorm_inv ; repeat rewrite Cnorm_IRC_Rabs. apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption. assumption. apply IRC_neq_0_compat ; assumption. field ; rewrite Cnorm_IRC_Rabs ; apply Rgt_not_eq ; assumption. apply pow1. apply IRC_neq_0_compat ; assumption. rewrite Rmult_1_l ; apply HC. exists u ; unfold_gt ; rewrite Cmult_comm ; reflexivity. field. rewrite IRC_pow_compat ; apply IRC_neq_0_compat ; apply pow_nonzero ; assumption. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia