diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Reals/PartSum.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Reals/PartSum.v')
-rw-r--r-- | theories/Reals/PartSum.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index d5ae2aca..6a33b809 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v 10710 2008-03-23 09:24:09Z herbelin $ i*) +(*i $Id$ i*) Require Import Rbase. Require Import Rfunctions. @@ -31,7 +31,7 @@ Lemma tech2 : forall (An:nat -> R) (m n:nat), (m < n)%nat -> sum_f_R0 An n = - sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m). + sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m). Proof. intros; induction n as [| n Hrecn]. elim (lt_n_O _ H). @@ -155,7 +155,7 @@ Lemma tech12 : Proof. intros; unfold Pser in |- *; unfold infinite_sum in |- *; unfold Un_cv in H; assumption. -Qed. +Qed. Lemma scal_sum : forall (An:nat -> R) (N:nat) (x:R), @@ -256,12 +256,12 @@ Qed. Lemma minus_sum : forall (An Bn:nat -> R) (N:nat), - sum_f_R0 (fun i:nat => An i - Bn i) N = sum_f_R0 An N - sum_f_R0 Bn N. + sum_f_R0 (fun i:nat => An i - Bn i) N = sum_f_R0 An N - sum_f_R0 Bn N. Proof. - intros; induction N as [| N HrecN]. - simpl in |- *; ring. - do 3 rewrite tech5; rewrite HrecN; ring. -Qed. + intros; induction N as [| N HrecN]. + simpl in |- *; ring. + do 3 rewrite tech5; rewrite HrecN; ring. +Qed. Lemma sum_decomposition : forall (An:nat -> R) (N:nat), @@ -346,7 +346,7 @@ Qed. (**********) Lemma Rabs_triang_gen : forall (An:nat -> R) (N:nat), - Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N. + Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N. Proof. intros. induction N as [| N HrecN]. |