diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 39 |
1 files changed, 31 insertions, 8 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index c540a931..fd16ea61 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -108,7 +108,7 @@ Section sequence. intros n H4. unfold R_dist. rewrite Rabs_left1, Ropp_minus_distr. - apply Rplus_lt_reg_r with (Un n - eps). + apply Rplus_lt_reg_l with (Un n - eps). apply Rlt_le_trans with (Un N). now replace (Un n - eps + (l - Un n)) with (l - eps) by ring. replace (Un n - eps + eps) with (Un n) by ring. @@ -171,7 +171,7 @@ Section sequence. rewrite H1. apply Rle_trans with (1 := proj2 (Hsum n)). apply Rlt_le. - apply Rplus_lt_reg_r with ((/2)^n - 1). + apply Rplus_lt_reg_l with ((/2)^n - 1). now ring_simplify. exists 0. now exists O. @@ -202,7 +202,7 @@ Section sequence. refine (False_ind _ (Rle_not_lt _ _ (H (l - eps) _) _)). intros x (n, H1). now rewrite H1. - apply Rplus_lt_reg_r with (eps - l). + apply Rplus_lt_reg_l with (eps - l). now ring_simplify. assert (Rabs (/2) < 1). @@ -237,9 +237,9 @@ Section sequence. apply le_n_Sn. rewrite (IHN H6), Rplus_0_l. unfold test. - destruct Rle_lt_dec. + destruct Rle_lt_dec as [Hle|Hlt]. apply eq_refl. - now elim Rlt_not_le with (1 := r). + now elim Rlt_not_le with (1 := Hlt). destruct (le_or_lt N n) as [Hn|Hn]. rewrite le_plus_minus with (1 := Hn). @@ -247,7 +247,7 @@ Section sequence. rewrite Hs, Rplus_0_l. set (k := (N + (n - N))%nat). apply Rlt_le. - apply Rplus_lt_reg_r with ((/2)^k - (/2)^N). + apply Rplus_lt_reg_l with ((/2)^k - (/2)^N). now ring_simplify. apply Rle_trans with (sum N). rewrite le_plus_minus with (1 := Hn). @@ -261,7 +261,7 @@ Section sequence. Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l. Proof. intros Hug Heub. - exists (projT1 (completeness EUn Heub EUn_noempty)). + exists (proj1_sig (completeness EUn Heub EUn_noempty)). destruct (completeness EUn Heub EUn_noempty) as (l, H). now apply Un_cv_crit_lub. Qed. @@ -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. |