*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2280 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index fb5ec988e..cdfb2fa08 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -239,6 +239,14 @@ Lemma sum_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivabl
 Unfold derivable; Intros f1 f2 H1 H2 x; Apply sum_derivable_pt; [Exact (H1 x) | Exact (H2 x)].
 Save.
 
+Lemma sum_derivable_pt_var : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt ([y:R]``(f1 y)+(f2 y)``) x).
+Intros; Generalize (sum_derivable_pt f1 f2 x H H0); Unfold plus_fct; Intro; Assumption.
+Save.
+
+Lemma derive_sum : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derive_pt ([y:R]``(f1 y)+(f2 y)``) x)==``(derive_pt f1 x)+(derive_pt f2 x)``.
+Intros; Generalize (deriv_sum f1 f2 x H H0); Unfold plus_fct; Intro; Assumption.
+Save.
+
 (* Opposite *)
 Lemma deriv_opposite : (f:R->R;x:R) (derivable_pt f x) -> ``(derive_pt (opp_fct f) x)==-(derive_pt f x)``.
 Intros; Generalize (derivable_derive f x H); Intro H0; Elim H0; Intros l H1; Rewrite H1; Unfold opp_fct; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f x l H1); Intro H3; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``( -(f (x+h))- -(f x))/h- -l`` with ``- (((f (x+h))-(f x))/h-l)``; [Rewrite Rabsolu_Ropp; Apply (H4 h H5 H6) | Field; Assumption].
@@ -269,6 +277,11 @@ Lemma diff_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivab
 Unfold derivable; Intros f1 f2 H1 H2 x; Apply diff_derivable_pt; [ Exact (H1 x) | Exact (H2 x)].
 Save. 
 
+Lemma derive_diff : (f1,f2:R->R;x:R) (derivable_pt f1 x)
+-> (derivable_pt f2 x) -> (derive_pt ([y:R]``(f1 y)-(f2 y)``) x)==``(derive_pt f1 x)-(derive_pt f2 x)``.
+Intros; Generalize (deriv_diff f1 f2 x H H0); Unfold minus_fct; Intro; Assumption.
+Save.
+
 (**********)
 Lemma deriv_scal : (f:R->R;a,x:R) (derivable_pt f x) -> ``(derive_pt (mult_real_fct a f) x)==a*(derive_pt f x)``.
 Intros f a x Ha; Unfold mult_real_fct; Generalize (derivable_derive f x Ha); Intro Hb; Elim Hb; Intros l Hc; Rewrite Hc; Apply derive_pt_def_0; Generalize (Req_EM a R0); Intro H0; Elim H0; Intro H1.
@@ -299,11 +312,19 @@ Field; Assumption.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)].
 Save.
 
+Lemma scal_derivable_pt_var : (f:R->R;a:R; x:R) (derivable_pt f x) -> (derivable_pt ([y:R]``a*(f y)``) x).
+Intros; Generalize (scal_derivable_pt f a x H); Unfold mult_real_fct; Intro; Assumption.
+Save.
+
 Lemma scal_derivable : (f:R->R;a:R) (derivable f) -> (derivable (mult_real_fct a f)).
 Unfold derivable; Intros f a H1 x; Apply scal_derivable_pt; Exact
 (H1 x).
 Save.
 
+Lemma derive_scal : (f:R->R;a,x:R) (derivable_pt f x) -> (derive_pt ([x:R]``a*(f x)``) x)==``a*(derive_pt f x)``.
+Intros; Generalize (deriv_scal f a x H); Unfold mult_real_fct; Intro; Assumption.
+Save.
+
 (* Multiplication *)
 Lemma deriv_prod : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(derive_pt (mult_fct f1 f2) x)==(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)``.
 Intros; Generalize (derivable_derive f1 x H); Intro; Generalize (derivable_derive f2 x H0); Intro; Elim H1; Clear H1; Intros l1 H1; Elim H2; Clear H2; Intros l2 H2; Cut l1==((fct_cte l1) x).
@@ -323,6 +344,11 @@ Lemma prod_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivab
 Unfold derivable; Intros f1 f2 H1 H2 x; Apply prod_derivable_pt; [ Exact (H1 x) | Exact (H2 x)].
 Save.
 
+Lemma derive_prod : (f1,f2:R->R;x:R) (derivable_pt f1 x)
+-> (derivable_pt f2 x) -> (derive_pt ([x:R]``(f1 x)*(f2 x)``) x)==``(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)``.
+Intros; Generalize (deriv_prod f1 f2 x H H0); Unfold mult_fct; Intro; Assumption.
+Save.
+
 (**********)
 Lemma deriv_const : (a:R;x:R) (derive_pt ([x:R] a) x)==``0``.
 Intros; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Replace ``a-a`` with ``0``; [Unfold Rdiv; Rewrite Rmult_Ol; Rewrite minus_R0; Rewrite Rabsolu_R0; Assumption | Ring].
@@ -804,5 +830,18 @@ Intro; Right; Apply (H0 x).
 Save.
 
 (**********)
+Axiom derive_increasing_interv_ax : (a,b:R;f:R->R) ``a<b``-> (((t:R) ``a<t<b`` -> ``0<(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``)) /\ (((t:R) ``a<t<b`` -> ``0<=(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``)).
+
+(**********)
+Lemma derive_increasing_interv : (a,b:R;f:R->R) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<(f y)``).
+Intros; Generalize (derive_increasing_interv_ax a b f H); Intro; Elim H4; Intros H5 _; Apply (H5 H0 x y H1 H2 H3).
+Save.
+
+(**********)
+Lemma derive_increasing_interv_var : (a,b:R;f:R->R) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t)``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``).
+Intros; Generalize (derive_increasing_interv_ax a b f H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3).
+Save.
+
+(**********)
 (**********)
 Axiom IAF : (f,g:R->R;a,b:R) ``a<=b`` -> (derivable f) -> (derivable g) -> ((c:R) ``a<=c<=b`` -> ``(derive_pt g c)<=(derive_pt f c)``) -> ``(g b)-(g a)<=(f b)-(f a)``.