summaryrefslogtreecommitdiff
path: root/theories/Reals/Alembert.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Alembert.v')
-rw-r--r--theories/Reals/Alembert.v260
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.