diff options
Diffstat (limited to 'theories7/Reals/SeqSeries.v')
| -rw-r--r-- | theories7/Reals/SeqSeries.v | 307 |
1 files changed, 307 insertions, 0 deletions
diff --git a/theories7/Reals/SeqSeries.v b/theories7/Reals/SeqSeries.v new file mode 100644 index 00000000..dd93c304 --- /dev/null +++ b/theories7/Reals/SeqSeries.v @@ -0,0 +1,307 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: SeqSeries.v,v 1.1.2.1 2004/07/16 19:31:36 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +Require Max. +Require Export Rseries. +Require Export SeqProp. +Require Export Rcomplete. +Require Export PartSum. +Require Export AltSeries. +Require Export Binomial. +Require Export Rsigma. +Require Export Rprod. +Require Export Cauchy_prod. +Require Export Alembert. +V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. +Open Local Scope R_scope. + +(**********) +Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``. +Intros; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](fn (plus (S N) l) x) n) l)). +Intro; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](An (plus (S N) l)) n) l)). +Intro; Elim X; Intros l1N H2. +Elim X0; Intros l2N H3. +Cut ``l1-(SP fn N x)==l1N``. +Intro; Cut ``l2-(sum_f_R0 An N)==l2N``. +Intro; Rewrite H4; Rewrite H5. +Apply sum_cv_maj with [l:nat](An (plus (S N) l)) [l:nat][x:R](fn (plus (S N) l) x) x. +Unfold SP; Apply H2. +Apply H3. +Intros; Apply H1. +Symmetry; EApply UL_sequence. +Apply H3. +Unfold Un_cv in H0; Unfold Un_cv; Intros; Elim (H0 eps H5); Intros N0 H6. +Unfold R_dist in H6; Exists N0; Intros. +Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring]. +Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))). +Apply H6; Unfold ge; Apply le_trans with n. +Apply H7. +Apply le_trans with (plus N n). +Apply le_plus_r. +Apply le_n_Sn. +Cut (le O N). +Cut (lt N (S (plus N n))). +Intros; Assert H10 := (sigma_split An H9 H8). +Unfold sigma in H10. +Do 2 Rewrite <- minus_n_O in H10. +Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))). +Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N). +Cut (minus (S (plus N n)) (S N))=n. +Intro; Rewrite H11 in H10. +Apply H10. +Apply INR_eq; Rewrite minus_INR. +Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_S; Apply le_plus_l. +Apply sum_eq; Intros. +Reflexivity. +Apply sum_eq; Intros. +Reflexivity. +Apply le_lt_n_Sm; Apply le_plus_l. +Apply le_O_n. +Symmetry; EApply UL_sequence. +Apply H2. +Unfold Un_cv in H; Unfold Un_cv; Intros. +Elim (H eps H4); Intros N0 H5. +Unfold R_dist in H5; Exists N0; Intros. +Unfold R_dist SP; Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring]. +Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))). +Unfold SP in H5; Apply H5; Unfold ge; Apply le_trans with n. +Apply H6. +Apply le_trans with (plus N n). +Apply le_plus_r. +Apply le_n_Sn. +Cut (le O N). +Cut (lt N (S (plus N n))). +Intros; Assert H9 := (sigma_split [k:nat](fn k x) H8 H7). +Unfold sigma in H9. +Do 2 Rewrite <- minus_n_O in H9. +Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))). +Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N). +Cut (minus (S (plus N n)) (S N))=n. +Intro; Rewrite H10 in H9. +Apply H9. +Apply INR_eq; Rewrite minus_INR. +Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_S; Apply le_plus_l. +Apply sum_eq; Intros. +Reflexivity. +Apply sum_eq; Intros. +Reflexivity. +Apply le_lt_n_Sm. +Apply le_plus_l. +Apply le_O_n. +Apply existTT with ``l2-(sum_f_R0 An N)``. +Unfold Un_cv in H0; Unfold Un_cv; Intros. +Elim (H0 eps H2); Intros N0 H3. +Unfold R_dist in H3; Exists N0; Intros. +Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring]. +Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))). +Apply H3; Unfold ge; Apply le_trans with n. +Apply H4. +Apply le_trans with (plus N n). +Apply le_plus_r. +Apply le_n_Sn. +Cut (le O N). +Cut (lt N (S (plus N n))). +Intros; Assert H7 := (sigma_split An H6 H5). +Unfold sigma in H7. +Do 2 Rewrite <- minus_n_O in H7. +Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))). +Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N). +Cut (minus (S (plus N n)) (S N))=n. +Intro; Rewrite H8 in H7. +Apply H7. +Apply INR_eq; Rewrite minus_INR. +Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_S; Apply le_plus_l. +Apply sum_eq; Intros. +Reflexivity. +Apply sum_eq; Intros. +Reflexivity. +Apply le_lt_n_Sm. +Apply le_plus_l. +Apply le_O_n. +Apply existTT with ``l1-(SP fn N x)``. +Unfold Un_cv in H; Unfold Un_cv; Intros. +Elim (H eps H2); Intros N0 H3. +Unfold R_dist in H3; Exists N0; Intros. +Unfold R_dist SP. +Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring]. +Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))). +Unfold SP in H3; Apply H3. +Unfold ge; Apply le_trans with n. +Apply H4. +Apply le_trans with (plus N n). +Apply le_plus_r. +Apply le_n_Sn. +Cut (le O N). +Cut (lt N (S (plus N n))). +Intros; Assert H7 := (sigma_split [k:nat](fn k x) H6 H5). +Unfold sigma in H7. +Do 2 Rewrite <- minus_n_O in H7. +Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))). +Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N). +Cut (minus (S (plus N n)) (S N))=n. +Intro; Rewrite H8 in H7. +Apply H7. +Apply INR_eq; Rewrite minus_INR. +Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_S; Apply le_plus_l. +Apply sum_eq; Intros. +Reflexivity. +Apply sum_eq; Intros. +Reflexivity. +Apply le_lt_n_Sm. +Apply le_plus_l. +Apply le_O_n. +Qed. + +(* Comparaison of convergence for series *) +Lemma Rseries_CV_comp : (An,Bn:nat->R) ((n:nat)``0<=(An n)<=(Bn n)``) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 Bn N) l)) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). +Intros; Apply cv_cauchy_2. +Assert H0 := (cv_cauchy_1 ? X). +Unfold Cauchy_crit_series; Unfold Cauchy_crit. +Intros; Elim (H0 eps H1); Intros. +Exists x; Intros. +Cut (Rle (R_dist (sum_f_R0 An n) (sum_f_R0 An m)) (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m))). +Intro; Apply Rle_lt_trans with (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). +Assumption. +Apply H2; Assumption. +Assert H5 := (lt_eq_lt_dec n m). +Elim H5; Intro. +Elim a; Intro. +Rewrite (tech2 An n m); [Idtac | Assumption]. +Rewrite (tech2 Bn n m); [Idtac | Assumption]. +Unfold R_dist; Unfold Rminus; Do 2 Rewrite Ropp_distr1; Do 2 Rewrite <- Rplus_assoc; Do 2 Rewrite Rplus_Ropp_r; Do 2 Rewrite Rplus_Ol; Do 2 Rewrite Rabsolu_Ropp; Repeat Rewrite Rabsolu_right. +Apply sum_Rle; Intros. +Elim (H (plus (S n) n0)); Intros. +Apply H8. +Apply Rle_sym1; Apply cond_pos_sum; Intro. +Elim (H (plus (S n) n0)); Intros. +Apply Rle_trans with (An (plus (S n) n0)); Assumption. +Apply Rle_sym1; Apply cond_pos_sum; Intro. +Elim (H (plus (S n) n0)); Intros; Assumption. +Rewrite b; Unfold R_dist; Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Right; Reflexivity. +Rewrite (tech2 An m n); [Idtac | Assumption]. +Rewrite (tech2 Bn m n); [Idtac | Assumption]. +Unfold R_dist; Unfold Rminus; Do 2 Rewrite Rplus_assoc; Rewrite (Rplus_sym (sum_f_R0 An m)); Rewrite (Rplus_sym (sum_f_R0 Bn m)); Do 2 Rewrite Rplus_assoc; Do 2 Rewrite Rplus_Ropp_l; Do 2 Rewrite Rplus_Or; Repeat Rewrite Rabsolu_right. +Apply sum_Rle; Intros. +Elim (H (plus (S m) n0)); Intros; Apply H8. +Apply Rle_sym1; Apply cond_pos_sum; Intro. +Elim (H (plus (S m) n0)); Intros. +Apply Rle_trans with (An (plus (S m) n0)); Assumption. +Apply Rle_sym1. +Apply cond_pos_sum; Intro. +Elim (H (plus (S m) n0)); Intros; Assumption. +Qed. + +(* Cesaro's theorem *) +Lemma Cesaro : (An,Bn:nat->R;l:R) (Un_cv Bn l) -> ((n:nat)``0<(An n)``) -> (cv_infty [n:nat](sum_f_R0 An n)) -> (Un_cv [n:nat](Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 An n)) l). +Proof with Trivial. +Unfold Un_cv; Intros; Assert H3 : (n:nat)``0<(sum_f_R0 An n)``. +Intro; Apply tech1. +Assert H4 : (n:nat) ``(sum_f_R0 An n)<>0``. +Intro; Red; Intro; Assert H5 := (H3 n); Rewrite H4 in H5; Elim (Rlt_antirefl ? H5). +Assert H5 := (cv_infty_cv_R0 ? H4 H1); Assert H6 : ``0<eps/2``. +Unfold Rdiv; Apply Rmult_lt_pos. +Apply Rlt_Rinv; Sup. +Elim (H ? H6); Clear H; Intros N1 H; Pose C := (Rabsolu (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` N1)); Assert H7 : (EX N:nat | (n:nat) (le N n) -> ``C/(sum_f_R0 An n)<eps/2``). +Case (Req_EM C R0); Intro. +Exists O; Intros. +Rewrite H7; Unfold Rdiv; Rewrite Rmult_Ol; Apply Rmult_lt_pos. +Apply Rlt_Rinv; Sup. +Assert H8 : ``0<eps/(2*(Rabsolu C))``. +Unfold Rdiv; Apply Rmult_lt_pos. +Apply Rlt_Rinv; Apply Rmult_lt_pos. +Sup. +Apply Rabsolu_pos_lt. +Elim (H5 ? H8); Intros; Exists x; Intros; Assert H11 := (H9 ? H10); Unfold R_dist in H11; Unfold Rminus in H11; Rewrite Ropp_O in H11; Rewrite Rplus_Or in H11. +Apply Rle_lt_trans with (Rabsolu ``C/(sum_f_R0 An n)``). +Apply Rle_Rabsolu. +Unfold Rdiv; Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu C)``. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt. +Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l; Replace ``/(Rabsolu C)*(eps*/2)`` with ``eps/(2*(Rabsolu C))``. +Unfold Rdiv; Rewrite Rinv_Rmult. +Ring. +DiscrR. +Apply Rabsolu_no_R0. +Apply Rabsolu_no_R0. +Elim H7; Clear H7; Intros N2 H7; Pose N := (max N1 N2); Exists (S N); Intros; Unfold R_dist; Replace (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 An n)) l) with (Rdiv (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` n) (sum_f_R0 An n)). +Assert H9 : (lt N1 n). +Apply lt_le_trans with (S N). +Apply le_lt_n_Sm; Unfold N; Apply le_max_l. +Rewrite (tech2 [k:nat]``(An k)*((Bn k)-l)`` ? ? H9); Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Apply Rle_lt_trans with (Rplus (Rabsolu (Rdiv (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` N1) (sum_f_R0 An n))) (Rabsolu (Rdiv (sum_f_R0 [i:nat]``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)`` (minus n (S N1))) (sum_f_R0 An n)))). +Apply Rabsolu_triang. +Rewrite (double_var eps); Apply Rplus_lt. +Unfold Rdiv; Rewrite Rabsolu_mult; Fold C; Rewrite Rabsolu_right. +Apply (H7 n); Apply le_trans with (S N). +Apply le_trans with N; [Unfold N; Apply le_max_r | Apply le_n_Sn]. +Apply Rle_sym1; Left; Apply Rlt_Rinv. + +Unfold R_dist in H; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``/(sum_f_R0 An n)``). +Apply Rle_lt_trans with (Rmult (sum_f_R0 [i:nat](Rabsolu ``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)``) (minus n (S N1))) ``/(sum_f_R0 An n)``). +Do 2 Rewrite <- (Rmult_sym ``/(sum_f_R0 An n)``); Apply Rle_monotony. +Left; Apply Rlt_Rinv. +Apply (sum_Rabsolu [i:nat]``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)`` (minus n (S N1))). +Apply Rle_lt_trans with (Rmult (sum_f_R0 [i:nat]``(An (plus (S N1) i))*eps/2`` (minus n (S N1))) ``/(sum_f_R0 An n)``). +Do 2 Rewrite <- (Rmult_sym ``/(sum_f_R0 An n)``); Apply Rle_monotony. +Left; Apply Rlt_Rinv. +Apply sum_Rle; Intros; Rewrite Rabsolu_mult; Pattern 2 (An (plus (S N1) n0)); Rewrite <- (Rabsolu_right (An (plus (S N1) n0))). +Apply Rle_monotony. +Apply Rabsolu_pos. +Left; Apply H; Unfold ge; Apply le_trans with (S N1); [Apply le_n_Sn | Apply le_plus_l]. +Apply Rle_sym1; Left. +Rewrite <- (scal_sum [i:nat](An (plus (S N1) i)) (minus n (S N1)) ``eps/2``); Unfold Rdiv; Repeat Rewrite Rmult_assoc; Apply Rlt_monotony. +Pattern 2 ``/2``; Rewrite <- Rmult_1r; Apply Rlt_monotony. +Apply Rlt_Rinv; Sup. +Rewrite Rmult_sym; Apply Rlt_monotony_contra with (sum_f_R0 An n). +Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l; Rewrite Rmult_1r; Rewrite (tech2 An N1 n). +Rewrite Rplus_sym; Pattern 1 (sum_f_R0 [i:nat](An (plus (S N1) i)) (minus n (S N1))); Rewrite <- Rplus_Or; Apply Rlt_compatibility. +Apply Rle_sym1; Left; Apply Rlt_Rinv. +Replace (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` n) with (Rplus (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 [k:nat]``(An k)*-l`` n)). +Rewrite <- (scal_sum An n ``-l``); Field. +Rewrite <- plus_sum; Apply sum_eq; Intros; Ring. +Qed. + +Lemma Cesaro_1 : (An:nat->R;l:R) (Un_cv An l) -> (Un_cv [n:nat]``(sum_f_R0 An (pred n))/(INR n)`` l). +Proof with Trivial. +Intros Bn l H; Pose An := [_:nat]R1. +Assert H0 : (n:nat) ``0<(An n)``. +Intro; Unfold An; Apply Rlt_R0_R1. +Assert H1 : (n:nat)``0<(sum_f_R0 An n)``. +Intro; Apply tech1. +Assert H2 : (cv_infty [n:nat](sum_f_R0 An n)). +Unfold cv_infty; Intro; Case (total_order_Rle M R0); Intro. +Exists O; Intros; Apply Rle_lt_trans with R0. +Assert H2 : ``0<M``. +Auto with real. +Clear n; Pose m := (up M); Elim (archimed M); Intros; Assert H5 : `0<=m`. +Apply le_IZR; Unfold m; Simpl; Left; Apply Rlt_trans with M. +Elim (IZN ? H5); Intros; Exists x; Intros; Unfold An; Rewrite sum_cte; Rewrite Rmult_1l; Apply Rlt_trans with (IZR (up M)). +Apply Rle_lt_trans with (INR x). +Rewrite INR_IZR_INZ; Fold m; Rewrite <- H6; Right. +Apply lt_INR; Apply le_lt_n_Sm. +Assert H3 := (Cesaro ? ? ? H H0 H2). +Unfold Un_cv; Unfold Un_cv in H3; Intros; Elim (H3 ? H4); Intros; Exists (S x); Intros; Unfold R_dist; Unfold R_dist in H5; Apply Rle_lt_trans with (Rabsolu (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` (pred n)) (sum_f_R0 An (pred n))) l)). +Right; Replace ``(sum_f_R0 Bn (pred n))/(INR n)-l`` with (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` (pred n)) (sum_f_R0 An (pred n))) l). +Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-l``); Apply Rplus_plus_r. +Unfold An; Replace (sum_f_R0 [k:nat]``1*(Bn k)`` (pred n)) with (sum_f_R0 Bn (pred n)). +Rewrite sum_cte; Rewrite Rmult_1l; Replace (S (pred n)) with n. +Apply S_pred with O; Apply lt_le_trans with (S x). +Apply lt_O_Sn. +Apply sum_eq; Intros; Ring. +Apply H5; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n. +Apply S_pred with O; Apply lt_le_trans with (S x). +Apply lt_O_Sn. +Qed. |