diff options
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 207 |
1 files changed, 165 insertions, 42 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index db0fddad..479d381d 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -1,16 +1,13 @@ (************************************************************************) (* 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-2010 *) (* \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. @@ -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) @@ -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 _ _ (refl_equal _))). + apply Rle_antisym with (2 := proj1 (Hsum n)). + now rewrite <- Hm. + + assert (Hub: forall n, Un n <= l - eps). + intros n. + generalize (refl_equal (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 refl_equal. + 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. (*********) |