proposition: Lemma Cv_radius_weak_padding_neg_compat : forall (An : nat -> C) (r : R) (N : nat), Cv_radius_weak (fun n => An (n + N)%nat) r -> Cv_radius_weak An r.
proof: Proof. intros An r N Rho. destruct Rho as [M HM]. destruct (Cseq_partial_bound (fun n => (An n) * r ^ n) N) as [M' HM']. destruct (Req_dec r 0) as [r_eq | r_neq]. exists (Cnorm (An 0%nat)) ; 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, r_eq, Rabs_R0, pow_i, Rmult_0_r ; [apply Cnorm_pos | intuition (auto with arith)]. exists (Rmax (M * Cnorm (r ^ N)) M') ; intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn. destruct (le_lt_dec n N) as [n_lb | n_ub]. apply Rle_trans with M' ; [apply HM' | apply RmaxLess2] ; assumption. apply Rle_trans with (M * Cnorm (r ^ N))%R ; [| apply RmaxLess1] ; unfold_gt. apply Rle_trans with (Cnorm (An n * r ^ n) * (/ Cnorm (r ^ N)) * Cnorm (r ^ N))%R. right ; field ; apply Cnorm_no_R0. apply Cpow_neq_compat ; apply IRC_neq_compat ; assumption. apply Rmult_le_compat_r ; [apply Cnorm_pos |]. apply HM ; exists (n - N)%nat. unfold_gt. rewrite Cnorm_pow, <- pow_inv, <- Cnorm_inv, <- Cnorm_pow, <- Cnorm_Cmult, <- Cpow_inv. assert (Hrew : (n = n - N + N)%nat). intuition lia. repeat rewrite Cnorm_Cmult ; rewrite Hrew at 1 ; rewrite Rmult_assoc ; apply Rmult_eq_compat_l ; rewrite <- Cnorm_Cmult ; apply Cnorm_eq_compat. rewrite Hrew at 1 ; rewrite Cpow_add, Cmult_assoc, Cinv_r, Cmult_1_r ; [reflexivity | apply Cpow_neq_compat ; apply IRC_neq_compat ; assumption]. apply IRC_neq_compat ; assumption. apply IRC_neq_compat ; assumption. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia