diff options
Diffstat (limited to 'theories/Reals/NewtonInt.v')
| -rw-r--r-- | theories/Reals/NewtonInt.v | 158 |
1 files changed, 79 insertions, 79 deletions
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index a4233021..67e353ee 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -9,9 +9,9 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. -Require Import Rtrigo. +Require Import Rtrigo1. Require Import Ranalysis. -Open Local Scope R_scope. +Local Open Scope R_scope. (*******************************************) (* Newton's Integral *) @@ -28,8 +28,8 @@ Lemma FTCN_step1 : forall (f:Differential) (a b:R), Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b. Proof. - intros f a b; unfold Newton_integrable in |- *; exists (d1 f); - unfold antiderivative in |- *; intros; case (Rle_dec a b); + intros f a b; unfold Newton_integrable; exists (d1 f); + unfold antiderivative; intros; case (Rle_dec a b); intro; [ left; split; [ intros; exists (cond_diff f x); reflexivity | assumption ] | right; split; @@ -42,26 +42,26 @@ Lemma FTC_Newton : NewtonInt (fun x:R => derive_pt f x (cond_diff f x)) a b (FTCN_step1 f a b) = f b - f a. Proof. - intros; unfold NewtonInt in |- *; reflexivity. + intros; unfold NewtonInt; reflexivity. Qed. (* $\int_a^a f$ exists forall a:R and f:R->R *) Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a. Proof. - intros f a; unfold Newton_integrable in |- *; + intros f a; unfold Newton_integrable; exists (fct_cte (f a) * id)%F; left; - unfold antiderivative in |- *; split. + unfold antiderivative; split. intros; assert (H1 : derivable_pt (fct_cte (f a) * id) x). apply derivable_pt_mult. apply derivable_pt_const. apply derivable_pt_id. exists H1; assert (H2 : x = a). elim H; intros; apply Rle_antisym; assumption. - symmetry in |- *; apply derive_pt_eq_0; + symmetry ; apply derive_pt_eq_0; replace (f x) with (0 * id x + fct_cte (f a) x * 1); [ apply (derivable_pt_lim_mult (fct_cte (f a)) id x); [ apply derivable_pt_lim_const | apply derivable_pt_lim_id ] - | unfold id, fct_cte in |- *; rewrite H2; ring ]. + | unfold id, fct_cte; rewrite H2; ring ]. right; reflexivity. Defined. @@ -69,8 +69,8 @@ Defined. Lemma NewtonInt_P2 : forall (f:R -> R) (a:R), NewtonInt f a a (NewtonInt_P1 f a) = 0. Proof. - intros; unfold NewtonInt in |- *; simpl in |- *; - unfold mult_fct, fct_cte, id in |- *; ring. + intros; unfold NewtonInt; simpl; + unfold mult_fct, fct_cte, id; ring. Qed. (* If $\int_a^b f$ exists, then $\int_b^a f$ exists too *) @@ -78,7 +78,7 @@ Lemma NewtonInt_P3 : forall (f:R -> R) (a b:R) (X:Newton_integrable f a b), Newton_integrable f b a. Proof. - unfold Newton_integrable in |- *; intros; elim X; intros g H; + unfold Newton_integrable; intros; elim X; intros g H; exists g; tauto. Defined. @@ -88,7 +88,7 @@ Lemma NewtonInt_P4 : NewtonInt f a b pr = - NewtonInt f b a (NewtonInt_P3 f a b pr). Proof. intros; unfold Newton_integrable in pr; elim pr; intros; elim p; intro. - unfold NewtonInt in |- *; + unfold NewtonInt; case (NewtonInt_P3 f a b (exist @@ -106,7 +106,7 @@ Proof. assert (H4 : a <= b <= b). split; [ assumption | right; reflexivity ]. assert (H5 := H2 _ H3); assert (H6 := H2 _ H4); rewrite H5; rewrite H6; ring. - unfold NewtonInt in |- *; + unfold NewtonInt; case (NewtonInt_P3 f a b (exist @@ -132,37 +132,37 @@ Lemma NewtonInt_P5 : Newton_integrable g a b -> Newton_integrable (fun x:R => l * f x + g x) a b. Proof. - unfold Newton_integrable in |- *; intros f g l a b X X0; + unfold Newton_integrable; 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. - left; unfold antiderivative in |- *; unfold antiderivative in H, H0; elim H; + left; unfold antiderivative; unfold antiderivative in H, H0; elim H; clear H; intros; elim H0; clear H0; intros H0 _. split. intros; elim (H _ H2); elim (H0 _ H2); intros. assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1). reg. - exists H5; symmetry in |- *; reg; rewrite <- H3; rewrite <- H4; reflexivity. + exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)). - left; rewrite <- H5; unfold antiderivative in |- *; split. + left; rewrite <- H5; unfold antiderivative; split. intros; elim H6; intros; assert (H9 : x1 = a). apply Rle_antisym; assumption. assert (H10 : a <= x1 <= b). - split; right; [ symmetry in |- *; assumption | rewrite <- H5; assumption ]. + split; right; [ symmetry ; assumption | rewrite <- H5; assumption ]. assert (H11 : b <= x1 <= a). - split; right; [ rewrite <- H5; symmetry in |- *; assumption | assumption ]. + split; right; [ rewrite <- H5; symmetry ; assumption | assumption ]. assert (H12 : derivable_pt x x1). - unfold derivable_pt in |- *; exists (f x1); elim (H3 _ H10); intros; - eapply derive_pt_eq_1; symmetry in |- *; apply H12. + unfold derivable_pt; exists (f x1); elim (H3 _ H10); intros; + eapply derive_pt_eq_1; symmetry ; apply H12. assert (H13 : derivable_pt x0 x1). - unfold derivable_pt in |- *; exists (g x1); elim (H1 _ H11); intros; - eapply derive_pt_eq_1; symmetry in |- *; apply H13. + unfold derivable_pt; exists (g x1); elim (H1 _ H11); intros; + eapply derive_pt_eq_1; symmetry ; apply H13. assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1). reg. - exists H14; symmetry in |- *; reg. + exists H14; symmetry ; reg. assert (H15 : derive_pt x0 x1 H13 = g x1). elim (H1 _ H11); intros; rewrite H15; apply pr_nu. assert (H16 : derive_pt x x1 H12 = f x1). @@ -172,34 +172,34 @@ Proof. elim p0; intro. unfold antiderivative in H, H0; elim H; elim H0; intros; elim H4; intro. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H5 H2)). - left; rewrite H5; unfold antiderivative in |- *; split. + left; rewrite H5; unfold antiderivative; split. intros; elim H6; intros; assert (H9 : x1 = a). apply Rle_antisym; assumption. assert (H10 : a <= x1 <= b). - split; right; [ symmetry in |- *; assumption | rewrite H5; assumption ]. + split; right; [ symmetry ; assumption | rewrite H5; assumption ]. assert (H11 : b <= x1 <= a). - split; right; [ rewrite H5; symmetry in |- *; assumption | assumption ]. + split; right; [ rewrite H5; symmetry ; assumption | assumption ]. assert (H12 : derivable_pt x x1). - unfold derivable_pt in |- *; exists (f x1); elim (H3 _ H11); intros; - eapply derive_pt_eq_1; symmetry in |- *; apply H12. + unfold derivable_pt; exists (f x1); elim (H3 _ H11); intros; + eapply derive_pt_eq_1; symmetry ; apply H12. assert (H13 : derivable_pt x0 x1). - unfold derivable_pt in |- *; exists (g x1); elim (H1 _ H10); intros; - eapply derive_pt_eq_1; symmetry in |- *; apply H13. + unfold derivable_pt; exists (g x1); elim (H1 _ H10); intros; + eapply derive_pt_eq_1; symmetry ; apply H13. assert (H14 : derivable_pt (fun y:R => l * x y + x0 y) x1). reg. - exists H14; symmetry in |- *; reg. + exists H14; symmetry ; reg. assert (H15 : derive_pt x0 x1 H13 = g x1). elim (H1 _ H10); intros; rewrite H15; apply pr_nu. assert (H16 : derive_pt x x1 H12 = f x1). elim (H3 _ H11); intros; rewrite H16; apply pr_nu. rewrite H15; rewrite H16; ring. right; reflexivity. - right; unfold antiderivative in |- *; unfold antiderivative in H, H0; elim H; + right; unfold antiderivative; unfold antiderivative in H, H0; elim H; clear H; intros; elim H0; clear H0; intros H0 _; split. intros; elim (H _ H2); elim (H0 _ H2); intros. assert (H5 : derivable_pt (fun y:R => l * x y + x0 y) x1). reg. - exists H5; symmetry in |- *; reg; rewrite <- H3; rewrite <- H4; reflexivity. + exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. Defined. @@ -210,12 +210,12 @@ Lemma antiderivative_P1 : antiderivative g G a b -> antiderivative (fun x:R => l * f x + g x) (fun x:R => l * F x + G x) a b. Proof. - unfold antiderivative in |- *; intros; elim H; elim H0; clear H H0; intros; + unfold antiderivative; intros; elim H; elim H0; clear H H0; intros; split. intros; elim (H _ H3); elim (H1 _ H3); intros. assert (H6 : derivable_pt (fun x:R => l * F x + G x) x). reg. - exists H6; symmetry in |- *; reg; rewrite <- H4; rewrite <- H5; ring. + exists H6; symmetry ; reg; rewrite <- H4; rewrite <- H5; ring. assumption. Qed. @@ -226,7 +226,7 @@ Lemma NewtonInt_P6 : NewtonInt (fun x:R => l * f x + g x) a b (NewtonInt_P5 f g l a b pr1 pr2) = l * NewtonInt f a b pr1 + NewtonInt g a b pr2. Proof. - intros f g l a b pr1 pr2; unfold NewtonInt in |- *; + intros f g l a b pr1 pr2; unfold NewtonInt; case (NewtonInt_P5 f g l a b pr1 pr2); intros; case pr1; intros; case pr2; intros; case (total_order_T a b); intro. @@ -277,7 +277,7 @@ Lemma antiderivative_P2 : | right _ => F1 x + (F0 b - F1 b) end) a c. Proof. - unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0; + unfold antiderivative; intros; elim H; clear H; intros; elim H0; clear H0; intros; split. 2: apply Rle_trans with b; assumption. intros; elim H3; clear H3; intros; case (total_order_T x b); intro. @@ -293,25 +293,25 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). - unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F0 x x0 = f x). - symmetry in |- *; assumption. + unfold derivable_pt_lim; assert (H7 : derive_pt F0 x x0 = f x). + symmetry ; assumption. assert (H8 := derive_pt_eq_1 F0 x (f x) x0 H7); unfold derivable_pt_lim in H8; intros; elim (H8 _ H9); intros; set (D := Rmin x1 (b - x)). assert (H11 : 0 < D). - unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - x)); intro. + unfold D; unfold Rmin; case (Rle_dec x1 (b - x)); intro. apply (cond_pos x1). apply Rlt_Rminus; assumption. exists (mkposreal _ H11); intros; case (Rle_dec x b); intro. case (Rle_dec (x + h) b); intro. apply H10. assumption. - apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_l ]. + apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. elim n; left; apply Rlt_le_trans with (x + D). apply Rplus_lt_compat_l; apply Rle_lt_trans with (Rabs h). apply RRle_abs. apply H13. apply Rplus_le_reg_l with (- x); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; - rewrite Rplus_0_l; rewrite Rplus_comm; unfold D in |- *; + rewrite Rplus_0_l; rewrite Rplus_comm; unfold D; apply Rmin_r. elim n; left; assumption. assert @@ -322,16 +322,16 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; exists (f x); apply H7. - exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7. + unfold derivable_pt; exists (f x); apply H7. + exists H8; symmetry ; apply derive_pt_eq_0; apply H7. assert (H5 : a <= x <= b). split; [ assumption | right; assumption ]. assert (H6 : b <= x <= c). - split; [ right; symmetry in |- *; assumption | assumption ]. + split; [ right; symmetry ; assumption | assumption ]. elim (H _ H5); elim (H0 _ H6); intros; assert (H9 : derive_pt F0 x x1 = f x). - symmetry in |- *; assumption. + symmetry ; assumption. assert (H10 : derive_pt F1 x x0 = f x). - symmetry in |- *; assumption. + symmetry ; assumption. assert (H11 := derive_pt_eq_1 F0 x (f x) x1 H9); assert (H12 := derive_pt_eq_1 F1 x (f x) x0 H10); assert @@ -342,21 +342,21 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). - unfold derivable_pt_lim in |- *; unfold derivable_pt_lim in H11, H12; intros; + unfold derivable_pt_lim; unfold derivable_pt_lim in H11, H12; intros; elim (H11 _ H13); elim (H12 _ H13); intros; set (D := Rmin x2 x3); assert (H16 : 0 < D). - unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x2 x3); intro. + unfold D; unfold Rmin; case (Rle_dec x2 x3); intro. apply (cond_pos x2). apply (cond_pos x3). exists (mkposreal _ H16); intros; case (Rle_dec x b); intro. case (Rle_dec (x + h) b); intro. apply H15. assumption. - apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_r ]. + apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_r ]. replace (F1 (x + h) + (F0 b - F1 b) - F0 x) with (F1 (x + h) - F1 x). apply H14. assumption. - apply Rlt_le_trans with D; [ assumption | unfold D in |- *; apply Rmin_l ]. + apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. rewrite b0; ring. elim n; right; assumption. assert @@ -367,8 +367,8 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; exists (f x); apply H13. - exists H14; symmetry in |- *; apply derive_pt_eq_0; apply H13. + unfold derivable_pt; exists (f x); apply H13. + exists H14; symmetry ; apply derive_pt_eq_0; apply H13. assert (H5 : b <= x <= c). split; [ left; assumption | assumption ]. assert (H6 := H0 _ H5); elim H6; clear H6; intros; @@ -380,12 +380,12 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). - unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F1 x x0 = f x). - symmetry in |- *; assumption. + unfold derivable_pt_lim; assert (H7 : derive_pt F1 x x0 = f x). + symmetry ; assumption. assert (H8 := derive_pt_eq_1 F1 x (f x) x0 H7); unfold derivable_pt_lim in H8; intros; elim (H8 _ H9); intros; set (D := Rmin x1 (x - b)); assert (H11 : 0 < D). - unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (x - b)); intro. + unfold D; unfold Rmin; case (Rle_dec x1 (x - b)); intro. apply (cond_pos x1). apply Rlt_Rminus; assumption. exists (mkposreal _ H11); intros; case (Rle_dec x b); intro. @@ -399,13 +399,13 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. apply Rlt_le_trans with D. apply H13. - unfold D in |- *; apply Rmin_r. + unfold D; apply Rmin_r. replace (F1 (x + h) + (F0 b - F1 b) - (F1 x + (F0 b - F1 b))) with (F1 (x + h) - F1 x); [ idtac | ring ]; apply H10. assumption. apply Rlt_le_trans with D. assumption. - unfold D in |- *; apply Rmin_l. + unfold D; apply Rmin_l. assert (H8 : derivable_pt @@ -414,8 +414,8 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; exists (f x); apply H7. - exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7. + unfold derivable_pt; exists (f x); apply H7. + exists H8; symmetry ; apply derive_pt_eq_0; apply H7. Qed. Lemma antiderivative_P3 : @@ -427,15 +427,15 @@ Proof. intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0; intros; case (total_order_T a c); intro. elim s; intro. - right; unfold antiderivative in |- *; split. + right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ assumption | apply Rle_trans with c; assumption ]. left; assumption. - right; unfold antiderivative in |- *; split. + right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ assumption | apply Rle_trans with c; assumption ]. right; assumption. - left; unfold antiderivative in |- *; split. + left; unfold antiderivative; split. intros; apply H; elim H3; intros; split; [ assumption | apply Rle_trans with a; assumption ]. left; assumption. @@ -450,15 +450,15 @@ Proof. intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0; intros; case (total_order_T c b); intro. elim s; intro. - right; unfold antiderivative in |- *; split. + right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ apply Rle_trans with c; assumption | assumption ]. left; assumption. - right; unfold antiderivative in |- *; split. + right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ apply Rle_trans with c; assumption | assumption ]. right; assumption. - left; unfold antiderivative in |- *; split. + left; unfold antiderivative; split. intros; apply H; elim H3; intros; split; [ apply Rle_trans with b; assumption | assumption ]. left; assumption. @@ -471,7 +471,7 @@ Lemma NewtonInt_P7 : Newton_integrable f a b -> Newton_integrable f b c -> Newton_integrable f a c. Proof. - unfold Newton_integrable in |- *; intros f a b c Hab Hbc X X0; elim X; + unfold Newton_integrable; intros f a b c Hab Hbc X X0; elim X; clear X; intros F0 H0; elim X0; clear X0; intros F1 H1; set (g := @@ -479,7 +479,7 @@ Proof. match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) - end); exists g; left; unfold g in |- *; + end); exists g; left; unfold g; apply antiderivative_P2. elim H0; intro. assumption. @@ -504,7 +504,7 @@ Proof. case (total_order_T b c); intro. elim s0; intro. (* a<b & b<c *) - unfold Newton_integrable in |- *; + unfold Newton_integrable; exists (fun x:R => match Rle_dec x b with @@ -523,7 +523,7 @@ Proof. (* a<b & b>c *) case (total_order_T a c); intro. elim s0; intro. - unfold Newton_integrable in |- *; exists F0. + unfold Newton_integrable; exists F0. left. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. @@ -537,7 +537,7 @@ Proof. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). rewrite b0; apply NewtonInt_P1. - unfold Newton_integrable in |- *; exists F1. + unfold Newton_integrable; exists F1. right. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. @@ -557,7 +557,7 @@ Proof. (* a>b & b<c *) case (total_order_T a c); intro. elim s0; intro. - unfold Newton_integrable in |- *; exists F1. + unfold Newton_integrable; exists F1. left. elim H1; intro. (*****************) @@ -572,7 +572,7 @@ Proof. unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). rewrite b0; apply NewtonInt_P1. - unfold Newton_integrable in |- *; exists F0. + unfold Newton_integrable; exists F0. right. elim H0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. @@ -601,7 +601,7 @@ Lemma NewtonInt_P9 : NewtonInt f a c (NewtonInt_P8 f a b c pr1 pr2) = NewtonInt f a b pr1 + NewtonInt f b c pr2. Proof. - intros; unfold NewtonInt in |- *. + intros; unfold NewtonInt. case (NewtonInt_P8 f a b c pr1 pr2); intros. case pr1; intros. case pr2; intros. @@ -641,7 +641,7 @@ Proof. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). (* a<b & b=c *) rewrite <- b0. - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. rewrite <- b0 in o. elim o0; intro. elim o; intro. @@ -759,7 +759,7 @@ Proof. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)). (* a>b & b=c *) rewrite <- b0. - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. rewrite <- b0 in o. elim o0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. |