proposition: Lemma Cv_radius_weak_shifts_compat : forall An r k, Cv_radius_weak An r <-> Cv_radius_weak (Rseq_shifts An k) r.
proof: Proof. intros An r k ; split ; intros [B HB]. destruct (Req_dec r 0) as [r_eq | r_neq]. rewrite r_eq ; exists (Rabs (An k)) ; intros x [i Hi] ; subst ; rewrite <- (Rseq_shifts_O An) ; apply gt_abs_pser_0_ub. assert (Rabs (r ^ k) <> 0) by (apply Rabs_no_R0 ; apply pow_nonzero ; assumption). exists (B * (/ Rabs (r ^ k))) ; intros x [i Hi] ; subst. apply Rle_trans with (Rseq_shifts (gt_abs_pser An r) k i * / Rabs (r ^ k)). unfold gt_abs_pser, gt_pser, Rseq_shifts, Rseq_abs, Rseq_mult ; simpl ; rewrite Nat.add_comm, pow_add, <- Rmult_assoc, (Rabs_mult (An (i + k)%nat * r ^ i)) ; right ; field ; assumption. apply Rmult_le_compat_r ; [left ; apply Rinv_0_lt_compat ; assert (T := Rabs_pos (r ^k)) ; apply Rle_neq_lt ; auto|]. apply HB ; exists (k + i)%nat ; unfold Rseq_shifts ; reflexivity. destruct (Rseq_partial_bound (gt_pser An r) k) as [C HC] ; exists (Rmax (B * Rabs (r ^ k)) C) ; intros u [i Hi] ; subst. destruct (le_lt_dec i k) as [k_lb | k_ub]. apply Rle_trans with C ; [apply HC | apply RmaxLess2] ; assumption. apply Rle_trans with (B * Rabs (r ^ k))%R ; [| apply RmaxLess1]. destruct (lt_exist k i k_ub) as [p Hp] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; rewrite Nat.add_comm, pow_add, Nat.add_comm, <- Rmult_assoc, Rabs_mult ; apply Rmult_le_compat_r ; [apply Rabs_pos |] ; apply HB ; exists p ; unfold Rseq_shifts, gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; reflexivity. 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