diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 243 |
1 files changed, 183 insertions, 60 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index db0fddad..3c10725b 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -1,18 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rseries.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Rbase. Require Import Rfunctions. -Require Import Classical. Require Import Compare. -Open Local Scope R_scope. +Local Open Scope R_scope. Implicit Type r : R. @@ -28,7 +25,7 @@ Section sequence. Variable Un : nat -> R. (*********) - Boxed Fixpoint Rmax_N (N:nat) : R := + Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) @@ -57,20 +54,20 @@ Section sequence. (*********) Lemma EUn_noempty : exists r : R, EUn r. Proof. - unfold EUn in |- *; split with (Un 0); split with 0%nat; trivial. + unfold EUn; split with (Un 0); split with 0%nat; trivial. Qed. (*********) Lemma Un_in_EUn : forall n:nat, EUn (Un n). Proof. - intro; unfold EUn in |- *; split with n; trivial. + intro; unfold EUn; split with n; trivial. Qed. (*********) Lemma Un_bound_imp : forall x:R, (forall n:nat, Un n <= x) -> is_upper_bound EUn x. Proof. - intros; unfold is_upper_bound in |- *; intros; unfold EUn in H0; elim H0; + intros; unfold is_upper_bound; intros; unfold EUn in H0; elim H0; clear H0; intros; generalize (H x1); intro; rewrite <- H0 in H1; trivial. Qed. @@ -80,7 +77,7 @@ Section sequence. forall n m:nat, Un_growing -> (n >= m)%nat -> Un n >= Un m. Proof. double induction n m; intros. - unfold Rge in |- *; right; trivial. + unfold Rge; right; trivial. exfalso; unfold ge in H1; generalize (le_Sn_O n0); intro; auto. cut (n0 >= 0)%nat. generalize H0; intros; unfold Un_growing in H0; @@ -92,7 +89,7 @@ Section sequence. elim y; clear y; intro y. unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro; exfalso; auto. - rewrite y; unfold Rge in |- *; right; trivial. + rewrite y; unfold Rge; right; trivial. unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro; unfold Un_growing in H1; apply @@ -100,47 +97,173 @@ Section sequence. (Rle_ge (Un n1) (Un (S n1)) (H1 n1)) H3). Qed. +(*********) + Lemma Un_cv_crit_lub : Un_growing -> forall l, is_lub EUn l -> Un_cv l. + Proof. + intros Hug l H eps Heps. + + cut (exists N, Un N > l - eps). + intros (N, H3). + exists N. + intros n H4. + unfold R_dist. + rewrite Rabs_left1, Ropp_minus_distr. + apply Rplus_lt_reg_r 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. + apply Rge_le. + now apply growing_prop. + apply Rle_minus. + apply (proj1 H). + now exists n. + + assert (Hi2pn: forall n, 0 < (/ 2)^n). + clear. intros n. + apply pow_lt. + apply Rinv_0_lt_compat. + now apply (IZR_lt 0 2). + + pose (test := fun n => match Rle_lt_dec (Un n) (l - eps) with left _ => false | right _ => true end). + pose (sum := let fix aux n := match n with S n' => aux n' + + if test n' then (/ 2)^n else 0 | O => 0 end in aux). + + assert (Hsum': forall m n, sum m <= sum (m + n)%nat <= sum m + (/2)^m - (/2)^(m + n)). + clearbody test. + clear -Hi2pn. + intros m. + induction n. + rewrite<- plus_n_O. + ring_simplify (sum m + (/ 2) ^ m - (/ 2) ^ m). + split ; apply Rle_refl. + rewrite <- plus_n_Sm. + simpl. + split. + apply Rle_trans with (sum (m + n)%nat + 0). + rewrite Rplus_0_r. + apply IHn. + apply Rplus_le_compat_l. + case (test (m + n)%nat). + apply Rlt_le. + exact (Hi2pn (S (m + n))). + apply Rle_refl. + apply Rle_trans with (sum (m + n)%nat + / 2 * (/ 2) ^ (m + n)). + apply Rplus_le_compat_l. + case (test (m + n)%nat). + apply Rle_refl. + apply Rlt_le. + exact (Hi2pn (S (m + n))). + apply Rplus_le_reg_r with (-(/ 2 * (/ 2) ^ (m + n))). + rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r. + apply Rle_trans with (1 := proj2 IHn). + apply Req_le. + field. + + assert (Hsum: forall n, 0 <= sum n <= 1 - (/2)^n). + intros N. + generalize (Hsum' O N). + simpl. + now rewrite Rplus_0_l. + + destruct (completeness (fun x : R => exists n : nat, x = sum n)) as (m, (Hm1, Hm2)). + exists 1. + intros x (n, H1). + rewrite H1. + apply Rle_trans with (1 := proj2 (Hsum n)). + apply Rlt_le. + apply Rplus_lt_reg_r with ((/2)^n - 1). + now ring_simplify. + exists 0. now exists O. + + destruct (Rle_or_lt m 0) as [[Hm|Hm]|Hm]. + elim Rlt_not_le with (1 := Hm). + apply Hm1. + now exists O. + + assert (Hs0: forall n, sum n = 0). + intros n. + specialize (Hm1 (sum n) (ex_intro _ _ (eq_refl _))). + apply Rle_antisym with (2 := proj1 (Hsum n)). + now rewrite <- Hm. + + assert (Hub: forall n, Un n <= l - eps). + intros n. + generalize (eq_refl (sum (S n))). + simpl sum at 1. + rewrite 2!Hs0, Rplus_0_l. + unfold test. + destruct Rle_lt_dec. easy. + intros H'. + elim Rgt_not_eq with (2 := H'). + exact (Hi2pn (S n)). + + clear -Heps H Hub. + destruct H as (_, H). + refine (False_ind _ (Rle_not_lt _ _ (H (l - eps) _) _)). + intros x (n, H1). + now rewrite H1. + apply Rplus_lt_reg_r with (eps - l). + now ring_simplify. + + assert (Rabs (/2) < 1). + rewrite Rabs_pos_eq. + rewrite <- Rinv_1 at 3. + apply Rinv_lt_contravar. + rewrite Rmult_1_l. + now apply (IZR_lt 0 2). + now apply (IZR_lt 1 2). + apply Rlt_le. + apply Rinv_0_lt_compat. + now apply (IZR_lt 0 2). + destruct (pow_lt_1_zero (/2) H0 m Hm) as [N H4]. + exists N. + apply Rnot_le_lt. + intros H5. + apply Rlt_not_le with (1 := H4 _ (le_refl _)). + rewrite Rabs_pos_eq. 2: now apply Rlt_le. + apply Hm2. + intros x (n, H6). + rewrite H6. clear x H6. + + assert (Hs: sum N = 0). + clear H4. + induction N. + easy. + simpl. + assert (H6: Un N <= l - eps). + apply Rle_trans with (2 := H5). + apply Rge_le. + apply growing_prop ; try easy. + apply le_n_Sn. + rewrite (IHN H6), Rplus_0_l. + unfold test. + destruct Rle_lt_dec. + apply eq_refl. + now elim Rlt_not_le with (1 := r). + + destruct (le_or_lt N n) as [Hn|Hn]. + rewrite le_plus_minus with (1 := Hn). + apply Rle_trans with (1 := proj2 (Hsum' N (n - N)%nat)). + rewrite Hs, Rplus_0_l. + set (k := (N + (n - N))%nat). + apply Rlt_le. + apply Rplus_lt_reg_r with ((/2)^k - (/2)^N). + now ring_simplify. + apply Rle_trans with (sum N). + rewrite le_plus_minus with (1 := Hn). + rewrite plus_Snm_nSm. + exact (proj1 (Hsum' _ _)). + rewrite Hs. + now apply Rlt_le. + Qed. -(** classical is needed: [not_all_not_ex] *) (*********) Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l. Proof. - unfold Un_growing, Un_cv in |- *; intros; - generalize (completeness_weak EUn H0 EUn_noempty); - intro; elim H1; clear H1; intros; split with x; intros; - unfold is_lub in H1; unfold bound in H0; unfold is_upper_bound in H0, H1; - elim H0; clear H0; intros; elim H1; clear H1; intros; - generalize (H3 x0 H0); intro; cut (forall n:nat, Un n <= x); - intro. - cut (exists N : nat, x - eps < Un N). - intro; elim H6; clear H6; intros; split with x1. - intros; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps). - unfold Rgt in H2; - apply (Rle_lt_trans (Un n - x) 0 eps (Rle_minus (Un n) x (H5 n)) H2). - fold Un_growing in H; generalize (growing_prop n x1 H H7); intro; - generalize - (Rlt_le_trans (x - eps) (Un x1) (Un n) H6 (Rge_le (Un n) (Un x1) H8)); - intro; generalize (Rplus_lt_compat_l (- x) (x - eps) (Un n) H9); - unfold Rminus in |- *; rewrite <- (Rplus_assoc (- x) x (- eps)); - rewrite (Rplus_comm (- x) (Un n)); fold (Un n - x) in |- *; - rewrite Rplus_opp_l; rewrite (let (H1, H2) := Rplus_ne (- eps) in H2); - trivial. - cut (~ (forall N:nat, x - eps >= Un N)). - intro; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)); red in |- *; - intro; red in H6; elim H6; clear H6; intro; - apply (Rnot_lt_ge (x - eps) (Un N) (H7 N)). - red in |- *; intro; cut (forall N:nat, Un N <= x - eps). - intro; generalize (Un_bound_imp (x - eps) H7); intro; - unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); - intro; generalize (Rle_minus x (x - eps) H9); unfold Rminus in |- *; - rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r; - rewrite (let (H1, H2) := Rplus_ne (- - eps) in H2); - rewrite Ropp_involutive; intro; unfold Rgt in H2; - generalize (Rgt_not_le eps 0 H2); intro; auto. - intro; elim (H6 N); intro; unfold Rle in |- *. - left; unfold Rgt in H7; assumption. - right; auto. - apply (H1 (Un n) (Un_in_EUn n)). + intros Hug Heub. + exists (projT1 (completeness EUn Heub EUn_noempty)). + destruct (completeness EUn Heub EUn_noempty) as (l, H). + now apply Un_cv_crit_lub. Qed. (*********) @@ -149,20 +272,20 @@ Section sequence. Proof. intro; induction N as [| N HrecN]. split with (Un 0); intros; rewrite (le_n_O_eq n H); - apply (Req_le (Un n) (Un n) (refl_equal (Un n))). + apply (Req_le (Un n) (Un n) (eq_refl (Un n))). elim HrecN; clear HrecN; intros; split with (Rmax (Un (S N)) x); intros; elim (Rmax_Rle (Un (S N)) x (Un n)); intros; clear H1; inversion H0. rewrite <- H1; rewrite <- H1 in H2; apply - (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (refl_equal (Un n))))). + (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (eq_refl (Un n))))). apply (H2 (or_intror (Un n <= Un (S N)) (H n H3))). Qed. (*********) Lemma cauchy_bound : Cauchy_crit -> bound EUn. Proof. - unfold Cauchy_crit, bound in |- *; intros; unfold is_upper_bound in |- *; + unfold Cauchy_crit, bound; intros; unfold is_upper_bound; unfold Rgt in H; elim (H 1 Rlt_0_1); clear H; intros; generalize (H x); intro; generalize (le_dec x); intro; elim (finite_greater x); intros; split with (Rmax x0 (Un x + 1)); @@ -201,12 +324,12 @@ End Isequence. Lemma GP_infinite : forall x:R, Rabs x < 1 -> Pser (fun n:nat => 1) x (/ (1 - x)). Proof. - intros; unfold Pser in |- *; unfold infinite_sum in |- *; intros; + intros; unfold Pser; unfold infinite_sum; intros; elim (Req_dec x 0). intros; exists 0%nat; intros; rewrite H1; rewrite Rminus_0_r; rewrite Rinv_1; cut (sum_f_R0 (fun n0:nat => 1 * 0 ^ n0) n = 1). intros; rewrite H3; rewrite R_dist_eq; auto. - elim n; simpl in |- *. + elim n; simpl. ring. intros; rewrite H3; ring. intro; cut (0 < eps * (Rabs (1 - x) * Rabs (/ x))). @@ -221,11 +344,11 @@ Proof. apply Rabs_pos_lt. apply Rminus_eq_contra. apply Rlt_dichotomy_converse. - right; unfold Rgt in |- *. + right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). apply RRle_abs. assumption. - unfold R_dist in |- *; rewrite <- Rabs_mult. + unfold R_dist; rewrite <- Rabs_mult. rewrite Rmult_minus_distr_l. cut ((1 - x) * sum_f_R0 (fun n0:nat => x ^ n0) n = @@ -236,7 +359,7 @@ Proof. cut (- (x ^ (n + 1) - 1) - 1 = - x ^ (n + 1)). intro; rewrite H7. rewrite Rabs_Ropp; cut ((n + 1)%nat = S n); auto. - intro H8; rewrite H8; simpl in |- *; rewrite Rabs_mult; + intro H8; rewrite H8; simpl; rewrite Rabs_mult; apply (Rlt_le_trans (Rabs x * Rabs (x ^ n)) (Rabs x * (eps * (Rabs (1 - x) * Rabs (/ x)))) ( @@ -250,7 +373,7 @@ Proof. Rabs x * Rabs (/ x) * (eps * Rabs (1 - x))). clear H8; intros; rewrite H8; rewrite <- Rabs_mult; rewrite Rinv_r. rewrite Rabs_R1; cut (1 * (eps * Rabs (1 - x)) = Rabs (1 - x) * eps). - intros; rewrite H9; unfold Rle in |- *; right; reflexivity. + intros; rewrite H9; unfold Rle; right; reflexivity. ring. assumption. ring. @@ -258,12 +381,12 @@ Proof. ring. apply Rminus_eq_contra. apply Rlt_dichotomy_converse. - right; unfold Rgt in |- *. + right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). apply RRle_abs. assumption. ring; ring. - elim n; simpl in |- *. + elim n; simpl. ring. intros; rewrite H5. ring. @@ -273,7 +396,7 @@ Proof. apply Rabs_pos_lt. apply Rminus_eq_contra. apply Rlt_dichotomy_converse. - right; unfold Rgt in |- *. + right; unfold Rgt. apply (Rle_lt_trans x (Rabs x) 1). apply RRle_abs. assumption. |