diff options
author | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
---|---|---|
committer | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
commit | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (patch) | |
tree | fd42f041d099700403dfc0a3af69ea5791ec5930 /theories/Reals/Rseries.v | |
parent | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (diff) |
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Diffstat (limited to 'theories/Reals/Rseries.v')
-rw-r--r-- | theories/Reals/Rseries.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 57b9d3d2f..b3e297598 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -404,3 +404,26 @@ Proof. apply Rinv_neq_0_compat. assumption. Qed. + +(* Convergence is preserved after shifting the indices. *) +Lemma CV_shift : + forall f k l, Un_cv (fun n => f (n + k)%nat) l -> Un_cv f l. +intros f' k l cvfk eps ep; destruct (cvfk eps ep) as [N Pn]. +exists (N + k)%nat; intros n nN; assert (tmp: (n = (n - k) + k)%nat). + rewrite Nat.sub_add;[ | apply le_trans with (N + k)%nat]; auto with arith. +rewrite tmp; apply Pn; apply Nat.le_add_le_sub_r; assumption. +Qed. + +Lemma CV_shift' : + forall f k l, Un_cv f l -> Un_cv (fun n => f (n + k)%nat) l. +intros f' k l cvf eps ep; destruct (cvf eps ep) as [N Pn]. +exists N; intros n nN; apply Pn; auto with arith. +Qed. + +(* Growing property is preserved after shifting the indices (one way only) *) + +Lemma Un_growing_shift : + forall k un, Un_growing un -> Un_growing (fun n => un (n + k)%nat). +Proof. +intros k un P n; apply P. +Qed. |