diff options
Diffstat (limited to 'theories/Reals')
53 files changed, 325 insertions, 324 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index a691b189..e6bc69b6 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Alembert.v,v 1.14.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Alembert.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -30,7 +30,7 @@ intros An H H0. cut (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). -intro; apply X. +intro X; apply X. apply completeness. unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2); [ intro | apply Rinv_0_lt_compat; prove_sup0 ]. @@ -107,7 +107,7 @@ red in |- *; intro; assert (H8 := H n); rewrite H7 in 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. -intro; elim X; intros. +intro X; elim X; intros. apply existT with x; apply tech10; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; @@ -418,7 +418,7 @@ intros An k Hyp H H0. cut (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). -intro; apply X. +intro X; apply X. apply completeness. assert (H1 := tech13 _ _ Hyp H0). elim H1; intros. @@ -517,7 +517,7 @@ 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. -intro; elim X; intros. +intro X; elim X; intros. apply existT with x; apply tech10; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; @@ -559,11 +559,11 @@ rewrite <- Rabs_mult. rewrite Rabs_Rabsolu. unfold Rdiv in H3; apply H3; assumption. apply H0. -intro. +intro X. elim X; intros. apply existT with x. assumption. -intro. +intro X. elim X; intros. apply existT with x. assumption. @@ -581,7 +581,7 @@ intros. cut (sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)). -intro. +intro X. elim X; intros. apply existT with x0. apply tech12; assumption. @@ -723,4 +723,4 @@ unfold Rdiv in |- *; 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). -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 166a8a46..1ec8c664 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: AltSeries.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: AltSeries.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index ad535a9d..24d64c07 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ArithProp.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: ArithProp.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rbasic_fun. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index e31b623c..940bd628 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Binomial.v,v 1.9.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Binomial.v 6295 2004-11-12 16:40:39Z gregoire $ i*) Require Import Rbase. Require Import Rfunctions. @@ -201,4 +201,4 @@ replace (p - p)%nat with 0%nat; [ idtac | apply minus_n_n ]. replace (INR (fact 0)) with 1; [ idtac | reflexivity ]. rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym; [ reflexivity | apply INR_fact_neq_0 ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 41a6284f..7f3727c7 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Cauchy_prod.v,v 1.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Cauchy_prod.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 422eb4a4..558632c5 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Cos_plus.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Cos_plus.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 9f76a5ad..8320382c 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Cos_rel.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Cos_rel.v 6245 2004-10-20 13:50:08Z barras $ i*) Require Import Rbase. Require Import Rfunctions. @@ -417,4 +417,4 @@ unfold sin_in in s. assert (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s). rewrite H1; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index f897e258..1c663288 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: DiscrR.v,v 1.21.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: DiscrR.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import RIneq. Require Import Omega. Open Local Scope R_scope. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index fcaeb11e..90ea93ef 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Exp_prop.v,v 1.16.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Exp_prop.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -895,7 +895,7 @@ cut Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)). -intro. +intro X. elim X; intros. exists x; intros. split. @@ -1008,4 +1008,4 @@ rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rmult_assoc; rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; rewrite exp_plus; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v index c3c3d9bb..d4f3a8ec 100644 --- a/theories/Reals/Integration.v +++ b/theories/Reals/Integration.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Integration.v,v 1.1.6.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: Integration.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Export NewtonInt. Require Export RiemannInt_SF. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index baa61304..241313a0 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: MVT.v,v 1.10.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: MVT.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -27,7 +27,7 @@ Theorem MVT : intros; assert (H2 := Rlt_le _ _ H). set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). cut (forall c:R, a < c < b -> derivable_pt h c). -intro; cut (forall c:R, a <= c <= b -> continuity_pt h c). +intro X; cut (forall c:R, a <= c <= b -> continuity_pt h c). intro; assert (H4 := continuity_ab_maj h a b H2 H3). assert (H5 := continuity_ab_min h a b H2 H3). elim H4; intros Mx H6. @@ -142,9 +142,9 @@ Lemma MVT_cor1 : a < b -> exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b. intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c); - [ intro | intros; apply pr ]. + [ intro X | intros; apply pr ]. cut (forall c:R, a < c < b -> derivable_pt id c); - [ intro | intros; apply derivable_pt_id ]. + [ intro X0 | intros; apply derivable_pt_id ]. cut (forall c:R, a <= c <= b -> continuity_pt f c); [ intro | intros; apply derivable_continuous_pt; apply pr ]. cut (forall c:R, a <= c <= b -> continuity_pt id c); @@ -166,11 +166,11 @@ Theorem MVT_cor2 : (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) -> exists c : R, f b - f a = f' c * (b - a) /\ a < c < b. intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c). -intro; cut (forall c:R, a < c < b -> derivable_pt f c). -intro; cut (forall c:R, a <= c <= b -> continuity_pt f c). +intro X; cut (forall c:R, a < c < b -> derivable_pt f c). +intro X0; cut (forall c:R, a <= c <= b -> continuity_pt f c). intro; cut (forall c:R, a <= c <= b -> derivable_pt id c). -intro; cut (forall c:R, a < c < b -> derivable_pt id c). -intro; cut (forall c:R, a <= c <= b -> continuity_pt id c). +intro X1; cut (forall c:R, a < c < b -> derivable_pt id c). +intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c). intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros; exists x; split. cut (derive_pt id x (X2 x x0) = 1). @@ -595,7 +595,7 @@ Lemma IAF_var : g b - g a <= f b - f a. intros. cut (derivable (g - f)). -intro. +intro X. cut (forall c:R, a <= c <= b -> derive_pt (g - f) c (X c) <= 0). intro. assert (H2 := IAF (g - f)%F a b 0 X H H1). diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 97cd4b94..62c53e6d 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: NewtonInt.v,v 1.11.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: NewtonInt.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -128,7 +128,8 @@ Lemma NewtonInt_P5 : Newton_integrable f a b -> Newton_integrable g a b -> Newton_integrable (fun x:R => l * f x + g x) a b. -unfold Newton_integrable in |- *; intros; elim X; intros; elim X0; intros; +unfold Newton_integrable in |- *; intros f g l a b X X0; + elim X; intros; elim X0; intros; exists (fun y:R => l * x y + x0 y). elim p; intro. elim p0; intro. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 0c19c8da..d6dc352c 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PSeries_reg.v,v 1.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) +(*i $Id: PSeries_reg.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 6087d3f2..bace7b9d 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*) +(*i $Id: PartSum.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -430,7 +430,7 @@ Lemma cv_cauchy_1 : forall An:nat -> R, sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) -> Cauchy_crit_series An. -intros. +intros An X. elim X; intros. unfold Un_cv in p. unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 5da14193..3e1dbccf 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RIneq.v,v 1.23.2.2 2005/03/29 15:35:13 herbelin Exp $ i*) +(*i $Id: RIneq.v 6897 2005-03-29 15:39:12Z herbelin $ i*) (***************************************************************************) (** Basic lemmas for the classical reals numbers *) diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 3b58c02f..551aec98 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RList.v,v 1.10.2.1 2004/07/16 19:31:11 herbelin Exp $ i*) +(*i $Id: RList.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 289b1921..97355238 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_Ifp.v,v 1.14.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: R_Ifp.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (**********************************************************) (** Complements for the reals.Integer and fractional part *) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 0abf9064..d87adc24 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqr.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: R_sqr.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rbasic_fun. Open Local Scope R_scope. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 660b0527..cb372840 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqrt.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: R_sqrt.v 6295 2004-11-12 16:40:39Z gregoire $ i*) Require Import Rbase. Require Import Rfunctions. @@ -396,4 +396,4 @@ unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse. rewrite Ropp_minus_distr. reflexivity. reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 88af8b20..b885e4ce 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 918ebfc0..6d30e291 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis1.v,v 1.21.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis1.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -453,7 +453,7 @@ Qed. Theorem derivable_continuous_pt : forall f (x:R), derivable_pt f x -> continuity_pt f x. -intros. +intros f x X. generalize (derivable_derive f x X); intro. elim H; intros l H1. cut (l = fct_cte l x). @@ -468,7 +468,7 @@ unfold fct_cte in |- *; reflexivity. Qed. Theorem derivable_continuous : forall f, derivable f -> continuity f. -unfold derivable, continuity in |- *; intros. +unfold derivable, continuity in |- *; intros f X x. apply (derivable_continuous_pt f x (X x)). Qed. @@ -661,7 +661,7 @@ Qed. Lemma derivable_pt_plus : forall f1 f2 (x:R), derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. apply existT with (x0 + x1). @@ -670,7 +670,7 @@ Qed. Lemma derivable_pt_opp : forall f (x:R), derivable_pt f x -> derivable_pt (- f) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f x X. elim X; intros. apply existT with (- x0). apply derivable_pt_lim_opp; assumption. @@ -679,7 +679,7 @@ Qed. Lemma derivable_pt_minus : forall f1 f2 (x:R), derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 - f2) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. apply existT with (x0 - x1). @@ -689,7 +689,7 @@ Qed. Lemma derivable_pt_mult : forall f1 f2 (x:R), derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 * f2) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. apply existT with (x0 * f2 x + f1 x * x1). @@ -704,7 +704,7 @@ Qed. Lemma derivable_pt_scal : forall f (a x:R), derivable_pt f x -> derivable_pt (mult_real_fct a f) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f1 a x X. elim X; intros. apply existT with (a * x0). apply derivable_pt_lim_scal; assumption. @@ -724,7 +724,7 @@ Qed. Lemma derivable_pt_comp : forall f1 f2 (x:R), derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x. -unfold derivable_pt in |- *; intros. +unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. apply existT with (x1 * x0). @@ -733,24 +733,24 @@ Qed. Lemma derivable_plus : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 x. apply (derivable_pt_plus _ _ x (X _) (X0 _)). Qed. Lemma derivable_opp : forall f, derivable f -> derivable (- f). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f X x. apply (derivable_pt_opp _ x (X _)). Qed. Lemma derivable_minus : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 x. apply (derivable_pt_minus _ _ x (X _) (X0 _)). Qed. Lemma derivable_mult : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 * f2). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 x. apply (derivable_pt_mult _ _ x (X _) (X0 _)). Qed. @@ -761,7 +761,7 @@ Qed. Lemma derivable_scal : forall f (a:R), derivable f -> derivable (mult_real_fct a f). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f a X x. apply (derivable_pt_scal _ a x (X _)). Qed. @@ -775,7 +775,7 @@ Qed. Lemma derivable_comp : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f2 o f1). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 x. apply (derivable_pt_comp _ _ x (X _) (X0 _)). Qed. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 35f7eab8..0627e22c 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis2.v,v 1.11.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis2.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 9f85b00a..663ccb07 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis3.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis3.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -20,9 +20,9 @@ Theorem derivable_pt_lim_div : derivable_pt_lim f2 x l2 -> f2 x <> 0 -> derivable_pt_lim (f1 / f2) x ((l1 * f2 x - l2 * f1 x) / Rsqr (f2 x)). -intros. +intros f1 f2 x l1 l2 H H0 H1. cut (derivable_pt f2 x); - [ intro | unfold derivable_pt in |- *; apply existT with l2; exact H0 ]. + [ intro X | unfold derivable_pt in |- *; apply existT with l2; exact H0 ]. assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1). elim H2; clear H2; intros eps_f2 H2. unfold div_fct in |- *. @@ -756,7 +756,7 @@ Lemma derivable_pt_div : derivable_pt f1 x -> derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x. unfold derivable_pt in |- *. -intros. +intros f1 f2 x X X0 H. elim X; intros. elim X0; intros. apply existT with ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)). @@ -767,7 +767,7 @@ Lemma derivable_div : forall f1 f2:R -> R, derivable f1 -> derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2). -unfold derivable in |- *; intros. +unfold derivable in |- *; intros f1 f2 X X0 H x. apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)). Qed. @@ -790,4 +790,4 @@ unfold derive_pt in H; rewrite H in H3. assert (H4 := projT2 pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_div; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 86f49cd4..40bb2429 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis4.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Ranalysis4.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -20,13 +20,13 @@ Require Import Exp_prop. Open Local Scope R_scope. Lemma derivable_pt_inv : forall (f:R -> R) (x:R), f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x. -intros; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). -intro; apply X0. +intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x). +intro X0; apply X0. apply derivable_pt_div. apply derivable_pt_const. assumption. assumption. -unfold div_fct, inv_fct, fct_cte in |- *; intro; elim X0; intros; +unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros; unfold derivable_pt in |- *; apply existT with x0; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; @@ -76,8 +76,8 @@ Qed. (**********) Lemma derivable_inv : forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f). -intros. -unfold derivable in |- *; intro. +intros f H X. +unfold derivable in |- *; intro x. apply derivable_pt_inv. apply (H x). apply (X x). @@ -381,4 +381,4 @@ Lemma derive_pt_sinh : forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x. intro; apply derive_pt_eq_0. apply derivable_pt_lim_sinh. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index bef9f89c..61902568 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Raxioms.v,v 1.20.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Raxioms.v 6338 2004-11-22 09:10:51Z gregoire $ i*) (*********************************************************) (** Axiomatisation of the classical reals *) @@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) (**********) -Fixpoint INR (n:nat) : R := +Boxed Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 773819a2..5bfb692a 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rbase.v,v 1.39.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rbase.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Export Rdefinitions. Require Export Raxioms. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 49ba48f7..436a8011 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rbasic_fun.v,v 1.22.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rbasic_fun.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (*********************************************************) (** Complements for the real numbers *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index dd8379cb..2f11a404 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rcomplete.v,v 1.10.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rcomplete.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 33f494df..62aec6bc 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rdefinitions.v,v 1.14.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rdefinitions.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (*********************************************************) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 81db80ab..42663de6 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rderiv.v,v 1.15.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rderiv.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (*********************************************************) (** Definition of the derivative,continuity *) diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 5e4b3e7b..c9cd189d 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Reals.v,v 1.24.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Reals.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (* The library REALS is divided in 6 parts : - Rbase: basic lemmas on R diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index cdff9fcb..0ab93229 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rfunctions.v,v 1.31.2.1 2004/07/16 19:31:12 herbelin Exp $ i*) +(*i $Id: Rfunctions.v 6338 2004-11-22 09:10:51Z gregoire $ i*) (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) @@ -63,7 +63,7 @@ Qed. (* Power *) (*******************************) (*********) -Fixpoint pow (r:R) (n:nat) {struct n} : R := +Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := match n with | O => 1 | S n => r * pow r n @@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** Sum of n first naturals *) (*******************************) (*********) -Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index a01e7b52..9ce20839 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rgeom.v,v 1.13.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rgeom.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index ce33afdb..79cb7797 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt.v,v 1.18.2.2 2005/07/13 23:18:52 herbelin Exp $ i*) +(*i $Id: RiemannInt.v 7223 2005-07-13 23:43:54Z herbelin $ i*) Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 0ae8f9f2..71ab0b4c 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt_SF.v,v 1.16.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: RiemannInt_SF.v 6338 2004-11-22 09:10:51Z gregoire $ i*) Require Import Rbase. Require Import Rfunctions. @@ -147,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := | existT a b => a end. -Fixpoint Int_SF (l k:Rlist) {struct l} : R := +Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := match l with | nil => 0 | cons a l' => diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 0fbb17c6..b8d304b1 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rlimit.v,v 1.23.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rlimit.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (*********************************************************) (* Definition of the limit *) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 7575d929..aa9e9887 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rpower.v,v 1.17.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rpower.v 6295 2004-11-12 16:40:39Z gregoire $ i*) (*i Due to L.Thery i*) (************************************************************) @@ -658,4 +658,4 @@ apply derivable_pt_lim_const with (a := y). apply derivable_pt_lim_id. ring. apply derivable_pt_lim_exp. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 6577146f..ec738996 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rprod.v,v 1.10.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rprod.v 6338 2004-11-22 09:10:51Z gregoire $ i*) Require Import Compare. Require Import Rbase. @@ -17,7 +17,7 @@ Require Import Binomial. Open Local Scope R_scope. (* TT Ak; 1<=k<=N *) -Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := +Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := match N with | O => 1 | S p => prod_f_SO An p * An (S p) @@ -188,4 +188,4 @@ rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0. apply prod_neq_R0; apply INR_fact_neq_0. apply INR_eq; rewrite minus_INR; [ rewrite mult_INR; do 2 rewrite S_INR; ring | apply le_n_2n ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index cbf93278..aa3a0316 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rseries.v,v 1.11.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rseries.v 6338 2004-11-22 09:10:51Z gregoire $ i*) Require Import Rbase. Require Import Rfunctions. @@ -28,7 +28,7 @@ Section sequence. Variable Un : nat -> R. (*********) -Fixpoint Rmax_N (N:nat) : R := +Boxed Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index e54c3675..1e69a8f5 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rsigma.v,v 1.12.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rsigma.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 459f2716..de3422e8 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rsqrt_def.v,v 1.14.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rsqrt_def.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Sumbool. Require Import Rbase. @@ -15,7 +15,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Open Local Scope R_scope. -Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := +Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => @@ -455,7 +455,7 @@ cut (x <= y). intro. generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). -intros. +intros X X0. elim X; intros. elim X0; intros. assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). @@ -759,4 +759,4 @@ apply Rsqr_inj. assumption. assumption. rewrite <- H0; rewrite <- H2; reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 1c112bf1..84f3b081 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtopology.v,v 1.19.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) +(*i $Id: Rtopology.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index e4cae6c6..060070c4 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo.v,v 1.40.2.1 2004/07/16 19:31:14 herbelin Exp $ i*) +(*i $Id: Rtrigo.v 6245 2004-10-20 13:50:08Z barras $ i*) Require Import Rbase. Require Import Rfunctions. @@ -1704,4 +1704,4 @@ Lemma cos_eq_0_2PI_1 : intros x H1 H2 H3; elim H3; intro H4; [ rewrite H4; rewrite cos_PI2; reflexivity | rewrite H4; rewrite cos_3PI2; reflexivity ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 3cda9290..fc465bc4 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_alt.v,v 1.16.2.1 2004/07/16 19:31:14 herbelin Exp $ i*) +(*i $Id: Rtrigo_alt.v 6245 2004-10-20 13:50:08Z barras $ i*) Require Import Rbase. Require Import Rfunctions. @@ -423,4 +423,4 @@ intros; unfold cos_approx in |- *; apply sum_eq; intros; unfold cos_term in |- *; do 2 rewrite pow_Rsqr; rewrite Rsqr_neg; unfold Rdiv in |- *; reflexivity. apply Ropp_0_gt_lt_contravar; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 0ef87322..f8c15667 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_calc.v,v 1.15.2.1 2004/07/16 19:31:14 herbelin Exp $ i*) +(*i $Id: Rtrigo_calc.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 92ec68ce..94f5ec97 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_def.v,v 1.17.2.1 2004/07/16 19:31:14 herbelin Exp $ i*) +(*i $Id: Rtrigo_def.v 6295 2004-11-12 16:40:39Z gregoire $ i*) Require Import Rbase. Require Import Rfunctions. @@ -409,4 +409,4 @@ apply H. exact (projT2 exist_cos0). assert (H := projT2 (exist_cos (Rsqr 0))); unfold cos in |- *; pattern 0 at 1 in |- *; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index b0f29e5c..eaf2121e 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_fun.v,v 1.7.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: Rtrigo_fun.v 8691 2006-04-10 09:23:37Z msozeau $ i*) Require Import Rbase. Require Import Rfunctions. @@ -61,10 +61,10 @@ intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros; rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0). intro; rewrite (Rabs_pos_eq (/ INR (S n))). cut (/ eps - 1 < INR x). -intro; +intro ; generalize (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4 - (le_INR x n ((fun (n m:nat) (H:(m >= n)%nat) => H) x n H2))); + (le_INR x n H2)); clear H4; intro; unfold Rminus in H4; generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4); replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ]. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 9d3b60c6..1c9a9445 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_reg.v,v 1.15.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: Rtrigo_reg.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -32,7 +32,7 @@ cut (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) n) l)). -intro; elim X; intros. +intro X; elim X; intros. apply existT with x. split. apply p. @@ -206,7 +206,7 @@ cut sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n) l)). -intro; elim X; intros. +intro X; elim X; intros. apply existT with x. split. apply p. @@ -605,4 +605,4 @@ Lemma derive_pt_cos : forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x. intros; apply derive_pt_eq_0. apply derivable_pt_lim_cos. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 34f9fd72..2e851b13 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: SeqProp.v,v 1.13.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) + +(*i $Id: SeqProp.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -48,7 +48,7 @@ cut (~ (forall N:nat, Un N <= x - eps)). intro H6; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)). intro H7; apply H6; intro N; apply Rnot_lt_le; apply H7. intro H7; generalize (Un_bound_imp Un (x - eps) H7); intro H8; - unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); + unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); apply Rlt_not_le; apply tech_Rgt_minus; exact H1. Qed. @@ -66,12 +66,12 @@ Lemma decreasing_cv : Un_decreasing Un -> has_lb Un -> sigT (fun l:R => Un_cv Un l). intros. cut (sigT (fun l:R => Un_cv (opp_seq Un) l) -> sigT (fun l:R => Un_cv Un l)). -intro. +intro X. apply X. apply growing_cv. apply decreasing_growing; assumption. exact H0. -intro. +intro X. elim X; intros. apply existT with (- x). unfold Un_cv in p. @@ -155,14 +155,14 @@ elim H1; intros. exists (k + x1)%nat; assumption. Qed. -Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) +Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) (i:nat) : R := majorant (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr). -Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) +Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) (i:nat) : R := minorant (fun k:nat => Un (i + k)%nat) (min_ss Un i pr). Lemma Wn_decreasing : - forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). + forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). intros. unfold Un_decreasing in |- *. intro. @@ -289,14 +289,14 @@ Qed. (**********) Lemma Vn_Un_Wn_order : - forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) - (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. + forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) + (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. intros. split. unfold sequence_minorant in |- *. cut (sigT (fun l:R => is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l)). -intro. +intro X. elim X; intros. replace (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x). unfold is_lub in p. @@ -329,7 +329,7 @@ apply min_inf. apply min_ss; assumption. unfold sequence_majorant in |- *. cut (sigT (fun l:R => is_lub (EUn (fun i:nat => Un (n + i)%nat)) l)). -intro. +intro X. elim X; intros. replace (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x. unfold is_lub in p. @@ -379,7 +379,7 @@ Qed. Lemma maj_min : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un), - has_lb (sequence_majorant Un pr1). + has_lb (sequence_majorant Un pr1). intros. assert (H := Vn_Un_Wn_order Un pr1 pr2). unfold has_lb in |- *. @@ -486,7 +486,7 @@ Qed. Lemma not_Rlt : forall r1 r2:R, ~ r1 < r2 -> r1 >= r2. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rge in |- *. tauto. -Qed. +Qed. (**********) Lemma approx_maj : @@ -628,234 +628,234 @@ assert (H2 := H1 n). apply not_Rlt; assumption. Qed. -(* Unicity of limit for convergent sequences *) +(* Unicity of limit for convergent sequences *) Lemma UL_sequence : - forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2. -intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros. -apply cond_eq. + forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2. +intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros. +apply cond_eq. intros; cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (H (eps / 2) H2); intros. -elim (H0 (eps / 2) H2); intros. -set (N := max x x0). -apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (H (eps / 2) H2); intros. +elim (H0 (eps / 2) H2); intros. +set (N := max x x0). +apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). replace (l1 - l2) with (l1 - Un N + (Un N - l2)); - [ apply Rabs_triang | ring ]. -rewrite (double_var eps); apply Rplus_lt_compat. + [ apply Rabs_triang | ring ]. +rewrite (double_var eps); apply Rplus_lt_compat. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H3; - unfold ge, N in |- *; apply le_max_l. -apply H4; unfold ge, N in |- *; apply le_max_r. + unfold ge, N in |- *; apply le_max_l. +apply H4; unfold ge, N in |- *; apply le_max_r. Qed. -(**********) +(**********) Lemma CV_plus : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2). -unfold Un_cv in |- *; unfold R_dist in |- *; intros. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2). +unfold Un_cv in |- *; unfold R_dist in |- *; intros. cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (H (eps / 2) H2); intros. -elim (H0 (eps / 2) H2); intros. -set (N := max x x0). -exists N; intros. + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (H (eps / 2) H2); intros. +elim (H0 (eps / 2) H2); intros. +set (N := max x x0). +exists N; intros. replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2)); - [ idtac | ring ]. -apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). -apply Rabs_triang. -rewrite (double_var eps); apply Rplus_lt_compat. + [ idtac | ring ]. +apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). +apply Rabs_triang. +rewrite (double_var eps); apply Rplus_lt_compat. apply H3; unfold ge in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_l | assumption ]. + [ unfold N in |- *; apply le_max_l | assumption ]. apply H4; unfold ge in |- *; apply le_trans with N; - [ unfold N in |- *; apply le_max_r | assumption ]. + [ unfold N in |- *; apply le_max_r | assumption ]. Qed. -(**********) +(**********) Lemma cv_cvabs : forall (Un:nat -> R) (l:R), - Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l). -unfold Un_cv in |- *; unfold R_dist in |- *; intros. -elim (H eps H0); intros. -exists x; intros. -apply Rle_lt_trans with (Rabs (Un n - l)). -apply Rabs_triang_inv2. -apply H1; assumption. -Qed. + Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l). +unfold Un_cv in |- *; unfold R_dist in |- *; intros. +elim (H eps H0); intros. +exists x; intros. +apply Rle_lt_trans with (Rabs (Un n - l)). +apply Rabs_triang_inv2. +apply H1; assumption. +Qed. -(**********) +(**********) Lemma CV_Cauchy : - forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. -intros; elim X; intros. -unfold Cauchy_crit in |- *; intros. -unfold Un_cv in p; unfold R_dist in p. + forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. +intros Un X; elim X; intros. +unfold Cauchy_crit in |- *; intros. +unfold Un_cv in p; unfold R_dist in p. cut (0 < eps / 2); [ intro | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. -elim (p (eps / 2) H0); intros. -exists x0; intros. + [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. +elim (p (eps / 2) H0); intros. +exists x0; intros. unfold R_dist in |- *; - apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). + apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). replace (Un n - Un m) with (Un n - x + (x - Un m)); - [ apply Rabs_triang | ring ]. -rewrite (double_var eps); apply Rplus_lt_compat. -apply H1; assumption. -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. -Qed. + [ apply Rabs_triang | ring ]. +rewrite (double_var eps); apply Rplus_lt_compat. +apply H1; assumption. +rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. +Qed. (**********) Lemma maj_by_pos : forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> - exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). -intros; elim X; intros. -cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). -intro. -assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). -assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). -elim H0; intros. -exists (x0 + 1). -cut (0 <= x0). -intro. -split. -apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. -intros. -apply Rle_trans with x0. -unfold is_upper_bound in H1. -apply H1. -exists n; reflexivity. + exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). +intros Un X; elim X; intros. +cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). +intro X0. +assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). +assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). +elim H0; intros. +exists (x0 + 1). +cut (0 <= x0). +intro. +split. +apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. +intros. +apply Rle_trans with x0. +unfold is_upper_bound in H1. +apply H1. +exists n; reflexivity. pattern x0 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; - apply Rlt_0_1. -apply Rle_trans with (Rabs (Un 0%nat)). -apply Rabs_pos. -unfold is_upper_bound in H1. -apply H1. -exists 0%nat; reflexivity. -apply existT with (Rabs x). -apply cv_cvabs; assumption. -Qed. - -(**********) + apply Rlt_0_1. +apply Rle_trans with (Rabs (Un 0%nat)). +apply Rabs_pos. +unfold is_upper_bound in H1. +apply H1. +exists 0%nat; reflexivity. +apply existT with (Rabs x). +apply cv_cvabs; assumption. +Qed. + +(**********) Lemma CV_mult : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). -intros. -cut (sigT (fun l:R => Un_cv An l)). -intro. -assert (H1 := maj_by_pos An X). -elim H1; intros M H2. -elim H2; intros. -unfold Un_cv in |- *; unfold R_dist in |- *; intros. -cut (0 < eps / (2 * M)). -intro. -case (Req_dec l2 0); intro. -unfold Un_cv in H0; unfold R_dist in H0. -elim (H0 (eps / (2 * M)) H6); intros. -exists x; intros. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). +intros. +cut (sigT (fun l:R => Un_cv An l)). +intro X. +assert (H1 := maj_by_pos An X). +elim H1; intros M H2. +elim H2; intros. +unfold Un_cv in |- *; unfold R_dist in |- *; intros. +cut (0 < eps / (2 * M)). +intro. +case (Req_dec l2 0); intro. +unfold Un_cv in H0; unfold R_dist in H0. +elim (H0 (eps / (2 * M)) H6); intros. +exists x; intros. apply Rle_lt_trans with - (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). + (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)); - [ apply Rabs_triang | ring ]. + [ apply Rabs_triang | ring ]. replace (Rabs (An n * Bn n - An n * l2)) with - (Rabs (An n) * Rabs (Bn n - l2)). -replace (Rabs (An n * l2 - l1 * l2)) with 0. -rewrite Rplus_0_r. -apply Rle_lt_trans with (M * Rabs (Bn n - l2)). -do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). -apply Rmult_le_compat_l. -apply Rabs_pos. -apply H4. -apply Rmult_lt_reg_l with (/ M). -apply Rinv_0_lt_compat; apply H3. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). -apply Rlt_trans with (eps / (2 * M)). -apply H8; assumption. -unfold Rdiv in |- *; rewrite Rinv_mult_distr. -apply Rmult_lt_reg_l with 2. + (Rabs (An n) * Rabs (Bn n - l2)). +replace (Rabs (An n * l2 - l1 * l2)) with 0. +rewrite Rplus_0_r. +apply Rle_lt_trans with (M * Rabs (Bn n - l2)). +do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). +apply Rmult_le_compat_l. +apply Rabs_pos. +apply H4. +apply Rmult_lt_reg_l with (/ M). +apply Rinv_0_lt_compat; apply H3. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). +apply Rlt_trans with (eps / (2 * M)). +apply H8; assumption. +unfold Rdiv in |- *; rewrite Rinv_mult_distr. +apply Rmult_lt_reg_l with 2. prove_sup0. replace (2 * (eps * (/ 2 * / M))) with (2 * / 2 * (eps * / M)); - [ idtac | ring ]. -rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; rewrite double. -pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r. + [ idtac | ring ]. +rewrite <- Rinv_r_sym. +rewrite Rmult_1_l; rewrite double. +pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l; apply Rmult_lt_0_compat; - [ assumption | apply Rinv_0_lt_compat; assumption ]. -discrR. -discrR. -red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). -red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). + [ assumption | apply Rinv_0_lt_compat; assumption ]. +discrR. +discrR. +red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). +red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). rewrite H7; do 2 rewrite Rmult_0_r; unfold Rminus in |- *; - rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. -replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ]. -symmetry in |- *; apply Rabs_mult. -cut (0 < eps / (2 * Rabs l2)). -intro. + rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. +replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ]. +symmetry in |- *; apply Rabs_mult. +cut (0 < eps / (2 * Rabs l2)). +intro. unfold Un_cv in H; unfold R_dist in H; unfold Un_cv in H0; - unfold R_dist in H0. -elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. -elim (H0 (eps / (2 * M)) H6); intros N2 H10. -set (N := max N1 N2). -exists N; intros. + unfold R_dist in H0. +elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. +elim (H0 (eps / (2 * M)) H6); intros N2 H10. +set (N := max N1 N2). +exists N; intros. apply Rle_lt_trans with - (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). + (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). replace (An n * Bn n - l1 * l2) with (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2)); - [ apply Rabs_triang | ring ]. + [ apply Rabs_triang | ring ]. replace (Rabs (An n * Bn n - An n * l2)) with - (Rabs (An n) * Rabs (Bn n - l2)). -replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). -rewrite (double_var eps); apply Rplus_lt_compat. -apply Rle_lt_trans with (M * Rabs (Bn n - l2)). -do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). -apply Rmult_le_compat_l. -apply Rabs_pos. -apply H4. -apply Rmult_lt_reg_l with (/ M). -apply Rinv_0_lt_compat; apply H3. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). -apply Rlt_le_trans with (eps / (2 * M)). -apply H10. -unfold ge in |- *; apply le_trans with N. -unfold N in |- *; apply le_max_r. -assumption. -unfold Rdiv in |- *; rewrite Rinv_mult_distr. -right; ring. -discrR. -red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). -red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). -apply Rmult_lt_reg_l with (/ Rabs l2). -apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. -rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). -apply H9. -unfold ge in |- *; apply le_trans with N. -unfold N in |- *; apply le_max_l. -assumption. -unfold Rdiv in |- *; right; rewrite Rinv_mult_distr. -ring. -discrR. -apply Rabs_no_R0; assumption. -apply Rabs_no_R0; assumption. + (Rabs (An n) * Rabs (Bn n - l2)). +replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). +rewrite (double_var eps); apply Rplus_lt_compat. +apply Rle_lt_trans with (M * Rabs (Bn n - l2)). +do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). +apply Rmult_le_compat_l. +apply Rabs_pos. +apply H4. +apply Rmult_lt_reg_l with (/ M). +apply Rinv_0_lt_compat; apply H3. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). +apply Rlt_le_trans with (eps / (2 * M)). +apply H10. +unfold ge in |- *; apply le_trans with N. +unfold N in |- *; apply le_max_r. +assumption. +unfold Rdiv in |- *; rewrite Rinv_mult_distr. +right; ring. +discrR. +red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). +red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). +apply Rmult_lt_reg_l with (/ Rabs l2). +apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. +rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). +apply H9. +unfold ge in |- *; apply le_trans with N. +unfold N in |- *; apply le_max_l. +assumption. +unfold Rdiv in |- *; right; rewrite Rinv_mult_distr. +ring. +discrR. +apply Rabs_no_R0; assumption. +apply Rabs_no_R0; assumption. replace (An n * l2 - l1 * l2) with (l2 * (An n - l1)); - [ symmetry in |- *; apply Rabs_mult | ring ]. + [ symmetry in |- *; apply Rabs_mult | ring ]. replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); - [ symmetry in |- *; apply Rabs_mult | ring ]. -unfold Rdiv in |- *; apply Rmult_lt_0_compat. -assumption. + [ symmetry in |- *; apply Rabs_mult | ring ]. +unfold Rdiv in |- *; apply Rmult_lt_0_compat. +assumption. apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; - [ prove_sup0 | apply Rabs_pos_lt; assumption ]. + [ prove_sup0 | apply Rabs_pos_lt; assumption ]. unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; - [ prove_sup0 | assumption ] ]. -apply existT with l1; assumption. -Qed. + [ prove_sup0 | assumption ] ]. +apply existT with l1; assumption. +Qed. Lemma tech9 : forall Un:nat -> R, @@ -905,13 +905,13 @@ rewrite b; assumption. cut (forall n:nat, Un n <= x0). intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros. cut (forall y:R, EUn Un y -> y <= x0). -intro; assert (H8 := H6 _ H7). +intro; assert (H8 := H6 _ H7). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 r)). unfold EUn in |- *; intros; elim H7; intros. rewrite H8; apply H4. intro; case (Rle_dec (Un n) x0); intro. assumption. -cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0). +cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0). intro; unfold Un_cv in H3; cut (0 < Un n - x0). intro; elim (H3 (Un n - x0) H5); intros. cut (max n x1 >= x1)%nat. @@ -931,7 +931,7 @@ left; assumption. unfold ge in |- *; apply le_max_r. apply Rplus_lt_reg_r with x0. rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm x0); - rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; + rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H4; apply le_n. intros; apply Rlt_le_trans with (Un n). case (Rlt_le_dec x0 (Un n)); intro. @@ -977,7 +977,7 @@ unfold R_dist in H4; rewrite <- Rabs_Rabsolu; apply Rabs_triang. rewrite (Rabs_right k). apply Rplus_lt_reg_r with (- k); rewrite <- (Rplus_comm k); - repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; + repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; repeat rewrite Rplus_0_l; apply H4. apply Rle_ge; elim H; intros; assumption. unfold Rdiv in |- *; apply Rmult_lt_0_compat. @@ -989,7 +989,7 @@ Qed. (**********) Lemma growing_ineq : forall (Un:nat -> R) (l:R), - Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. + Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. intros; case (total_order_T (Un n) l); intro. elim s; intro. left; assumption. @@ -1042,14 +1042,14 @@ Qed. (**********) Lemma CV_minus : forall (An Bn:nat -> R) (l1 l2:R), - Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2). -intros. -replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). -unfold Rminus in |- *; apply CV_plus. -assumption. -apply CV_opp; assumption. -unfold Rminus, opp_seq in |- *; reflexivity. -Qed. + Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2). +intros. +replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). +unfold Rminus in |- *; apply CV_plus. +assumption. +apply CV_opp; assumption. +unfold Rminus, opp_seq in |- *; reflexivity. +Qed. (* Un -> +oo *) Definition cv_infty (Un:nat -> R) : Prop := @@ -1265,7 +1265,7 @@ apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro; assert (H8 := sym_eq H7); elim (fact_neq_0 _ H8). clear Un Vn; apply INR_le; simpl in |- *. induction M_nat as [| M_nat HrecM_nat]. -assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. +assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index deb98492..6cab2486 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: SeqSeries.v,v 1.14.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: SeqSeries.v 8670 2006-03-28 22:16:14Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -36,12 +36,12 @@ intros; (sigT (fun l:R => Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)). -intro; +intro X; cut (sigT (fun l:R => Un_cv (fun n:nat => sum_f_R0 (fun l:nat => An (S N + l)%nat) n) l)). -intro; elim X; intros l1N H2. +intro X0; elim X; intros l1N H2. elim X0; intros l2N H3. cut (l1 - SP fn N x = l1N). intro; cut (l2 - sum_f_R0 An N = l2N). @@ -217,7 +217,7 @@ Lemma Rseries_CV_comp : (forall n:nat, 0 <= An n <= Bn n) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 Bn N) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). -intros; apply cv_cauchy_2. +intros An Bn H X; apply cv_cauchy_2. assert (H0 := cv_cauchy_1 _ X). unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *. intros; elim (H0 eps H1); intros. diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index b4026e67..11b9d57b 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: SplitAbsolu.v,v 1.6.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: SplitAbsolu.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbasic_fun. diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 19df2afa..31d49b76 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: SplitRmult.v,v 1.7.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: SplitRmult.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index b11e51f0..3e2b6b9f 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sqrt_reg.v,v 1.9.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: Sqrt_reg.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. |