proposition: Lemma Cv_radius_weak_padding_pos_compat : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> forall N, Cv_radius_weak (fun n => An (n + N)%nat) r.
proof: Proof. intros An r Rho N. destruct (Req_dec r 0) as [r_eq | r_neq]. rewrite r_eq ; exists (Cnorm (An N)). intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn ; unfold_gt ; destruct n. simpl ; rewrite Cmult_1_r ; right ; reflexivity. rewrite Cnorm_Cmult, Cnorm_pow, Cnorm_IRC_Rabs, RPow_abs, pow_i, Rabs_R0, Rmult_0_r ; [apply Cnorm_pos | intuition (auto with arith)]. destruct Rho as [M HM]. exists (M * (/ Rabs r) ^ N)%R. intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn. unfold_gt ; simpl. rewrite Cnorm_Cmult ; apply Rle_trans with (Cnorm (An (n + N)%nat) * Cnorm (r ^ n) * (Rabs r ^ N) * ((/Rabs r) ^ N))%R. right ; repeat rewrite Rmult_assoc ; repeat apply Rmult_eq_compat_l. rewrite <- Rpow_mult_distr, Rinv_r, pow1, Rmult_1_r ; [reflexivity | apply Rabs_no_R0 ; assumption]. apply Rmult_le_compat_r. apply pow_le ; left ; apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption. rewrite <- Cnorm_IRC_Rabs, Rmult_assoc, <- Cnorm_pow, <- Cnorm_Cmult. apply HM. exists (n + N)%nat ; unfold_gt. repeat rewrite Cnorm_Cmult ; apply IRC_eq_compat. apply Rmult_eq_compat_l ; rewrite <- Cnorm_Cmult ; apply Cnorm_eq_compat. symmetry ; apply Cpow_add. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia