diff options
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 113 |
1 files changed, 52 insertions, 61 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index a8548eb7..e848e4df 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.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 *) @@ -35,10 +35,8 @@ Proof. [ intro | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H0 (/ 2) H1); intros. exists (sum_f_R0 An x + 2 * An (S x)). - unfold is_upper_bound; intros; unfold EUn in H3; elim H3; intros. - rewrite H4; assert (H5 := lt_eq_lt_dec x1 x). - elim H5; intros. - elim a; intro. + unfold is_upper_bound; intros; unfold EUn in H3; destruct H3 as (x1,->). + destruct (lt_eq_lt_dec x1 x) as [[| -> ]|]. replace (sum_f_R0 An x) with (sum_f_R0 An x1 + sum_f_R0 (fun i:nat => An (S x1 + i)%nat) (x - S x1)). pattern (sum_f_R0 An x1) at 1; rewrite <- Rplus_0_r; @@ -47,7 +45,7 @@ Proof. apply tech1; intros; apply H. apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. symmetry ; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r; + pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. replace (sum_f_R0 An x1) with @@ -68,7 +66,7 @@ Proof. pattern 2 at 3; rewrite <- Rmult_1_r; rewrite <- (Rmult_comm 2); apply Rmult_le_compat_l. left; prove_sup0. - left; apply Rplus_lt_reg_r with ((/ 2) ^ S (x1 - S x)). + left; apply Rplus_lt_reg_l with ((/ 2) ^ S (x1 - S x)). replace ((/ 2) ^ S (x1 - S x) + (1 - (/ 2) ^ S (x1 - S x))) with 1; [ idtac | ring ]. rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r; @@ -86,8 +84,8 @@ Proof. apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)). left; apply Rinv_0_lt_compat; prove_sup0. intro; cut (forall n:nat, (n >= x)%nat -> An (S n) < / 2 * An n). - intro; replace (S x + S i)%nat with (S (S x + i)). - apply H6; unfold ge; apply tech8. + intro H4; replace (S x + S i)%nat with (S (S x + i)). + apply H4; unfold ge; apply tech8. apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring. intros; unfold R_dist in H2; apply Rmult_lt_reg_l with (/ An n). apply Rinv_0_lt_compat; apply H. @@ -101,17 +99,17 @@ Proof. unfold Rdiv; reflexivity. left; unfold Rdiv; change (0 < An (S n) * / An n); apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply H ]. - red; intro; assert (H8 := H n); rewrite H7 in H8; + intro H5; assert (H8 := H n); rewrite H5 in H8; elim (Rlt_irrefl _ H8). replace (S x + 0)%nat with (S x); [ reflexivity | ring ]. symmetry ; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. - intro X; elim X; intros. + intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H - | apply p ]. + | apply H1 ]. Defined. Lemma Alembert_C2 : @@ -127,14 +125,12 @@ Proof. intro; cut (forall n:nat, 0 < Wn n). intro; cut (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0). intro; cut (Un_cv (fun n:nat => Rabs (Wn (S n) / Wn n)) 0). - intro; assert (H5 := Alembert_C1 Vn H1 H3). - assert (H6 := Alembert_C1 Wn H2 H4). - elim H5; intros. - elim H6; intros. + intro; pose proof (Alembert_C1 Vn H1 H3) as (x,p). + pose proof (Alembert_C1 Wn H2 H4) as (x0,p0). exists (x - x0); unfold Un_cv; unfold Un_cv in p; unfold Un_cv in p0; intros; cut (0 < eps / 2). - intro; elim (p (eps / 2) H8); clear p; intros. - elim (p0 (eps / 2) H8); clear p0; intros. + intro H6; destruct (p (eps / 2) H6) as (x1,H8). clear p. + destruct (p0 (eps / 2) H6) as (x2,H9). clear p0. set (N := max x1 x2). exists N; intros; replace (sum_f_R0 An n) with (sum_f_R0 Vn n - sum_f_R0 Wn n). @@ -146,9 +142,9 @@ Proof. apply Rabs_triang. rewrite Rabs_Ropp; apply Rlt_le_trans with (eps / 2 + eps / 2). apply Rplus_lt_compat. - unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N; + unfold R_dist in H8; apply H8; unfold ge; apply le_trans with N; [ unfold N; apply le_max_l | assumption ]. - unfold R_dist in H10; apply H10; unfold ge; apply le_trans with N; + unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N; [ unfold N; apply le_max_r | assumption ]. right; symmetry ; apply double_var. symmetry ; apply tech11; intro; unfold Vn, Wn; @@ -315,7 +311,7 @@ Proof. intro; unfold Wn; unfold Rdiv; rewrite <- (Rmult_0_r (/ 2)); rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l. apply Rinv_0_lt_compat; prove_sup0. - apply Rplus_lt_reg_r with (An n); rewrite Rplus_0_r; unfold Rminus; + apply Rplus_lt_reg_l with (An n); rewrite Rplus_0_r; unfold Rminus; rewrite (Rplus_comm (An n)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply Rle_lt_trans with (Rabs (An n)). @@ -325,7 +321,7 @@ Proof. intro; unfold Vn; unfold Rdiv; rewrite <- (Rmult_0_r (/ 2)); rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l. apply Rinv_0_lt_compat; prove_sup0. - apply Rplus_lt_reg_r with (- An n); rewrite Rplus_0_r; unfold Rminus; + apply Rplus_lt_reg_l with (- An n); rewrite Rplus_0_r; unfold Rminus; rewrite (Rplus_comm (- An n)); rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; apply Rle_lt_trans with (Rabs (An n)). @@ -344,9 +340,8 @@ Proof. intros; set (Bn := fun i:nat => An i * x ^ i). cut (forall n:nat, Bn n <> 0). intro; cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0). - intro; assert (H4 := Alembert_C2 Bn H2 H3). - elim H4; intros. - exists x0; unfold Bn in p; apply tech12; assumption. + intro; destruct (Alembert_C2 Bn H2 H3) as (x0,H4). + exists x0; unfold Bn in H4; apply tech12; assumption. unfold Un_cv; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x). intro; elim (H1 (eps / Rabs x) H4); intros. exists x0; intros; unfold R_dist; unfold Rminus; @@ -400,15 +395,14 @@ Theorem Alembert_C3 : Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Pser An x l }. Proof. - intros; case (total_order_T x 0); intro. - elim s; intro. + intros; destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red; intro; rewrite H1 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H1 in Hlt; elim (Rlt_irrefl _ Hlt). apply AlembertC3_step2; assumption. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red; intro; rewrite H1 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). Defined. Lemma Alembert_C4 : @@ -432,9 +426,7 @@ Proof. unfold is_upper_bound; intros; unfold EUn in H6. elim H6; intros. rewrite H7. - assert (H8 := lt_eq_lt_dec x2 x0). - elim H8; intros. - elim a; intro. + destruct (lt_eq_lt_dec x2 x0) as [[| -> ]|]. replace (sum_f_R0 An x0) with (sum_f_R0 An x2 + sum_f_R0 (fun i:nat => An (S x2 + i)%nat) (x0 - S x2)). pattern (sum_f_R0 An x2) at 1; rewrite <- Rplus_0_r. @@ -443,14 +435,14 @@ Proof. apply tech1. intros; apply H. apply Rmult_lt_0_compat. - apply Rinv_0_lt_compat; apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; + apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. apply H. symmetry ; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r; + pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat. - apply Rinv_0_lt_compat; apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; + apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. apply H. replace (sum_f_R0 An x2) with @@ -466,7 +458,7 @@ Proof. left; apply H. rewrite tech3. unfold Rdiv; apply Rmult_le_reg_l with (1 - x). - apply Rplus_lt_reg_r with x; rewrite Rplus_0_r. + apply Rplus_lt_reg_l with x; rewrite Rplus_0_r. replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. do 2 rewrite (Rmult_comm (1 - x)). rewrite Rmult_assoc; rewrite <- Rinv_l_sym. @@ -480,11 +472,11 @@ Proof. elim Hyp; intros; assumption. elim H3; intros; assumption. apply Rminus_eq_contra. - red; intro. - elim H3; intros. + red; intro H10. + elim H3; intros H11 H12. rewrite H10 in H12; elim (Rlt_irrefl _ H12). - red; intro. - elim H3; intros. + red; intro H10. + elim H3; intros H11 H12. rewrite H10 in H12; elim (Rlt_irrefl _ H12). replace (An (S x0)) with (An (S x0 + 0)%nat). apply (tech6 (fun i:nat => An (S x0 + i)%nat) x). @@ -493,7 +485,7 @@ Proof. elim H3; intros; assumption. intro. cut (forall n:nat, (n >= x0)%nat -> An (S n) < x * An n). - intro. + intro H9. replace (S x0 + S i)%nat with (S (S x0 + i)). apply H9. unfold ge. @@ -515,18 +507,18 @@ Proof. apply Rmult_lt_0_compat. apply H. apply Rinv_0_lt_compat; apply H. - red; intro. + red; intro H10. assert (H11 := H n). rewrite H10 in H11; elim (Rlt_irrefl _ H11). replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ]. symmetry ; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. - intro X; elim X; intros. + intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H - | apply p ]. + | apply H1]. Qed. Lemma Alembert_C5 : @@ -586,14 +578,13 @@ Lemma Alembert_C6 : elim X; intros. exists x0. apply tech12; assumption. - case (total_order_T x 0); intro. - elim s; intro. + destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. eapply Alembert_C5 with (k * Rabs x). split. unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H3 in Hlt; elim (Rlt_irrefl _ Hlt). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. @@ -604,7 +595,7 @@ Lemma Alembert_C6 : intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H3 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). @@ -621,7 +612,7 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. @@ -629,7 +620,7 @@ Lemma Alembert_C6 : unfold R_dist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. simpl. @@ -641,14 +632,14 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). apply H0. apply pow_nonzero. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro H7; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). exists (An 0%nat). unfold Un_cv. intros. @@ -661,14 +652,14 @@ Lemma Alembert_C6 : simpl; ring. rewrite tech5. rewrite <- Hrecn. - rewrite b; simpl; ring. + rewrite Heq; simpl; ring. unfold ge; apply le_O_n. eapply Alembert_C5 with (k * Rabs x). split. unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H3 in Hgt; elim (Rlt_irrefl _ Hgt). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. @@ -679,7 +670,7 @@ Lemma Alembert_C6 : intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H3 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). @@ -696,7 +687,7 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. @@ -704,7 +695,7 @@ Lemma Alembert_C6 : unfold R_dist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. simpl. @@ -716,12 +707,12 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). apply H0. apply pow_nonzero. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro H7; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). Qed. |