diff options
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 260 |
1 files changed, 129 insertions, 131 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 092eafa3..13b33301 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -1,13 +1,11 @@ (************************************************************************) (* 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: Alembert.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. @@ -15,7 +13,7 @@ Require Import SeqProp. Require Import PartSum. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (***************************************************) (* Various versions of the criterion of D'Alembert *) @@ -33,23 +31,23 @@ Proof. { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). intro X; apply X. apply completeness. - unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2); + unfold Un_cv in H0; unfold bound; cut (0 < / 2); [ 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 in |- *; intros; unfold EUn in H3; elim H3; intros. + 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. 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 in |- *; rewrite <- Rplus_0_r; + pattern (sum_f_R0 An x1) at 1; rewrite <- Rplus_0_r; rewrite Rplus_assoc; apply Rplus_le_compat_l. left; apply Rplus_lt_0_compat. apply tech1; intros; apply H. apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. - symmetry in |- *; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x) at 1 in |- *; rewrite <- Rplus_0_r; + symmetry ; apply tech2; assumption. + rewrite b; 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 @@ -66,14 +64,14 @@ Proof. left; apply H. rewrite tech3. replace (1 - / 2) with (/ 2). - unfold Rdiv in |- *; rewrite Rinv_involutive. - pattern 2 at 3 in |- *; rewrite <- Rmult_1_r; rewrite <- (Rmult_comm 2); + unfold Rdiv; rewrite Rinv_involutive. + 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)). replace ((/ 2) ^ S (x1 - S x) + (1 - (/ 2) ^ S (x1 - S x))) with 1; [ idtac | ring ]. - rewrite <- (Rplus_comm 1); pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; + rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. apply pow_lt; apply Rinv_0_lt_compat; prove_sup0. discrR. @@ -82,14 +80,14 @@ Proof. ring. discrR. discrR. - pattern 1 at 3 in |- *; replace 1 with (/ 1); + pattern 1 at 3; replace 1 with (/ 1); [ apply tech7; discrR | apply Rinv_1 ]. replace (An (S x)) with (An (S x + 0)%nat). 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 in |- *; apply tech8. + apply H6; 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. @@ -98,20 +96,20 @@ Proof. rewrite Rmult_1_r; replace (An (S n) * / An n) with (Rabs (Rabs (An (S n) / An n) - 0)). apply H2; assumption. - unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; + unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; rewrite Rabs_right. - unfold Rdiv in |- *; reflexivity. - left; unfold Rdiv in |- *; change (0 < An (S n) * / An n) in |- *; + 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 in |- *; intro; assert (H8 := H n); rewrite H7 in H8; + red; intro; assert (H8 := H n); rewrite H7 in H8; elim (Rlt_irrefl _ H8). replace (S x + 0)%nat with (S x); [ reflexivity | ring ]. - symmetry in |- *; apply tech2; assumption. - exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. + symmetry ; apply tech2; assumption. + exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. intro X; elim X; intros. - exists x; apply tech10; - [ unfold Un_growing in |- *; intro; rewrite tech5; - pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; + 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 ]. Defined. @@ -133,14 +131,14 @@ Proof. assert (H6 := Alembert_C1 Wn H2 H4). elim H5; intros. elim H6; intros. - exists (x - x0); unfold Un_cv in |- *; unfold Un_cv in p; + 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. 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). - unfold R_dist in |- *; + unfold R_dist; replace (sum_f_R0 Vn n - sum_f_R0 Wn n - (x - x0)) with (sum_f_R0 Vn n - x + - (sum_f_R0 Wn n - x0)); [ idtac | ring ]; apply Rle_lt_trans with @@ -148,29 +146,29 @@ 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 in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_l | assumption ]. - unfold R_dist in H10; apply H10; unfold ge in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_r | assumption ]. - right; symmetry in |- *; apply double_var. - symmetry in |- *; apply tech11; intro; unfold Vn, Wn in |- *; - unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ 2)); + unfold R_dist in H9; apply H9; 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 N; apply le_max_r | assumption ]. + right; symmetry ; apply double_var. + symmetry ; apply tech11; intro; unfold Vn, Wn; + unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_eq_reg_l with 2. rewrite Rmult_minus_distr_l; repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. ring. discrR. discrR. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. cut (forall n:nat, / 2 * Rabs (An n) <= Wn n <= 3 * / 2 * Rabs (An n)). intro; cut (forall n:nat, / Wn n <= 2 * / Rabs (An n)). intro; cut (forall n:nat, Wn (S n) / Wn n <= 3 * Rabs (An (S n) / An n)). - intro; unfold Un_cv in |- *; intros; unfold Un_cv in H0; cut (0 < eps / 3). + intro; unfold Un_cv; intros; unfold Un_cv in H0; cut (0 < eps / 3). intro; elim (H0 (eps / 3) H8); intros. exists x; intros. assert (H11 := H9 n H10). - unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; + unfold R_dist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold R_dist in H11; unfold Rminus in H11; rewrite Ropp_0 in H11; rewrite Rplus_0_r in H11; rewrite Rabs_Rabsolu in H11; rewrite Rabs_right. @@ -181,13 +179,13 @@ Proof. rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ]; rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H11; exact H11. - left; change (0 < Wn (S n) / Wn n) in |- *; unfold Rdiv in |- *; + left; change (0 < Wn (S n) / Wn n); unfold Rdiv; apply Rmult_lt_0_compat. apply H2. apply Rinv_0_lt_compat; apply H2. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - intro; unfold Rdiv in |- *; rewrite Rabs_mult; rewrite <- Rmult_assoc; + intro; unfold Rdiv; rewrite Rabs_mult; rewrite <- Rmult_assoc; replace 3 with (2 * (3 * / 2)); [ idtac | rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR ]; apply Rle_trans with (Wn (S n) * 2 * / Rabs (An n)). @@ -220,32 +218,32 @@ Proof. rewrite Rmult_1_l; elim (H4 n); intros; assumption. discrR. apply Rabs_no_R0; apply H. - red in |- *; intro; assert (H6 := H2 n); rewrite H5 in H6; + red; intro; assert (H6 := H2 n); rewrite H5 in H6; elim (Rlt_irrefl _ H6). intro; split. - unfold Wn in |- *; unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + unfold Wn; unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; prove_sup0. - pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r; rewrite double; - unfold Rminus in |- *; rewrite Rplus_assoc; apply Rplus_le_compat_l. + pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; rewrite double; + unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l. apply Rplus_le_reg_l with (An n). rewrite Rplus_0_r; rewrite (Rplus_comm (An n)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply RRle_abs. - unfold Wn in |- *; unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 2)); + unfold Wn; unfold Rdiv; repeat rewrite <- (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc; apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; prove_sup0. - unfold Rminus in |- *; rewrite double; + unfold Rminus; rewrite double; replace (3 * Rabs (An n)) with (Rabs (An n) + Rabs (An n) + Rabs (An n)); [ idtac | ring ]; repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l. rewrite <- Rabs_Ropp; apply RRle_abs. cut (forall n:nat, / 2 * Rabs (An n) <= Vn n <= 3 * / 2 * Rabs (An n)). intro; cut (forall n:nat, / Vn n <= 2 * / Rabs (An n)). intro; cut (forall n:nat, Vn (S n) / Vn n <= 3 * Rabs (An (S n) / An n)). - intro; unfold Un_cv in |- *; intros; unfold Un_cv in H1; cut (0 < eps / 3). + intro; unfold Un_cv; intros; unfold Un_cv in H1; cut (0 < eps / 3). intro; elim (H0 (eps / 3) H7); intros. exists x; intros. assert (H10 := H8 n H9). - unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; + unfold R_dist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold R_dist in H10; unfold Rminus in H10; rewrite Ropp_0 in H10; rewrite Rplus_0_r in H10; rewrite Rabs_Rabsolu in H10; rewrite Rabs_right. @@ -256,13 +254,13 @@ Proof. rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ]; rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H10; exact H10. - left; change (0 < Vn (S n) / Vn n) in |- *; unfold Rdiv in |- *; + left; change (0 < Vn (S n) / Vn n); unfold Rdiv; apply Rmult_lt_0_compat. apply H1. apply Rinv_0_lt_compat; apply H1. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - intro; unfold Rdiv in |- *; rewrite Rabs_mult; rewrite <- Rmult_assoc; + intro; unfold Rdiv; rewrite Rabs_mult; rewrite <- Rmult_assoc; replace 3 with (2 * (3 * / 2)); [ idtac | rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR ]; apply Rle_trans with (Vn (S n) * 2 * / Rabs (An n)). @@ -295,44 +293,44 @@ Proof. rewrite Rmult_1_l; elim (H3 n); intros; assumption. discrR. apply Rabs_no_R0; apply H. - red in |- *; intro; assert (H5 := H1 n); rewrite H4 in H5; + red; intro; assert (H5 := H1 n); rewrite H4 in H5; elim (Rlt_irrefl _ H5). intro; split. - unfold Vn in |- *; unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + unfold Vn; unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; prove_sup0. - pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r; rewrite double; + pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; rewrite double; rewrite Rplus_assoc; apply Rplus_le_compat_l. apply Rplus_le_reg_l with (- An n); rewrite Rplus_0_r; rewrite <- (Rplus_comm (An n)); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite <- Rabs_Ropp; apply RRle_abs. - unfold Vn in |- *; unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 2)); + unfold Vn; unfold Rdiv; repeat rewrite <- (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc; apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; prove_sup0. - unfold Rminus in |- *; rewrite double; + unfold Rminus; rewrite double; replace (3 * Rabs (An n)) with (Rabs (An n) + Rabs (An n) + Rabs (An n)); [ idtac | ring ]; repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l; apply RRle_abs. - intro; unfold Wn in |- *; unfold Rdiv in |- *; rewrite <- (Rmult_0_r (/ 2)); + 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 in |- *; + apply Rplus_lt_reg_r 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)). apply RRle_abs. - rewrite double; pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r; + rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. - intro; unfold Vn in |- *; unfold Rdiv in |- *; rewrite <- (Rmult_0_r (/ 2)); + 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 in |- *; + apply Rplus_lt_reg_r 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)). rewrite <- Rabs_Ropp; apply RRle_abs. - rewrite double; pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r; + rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. Defined. @@ -349,11 +347,11 @@ Proof. intro; assert (H4 := Alembert_C2 Bn H2 H3). elim H4; intros. exists x0; unfold Bn in p; apply tech12; assumption. - unfold Un_cv in |- *; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x). + 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 in |- *; unfold Rminus in |- *; + exists x0; intros; unfold R_dist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; - unfold Bn in |- *; + unfold Bn; replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. @@ -362,22 +360,22 @@ Proof. rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H5; replace (Rabs (An (S n) / An n)) with (R_dist (Rabs (An (S n) * / An n)) 0). apply H5; assumption. - unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold Rdiv in |- *; + unfold R_dist; unfold Rminus; rewrite Ropp_0; + rewrite Rplus_0_r; rewrite Rabs_Rabsolu; unfold Rdiv; reflexivity. apply Rabs_no_R0; assumption. replace (S n) with (n + 1)%nat; [ idtac | ring ]; rewrite pow_add; - unfold Rdiv in |- *; rewrite Rinv_mult_distr. + unfold Rdiv; rewrite Rinv_mult_distr. replace (An (n + 1)%nat * (x ^ n * x ^ 1) * (/ An n * / x ^ n)) with (An (n + 1)%nat * x ^ 1 * / An n * (x ^ n * / x ^ n)); [ idtac | ring ]; rewrite <- Rinv_r_sym. - simpl in |- *; ring. + simpl; ring. apply pow_nonzero; assumption. apply H0. apply pow_nonzero; assumption. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. - intro; unfold Bn in |- *; apply prod_neq_R0; + intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. Defined. @@ -385,14 +383,14 @@ Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. Proof. intros; exists (An 0%nat). - unfold Pser in |- *; unfold infinite_sum in |- *; intros; exists 0%nat; intros; + unfold Pser; unfold infinite_sum; intros; exists 0%nat; intros; replace (sum_f_R0 (fun n0:nat => An n0 * x ^ n0) n) with (An 0%nat). - unfold R_dist in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + unfold R_dist; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. induction n as [| n Hrecn]. - simpl in |- *; ring. + simpl; ring. rewrite tech5; rewrite Hrecn; - [ rewrite H; simpl in |- *; ring | unfold ge in |- *; apply le_O_n ]. + [ rewrite H; simpl; ring | unfold ge; apply le_O_n ]. Qed. (** A useful criterion of convergence for power series *) @@ -406,11 +404,11 @@ Proof. elim s; intro. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red in |- *; intro; rewrite H1 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H1 in a; elim (Rlt_irrefl _ a). apply AlembertC3_step2; assumption. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red in |- *; intro; rewrite H1 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H1 in r; elim (Rlt_irrefl _ r). Defined. Lemma Alembert_C4 : @@ -430,8 +428,8 @@ Proof. elim H1; intros. elim H2; intros. elim H4; intros. - unfold bound in |- *; exists (sum_f_R0 An x0 + / (1 - x) * An (S x0)). - unfold is_upper_bound in |- *; intros; unfold EUn in H6. + unfold bound; exists (sum_f_R0 An x0 + / (1 - x) * An (S x0)). + unfold is_upper_bound; intros; unfold EUn in H6. elim H6; intros. rewrite H7. assert (H8 := lt_eq_lt_dec x2 x0). @@ -439,7 +437,7 @@ Proof. elim a; intro. 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 in |- *; rewrite <- Rplus_0_r. + pattern (sum_f_R0 An x2) at 1; rewrite <- Rplus_0_r. rewrite Rplus_assoc; apply Rplus_le_compat_l. left; apply Rplus_lt_0_compat. apply tech1. @@ -448,8 +446,8 @@ Proof. apply Rinv_0_lt_compat; apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. apply H. - symmetry in |- *; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x0) at 1 in |- *; rewrite <- Rplus_0_r; + symmetry ; apply tech2; assumption. + rewrite b; 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; @@ -467,7 +465,7 @@ Proof. rewrite <- (Rmult_comm (An (S x0))); apply Rmult_le_compat_l. left; apply H. rewrite tech3. - unfold Rdiv in |- *; apply Rmult_le_reg_l with (1 - x). + unfold Rdiv; apply Rmult_le_reg_l with (1 - x). apply Rplus_lt_reg_r with x; rewrite Rplus_0_r. replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. do 2 rewrite (Rmult_comm (1 - x)). @@ -475,17 +473,17 @@ Proof. rewrite Rmult_1_r; apply Rplus_le_reg_l with (x ^ S (x2 - S x0)). replace (x ^ S (x2 - S x0) + (1 - x ^ S (x2 - S x0))) with 1; [ idtac | ring ]. - rewrite <- (Rplus_comm 1); pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; + rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply pow_lt. apply Rle_lt_trans with k. elim Hyp; intros; assumption. elim H3; intros; assumption. apply Rminus_eq_contra. - red in |- *; intro. + red; intro. elim H3; intros. rewrite H10 in H12; elim (Rlt_irrefl _ H12). - red in |- *; intro. + red; intro. elim H3; intros. rewrite H10 in H12; elim (Rlt_irrefl _ H12). replace (An (S x0)) with (An (S x0 + 0)%nat). @@ -498,7 +496,7 @@ Proof. intro. replace (S x0 + S i)%nat with (S (S x0 + i)). apply H9. - unfold ge in |- *. + unfold ge. apply tech8. apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring. @@ -512,21 +510,21 @@ Proof. replace (An (S n) * / An n) with (Rabs (An (S n) / An n)). apply H5; assumption. rewrite Rabs_right. - unfold Rdiv in |- *; reflexivity. - left; unfold Rdiv in |- *; change (0 < An (S n) * / An n) in |- *; + 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 in |- *; intro. + red; intro. assert (H11 := H n). rewrite H10 in H11; elim (Rlt_irrefl _ H11). replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ]. - symmetry in |- *; apply tech2; assumption. - exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. + symmetry ; apply tech2; assumption. + exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. intro X; elim X; intros. - exists x; apply tech10; - [ unfold Un_growing in |- *; intro; rewrite tech5; - pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; + 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 ]. Qed. @@ -553,9 +551,9 @@ Proof. apply (Alembert_C4 (fun i:nat => Rabs (An i)) k). assumption. intro; apply Rabs_pos_lt; apply H0. - unfold Un_cv in |- *. + unfold Un_cv. unfold Un_cv in H1. - unfold Rdiv in |- *. + unfold Rdiv. intros. elim (H1 eps H2); intros. exists x; intros. @@ -592,22 +590,22 @@ Lemma Alembert_C6 : elim s; intro. eapply Alembert_C5 with (k * Rabs x). split. - unfold Rdiv in |- *; apply Rmult_le_pos. + unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red in |- *; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. rewrite Rmult_1_r; assumption. - red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H). + red; intro; rewrite H3 in H; elim (Rlt_irrefl _ H). intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red in |- *; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). - unfold Un_cv in |- *; unfold Un_cv in H1. + red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). intro. @@ -615,7 +613,7 @@ Lemma Alembert_C6 : exists x0. intros. replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). - unfold R_dist in |- *. + unfold R_dist. rewrite Rabs_mult. replace (Rabs (An (S n) / An n) * Rabs x - k * Rabs x) with (Rabs x * (Rabs (An (S n) / An n) - k)); [ idtac | ring ]. @@ -623,18 +621,18 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red in |- *; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. rewrite <- (Rmult_comm eps). unfold R_dist in H5. - unfold Rdiv in |- *; unfold Rdiv in H5; apply H5; assumption. + unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red in |- *; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). - unfold Rdiv in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ]. + red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. - simpl in |- *. + simpl. rewrite Rmult_1_r. rewrite Rinv_mult_distr. replace (An (n + 1)%nat * (x ^ n * x) * (/ An n * / x ^ n)) with @@ -643,46 +641,46 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red in |- *; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). apply H0. apply pow_nonzero. - red in |- *; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). - unfold Rdiv in |- *; apply Rmult_lt_0_compat. + red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red in |- *; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a). exists (An 0%nat). - unfold Un_cv in |- *. + unfold Un_cv. intros. exists 0%nat. intros. - unfold R_dist in |- *. + unfold R_dist. replace (sum_f_R0 (fun i:nat => An i * x ^ i) n) with (An 0%nat). - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. induction n as [| n Hrecn]. - simpl in |- *; ring. + simpl; ring. rewrite tech5. rewrite <- Hrecn. - rewrite b; simpl in |- *; ring. - unfold ge in |- *; apply le_O_n. + rewrite b; simpl; ring. + unfold ge; apply le_O_n. eapply Alembert_C5 with (k * Rabs x). split. - unfold Rdiv in |- *; apply Rmult_le_pos. + unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red in |- *; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. rewrite Rmult_1_r; assumption. - red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H). + red; intro; rewrite H3 in H; elim (Rlt_irrefl _ H). intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red in |- *; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). - unfold Un_cv in |- *; unfold Un_cv in H1. + red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). intro. @@ -690,7 +688,7 @@ Lemma Alembert_C6 : exists x0. intros. replace (An (S n) * x ^ S n / (An n * x ^ n)) with (An (S n) / An n * x). - unfold R_dist in |- *. + unfold R_dist. rewrite Rabs_mult. replace (Rabs (An (S n) / An n) * Rabs x - k * Rabs x) with (Rabs x * (Rabs (An (S n) / An n) - k)); [ idtac | ring ]. @@ -698,18 +696,18 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red in |- *; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. rewrite <- (Rmult_comm eps). unfold R_dist in H5. - unfold Rdiv in |- *; unfold Rdiv in H5; apply H5; assumption. + unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red in |- *; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). - unfold Rdiv in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ]. + red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. - simpl in |- *. + simpl. rewrite Rmult_1_r. rewrite Rinv_mult_distr. replace (An (n + 1)%nat * (x ^ n * x) * (/ An n * / x ^ n)) with @@ -718,12 +716,12 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red in |- *; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). apply H0. apply pow_nonzero. - red in |- *; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). - unfold Rdiv in |- *; apply Rmult_lt_0_compat. + red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red in |- *; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r). Qed. |