diff options
| author | desmettr | 2002-06-11 17:01:24 +0000 |
|---|---|---|
| committer | desmettr | 2002-06-11 17:01:24 +0000 |
| commit | 9e5b51066675777240ec2e5b35016686c0c89f41 (patch) | |
| tree | f8bcec6a71207d263a295673ffdeb8136d7928e8 | |
| parent | 9b9ed1245225fc95374b070f5f5ed699337448fc (diff) | |
Ranalysis.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2774 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/Ranalysis.v | 959 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis1.v | 1189 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 305 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis3.v | 606 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis4.v | 459 |
5 files changed, 2564 insertions, 954 deletions
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 15b31daea7..95046d292f 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -5,959 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) - -(*i $Id$ i*) - -Require Rbase. -Require Rbasic_fun. -Require R_sqr. -Require Rlimit. -Require Rderiv. -Require DiscrR. -Require Rtrigo. - -(****************************************************) -(** Basic operations on functions *) -(****************************************************) -Definition plus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)+(f2 x)``. -Definition opp_fct [f:R->R] : R->R := [x:R] ``-(f x)``. -Definition mult_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)*(f2 x)``. -Definition mult_real_fct [a:R;f:R->R] : R->R := [x:R] ``a*(f x)``. -Definition minus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)-(f2 x)``. -Definition div_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)/(f2 x)``. -Definition div_real_fct [a:R;f:R->R] : R->R := [x:R] ``a/(f x)``. -Definition comp [f1,f2:R->R] : R->R := [x:R] ``(f1 (f2 x))``. - -(****************************************************) -(** Variations of functions *) -(****************************************************) -Definition increasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f x)<=(f y)``. -Definition decreasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f y)<=(f x)``. -Definition strict_increasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f x)<(f y)``. -Definition strict_decreasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f y)<(f x)``. -Definition constant [f:R->R] : Prop := (x,y:R) ``(f x)==(f y)``. - -(**********) -Axiom fct_eq : (A,B:Type) (f1,f2:A->B) ((x:A)(f1 x)==(f2 x))->f1==f2. - -(**********) -Definition no_cond : R->Prop := [x:R] True. - -(***************************************************) -(** Definition of continuity as a limit *) -(***************************************************) - -(**********) -Definition continuity_pt [f:R->R; x0:R] : Prop := (continue_in f no_cond x0). - -(**********) -Lemma sum_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (plus_fct f1 f2) x0). -Unfold continuity_pt plus_fct; Unfold continue_in; Intros; Apply limit_plus; Assumption. -Qed. - -(**********) -Lemma diff_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (minus_fct f1 f2) x0). -Unfold continuity_pt minus_fct; Unfold continue_in; Intros; Apply limit_minus; Assumption. -Qed. - -(**********) -Lemma prod_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (mult_fct f1 f2) x0). -Unfold continuity_pt mult_fct; Unfold continue_in; Intros; Apply limit_mul; Assumption. -Qed. - -(**********) -Lemma const_continuous : (f:R->R; x0:R) (constant f) -> (continuity_pt f x0). -Unfold constant continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split; [Apply Rlt_R0_R1 | Intros; Generalize (H x x0); Intro; Rewrite H2; Simpl; Rewrite R_dist_eq; Assumption]. -Qed. - -(**********) -Lemma scal_continuous : (f:R->R;a:R; x0:R) (continuity_pt f x0) -> (continuity_pt (mult_real_fct a f) x0). -Unfold continuity_pt mult_real_fct; Unfold continue_in; Intros; Apply (limit_mul ([x:R] a) f (D_x no_cond x0) a (f x0) x0). -Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split. -Apply Rlt_R0_R1. -Intros; Rewrite R_dist_eq; Assumption. -Assumption. -Qed. - -(**********) -Lemma opp_continuous : (f:R->R; x0:R) (continuity_pt f x0) -> (continuity_pt (opp_fct f) x0). -Unfold continuity_pt opp_fct; Unfold continue_in; Intros; Apply limit_Ropp; Assumption. -Qed. - -(**********) -Lemma inv_continuous : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> -(continuity_pt ([x:R] ``/(f x)``) x0). -Unfold continuity_pt; Unfold continue_in; Intros; Apply limit_inv; Assumption. -Qed. - -Lemma div_eq_inv : (f1,f2:R->R) (div_fct f1 f2)==(mult_fct f1 ([x:R]``/(f2 x)``)). -Intros; Unfold div_fct; Unfold mult_fct; Unfold Rdiv; Apply fct_eq; Intro x; Reflexivity. -Qed. - -(**********) -Lemma div_continuous : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> ~``(f2 x0)==0`` -> (continuity_pt (div_fct f1 f2) x0). -Intros; Rewrite -> (div_eq_inv f1 f2); Apply prod_continuous; [Assumption | Apply inv_continuous; Assumption]. -Qed. - -(**********) -Definition continuity [f:R->R] : Prop := (x:R) (continuity_pt f x). - -Lemma sum_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (plus_fct f1 f2)). -Unfold continuity; Intros; Apply (sum_continuous f1 f2 x (H x) (H0 x)). -Qed. - -Lemma diff_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (minus_fct f1 f2)). -Unfold continuity; Intros; Apply (diff_continuous f1 f2 x (H x) (H0 x)). -Qed. - -Lemma prod_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (mult_fct f1 f2)). -Unfold continuity; Intros; Apply (prod_continuous f1 f2 x (H x) (H0 x)). -Qed. - -Lemma const_continuity : (f:R->R) (constant f) -> (continuity f). -Unfold continuity; Intros; Apply (const_continuous f x H). -Qed. - -Lemma scal_continuity : (f:R->R;a:R) (continuity f) -> (continuity (mult_real_fct a f)). -Unfold continuity; Intros; Apply (scal_continuous f a x (H x)). -Qed. - -Lemma opp_continuity : (f:R->R) (continuity f)->(continuity (opp_fct f)). -Unfold continuity; Intros; Apply (opp_continuous f x (H x)). -Qed. - -Lemma div_continuity : (f1,f2:R->R) (continuity f1)->(continuity f2)->((x:R) ~``(f2 x)==0``)->(continuity (div_fct f1 f2)). -Unfold continuity; Intros; Apply (div_continuous f1 f2 x (H x) (H0 x) (H1 x)). -Qed. - -Lemma inv_continuity : (f:R->R) (continuity f)->((x:R) ~``(f x)==0``)->(continuity ([x:R] ``/(f x)``)). -Unfold continuity; Intros; Apply (inv_continuous f x (H x) (H0 x)). -Qed. - -(*****************************************************) -(** Derivative's definition using Landau's kernel *) -(*****************************************************) -Definition derivable_pt [f:R->R; x:R] : Prop := (EXT l : R | ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``)))). - -Definition derivable [f:R->R] : Prop := (x:R) (derivable_pt f x). - -Parameter derive_pt : (R->R)->R->R. - -Axiom derive_pt_def : (f:R->R;x,l:R) ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))) <-> (derive_pt f x)==l. - -(**********) -Lemma derive_pt_def_0 : (f:R->R;x,l:R) ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))) -> (derive_pt f x)==l. -Intros; Elim (derive_pt_def f x l); Intros; Apply (H0 H). -Qed. - -(**********) -Lemma derive_pt_def_1 : (f:R->R;x,l:R) (derive_pt f x)==l -> ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))). -Intros; Elim (derive_pt_def f x l); Intros; Apply (H2 H eps H0). -Qed. - -(**********) -Definition derive [f:R->R] := [x:R] (derive_pt f x). - -(************************************) -(** Class of differential functions *) -(************************************) -Record Differential : Type := mkDifferential { -d1 :> R->R; -cond_diff : (derivable d1) }. - -Record Differential_D2 : Type := mkDifferential_D2 { -d2 :> R->R; -cond_D1 : (derivable d2); -cond_D2 : (derivable (derive d2)) }. - -(**********) -Lemma derivable_derive : (f:R->R;x:R) (derivable_pt f x) -> (EXT l : R | (derive_pt f x)==l). -Intros f x; Unfold derivable_pt; Intro H; Elim H; Intros l H0; Rewrite (derive_pt_def_0 f x l); [Exists l; Reflexivity | Assumption]. -Qed. - -(**********) -Lemma derive_derivable : (f:R->R;x,l:R) (derive_pt f x)==l -> (derivable_pt f x). -Intros; Unfold derivable_pt; Generalize (derive_pt_def_1 f x l H); Intro H0; Exists l; Assumption. -Qed. - -(********************************************************************) -(** Equivalence of this definition with the one using limit concept *) -(********************************************************************) -Lemma derive_pt_D_in : (f,df:R->R;x:R) (D_in f df no_cond x) <-> (derive_pt -f x)==(df x). -Intros; Split. -Unfold D_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros. -Apply derive_pt_def_0. -Intros; Elim (H eps H0); Intros alpha H1; Elim H1; Intros; Exists (mkposreal alpha H2); Intros; Generalize (H3 ``x+h``); Intro; Cut ``x+h-x==h``; [Intro; Cut ``(D_x no_cond x (x+h))``/\``(Rabsolu (x+h-x)) < alpha``; [Intro; Generalize (H6 H8); Rewrite H7; Intro; Assumption | Split; [Unfold D_x; Split; [Unfold no_cond; Trivial | Apply Rminus_not_eq_right; Rewrite H7; Assumption] | Rewrite H7; Assumption]] | Ring]. -Intro; Generalize (derive_pt_def_1 f x (df x) H); Intro; Unfold D_in; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros; Elim (H0 eps H1); Intros alpha H2; Exists (pos alpha); Split. -Apply (cond_pos alpha). -Intros; Elim H3; Intros; Unfold D_x in H4; Elim H4; Intros; Cut ``x0-x<>0``. -Intro; Generalize (H2 ``x0-x`` H8 H5); Replace ``x+(x0-x)`` with x0. -Intro; Assumption. -Ring. -Auto with real. -Qed. - -Definition fct_cte [a:R] : R->R := [x:R]a. - -(***********************************) -(** derivability -> continuity *) -(***********************************) -Theorem derivable_continuous_pt : (f:R->R;x:R) (derivable_pt f x) -> (continuity_pt f x). -Intros. -Generalize (derivable_derive f x H); Intro. -Elim H0; Intros l H1. -Cut l==((fct_cte l) x). -Intro. -Rewrite H2 in H1. -Generalize (derive_pt_D_in f (fct_cte l) x); Intro. -Elim H3; Intros. -Generalize (H5 H1); Intro. -Unfold continuity_pt. -Apply (cont_deriv f (fct_cte l) no_cond x H6). -Unfold fct_cte; Reflexivity. -Qed. -Theorem derivable_continuous : (f:R->R) (derivable f) -> (continuity f). -Unfold derivable continuity; Intros; Apply (derivable_continuous_pt f x (H x)). -Qed. - -(****************************************************************) -(** Main rules *) -(****************************************************************) - -(* Addition *) -Lemma deriv_sum : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(derive_pt (plus_fct f1 f2) x)==(derive_pt f1 x)+(derive_pt f2 x)``. -Intros; Generalize (derivable_derive f1 x H); Intro H1; Generalize (derivable_derive f2 x H0); Intro H2; Elim H1; Clear H1; Intros l1 H1; Elim H2; Clear H2; Intros l2 H2; Unfold plus_fct; Rewrite H1; Rewrite H2; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f1 x l1 H1); Clear H1; Intro H1; Generalize (derive_pt_def_1 f2 x l2 H2); Clear H2; Intro H2; Cut ~(O=(2)). -Intro Haux; Generalize (lt_INR_0 (2) (neq_O_lt (2) Haux)); Rewrite INR_eq_INR2; Unfold INR2; Intro Haux1; Generalize (Rlt_Rinv ``2`` Haux1); Clear Haux1; Intro Haux1; Generalize (Rmult_lt_pos eps ``/2`` H3 Haux1); Clear Haux1; Intro Haux1; Elim (H1 ``eps/2`` Haux1); Intros delta1 H4; Elim (H2 ``eps/2`` Haux1); Intros delta2 H5; Exists (mkposreal (Rmin delta1 delta2) (Rmin_stable_in_posreal delta1 delta2)); Intros h H6 H7; Unfold plus_fct; Replace ``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h-(l1+l2)`` with ``(((f1 (x+h))-(f1 x))/h-l1)+(((f2 (x+h))-(f2 x))/h-l2)``. -Apply Rle_lt_trans with ``(Rabsolu ((f1 (x+h))-(f1 x))/h-l1)+(Rabsolu ((f2 (x+h))-(f2 x))/h-l2)``. -Apply Rabsolu_triang. -Generalize (H5 h H6 (Rlt_le_trans (Rabsolu h) (Rmin delta1 delta2) delta2 H7 (Rmin_r delta1 delta2))); Intro H8; Generalize (H4 h H6 (Rlt_le_trans (Rabsolu h) (Rmin delta1 delta2) delta1 H7 (Rmin_l delta1 delta2))); Intro H9. -Generalize (Rplus_lt ``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))`` ``eps/2`` ``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2))`` ``eps/2`` H9 H8). -Replace ``eps/2+eps/2`` with ``eps``. -Intro H10; Assumption. -Apply double_var. -Unfold Rdiv. -Repeat Rewrite <- (Rmult_sym ``/h``). -Repeat Rewrite Rminus_distr. -Repeat Rewrite Rmult_Rplus_distr. -Unfold Rminus. -Repeat Rewrite Ropp_distr1. -Ring. -Discriminate. -Qed. - -Lemma sum_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (plus_fct f1 f2) 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; Apply (derive_derivable (plus_fct f1 f2) x ``l1+l2``); Rewrite <- H1; Rewrite <- H2; Apply deriv_sum; Assumption. -Qed. - -Lemma sum_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (plus_fct f1 f2)). -Unfold derivable; Intros f1 f2 H1 H2 x; Apply sum_derivable_pt; [Exact (H1 x) | Exact (H2 x)]. -Qed. - -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. -Qed. - -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. -Qed. - -(* 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). -Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. -Qed. - -Lemma opposite_derivable_pt : (f:R->R;x:R) (derivable_pt f x) -> (derivable_pt (opp_fct f) x). -Unfold opp_fct derivable_pt; Intros; Elim H; Intros; Exists ``-x0``; Intros; Elim (H0 eps H1); Intros; Exists x1; Intros; Generalize (H2 h H3 H4); Intro H5; Replace ``( -(f (x+h))- -(f x))/h- -x0`` with ``- (((f (x+h))-(f x))/h-x0)``. -Rewrite Rabsolu_Ropp; Assumption. -Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. -Qed. - -Lemma opposite_derivable : (f:R->R) (derivable f) -> (derivable (opp_fct f)). -Unfold derivable; Intros f H1 x; Apply opposite_derivable_pt; Exact (H1 x). -Qed. - -(* Difference *) -Lemma diff_plus_opp : (f1,f2:R->R) (minus_fct f1 f2)==(plus_fct f1 (opp_fct f2)). -Intros; Unfold minus_fct plus_fct opp_fct; Apply fct_eq; Intro x; Ring. -Qed. - -Lemma deriv_diff : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(derive_pt (minus_fct f1 f2) x)==(derive_pt f1 x)-(derive_pt f2 x)``. -Intros; Rewrite diff_plus_opp; Unfold Rminus; Rewrite <- (deriv_opposite f2 x H0); Apply deriv_sum; [Assumption | Apply opposite_derivable_pt; Assumption]. -Qed. - -Lemma diff_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (minus_fct f1 f2) x). -Intros; Rewrite (diff_plus_opp f1 f2); Apply sum_derivable_pt; [Assumption | Apply opposite_derivable_pt; Assumption]. -Qed. - -Lemma diff_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (minus_fct f1 f2)). -Unfold derivable; Intros f1 f2 H1 H2 x; Apply diff_derivable_pt; [ Exact (H1 x) | Exact (H2 x)]. -Qed. - -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. -Qed. - -(**********) -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. -Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Rewrite H1; Repeat Rewrite Rmult_Ol; Repeat Rewrite minus_R0; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption. -Intros; Generalize (derive_pt_def_1 f x l Hc); Intro H2; Elim (H2 ``eps/(Rabsolu a)``). -Intros; Exists x0; Intros; Replace ``(a*(f (x+h))-a*(f x))/h-a*l`` with ``a*(((f (x+h))-(f x))/h-l)``. -Rewrite Rabsolu_mult; Replace ``eps`` with ``(Rabsolu a)*(eps/(Rabsolu a))``. -Apply Rlt_monotony. -Apply (Rabsolu_pos_lt a H1). -Apply (H3 h H4 H5). -Rewrite <- Rmult_sym; Unfold Rdiv; Rewrite Rmult_assoc; Rewrite <- (Rinv_l_sym (Rabsolu a)); [Apply Rmult_1r | Apply (Rabsolu_no_R0 a H1)]. -Rewrite Rminus_distr. -Unfold Rdiv. -Rewrite <- Rmult_assoc. -Rewrite Rminus_distr. -Reflexivity. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. -Qed. - -Lemma scal_derivable_pt : (f:R->R;a:R; x:R) (derivable_pt f x) -> -(derivable_pt (mult_real_fct a f) x). -Unfold mult_real_fct derivable_pt; Intros; Generalize (Req_EM a R0); Intro H0; Elim H0; Intro H1. -Intros; Exists ``0``; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Rewrite H1; Repeat Rewrite Rmult_Ol; Unfold Rminus; Repeat Rewrite Ropp_O; Repeat Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption. -Elim H; Intros l H2; Exists ``a*l``; Intros; Elim (H2 ``eps/(Rabsolu a)``); Intros. -Exists x0; Intros; Replace ``(a*(f (x+h))-a*(f x))/h-a*l`` with ``a*(((f (x+h))-(f x))/h-l)``. -Rewrite Rabsolu_mult; Replace ``eps`` with ``(Rabsolu a)*(eps/(Rabsolu a))``. -Apply Rlt_monotony. -Apply (Rabsolu_pos_lt a H1). -Apply (H4 h H5 H6). -Rewrite <- Rmult_sym; Unfold Rdiv; Rewrite Rmult_assoc; Rewrite <- (Rinv_l_sym (Rabsolu a)); [Apply Rmult_1r | Apply (Rabsolu_no_R0 a H1)]. -Rewrite Rminus_distr. -Unfold Rdiv. -Rewrite <- Rmult_assoc. -Rewrite Rminus_distr. -Reflexivity. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. -Qed. - -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. -Qed. - -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). -Qed. - -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. -Qed. - -(* 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). -Cut l2==((fct_cte l2) x). -Intros; Rewrite H3 in H2; Rewrite H4 in H1; Generalize derive_pt_D_in; Intro; Generalize (H5 f1 (fct_cte l1) x); Intro; Generalize (H5 f2 (fct_cte l2) x); Intro; Elim H6; Elim H7; Intros; Generalize (H11 H1); Intro; Generalize (H9 H2); Intro; Rewrite H1; Rewrite H2; Replace ``(fct_cte l1 x)*(f2 x)+(fct_cte l2 x)*(f1 x)`` with ``((plus_fct (mult_fct (fct_cte l1) f2) (mult_fct f1 (fct_cte l2))) x)``. -Generalize (H5 (mult_fct f1 f2) (plus_fct (mult_fct (fct_cte l1) f2) (mult_fct f1 (fct_cte l2))) x); Intro; Elim H14; Intros; Apply H15; Unfold mult_fct plus_fct; Apply Dmult; Assumption. -Unfold plus_fct mult_fct fct_cte; Ring. -Unfold fct_cte; Reflexivity. -Unfold fct_cte; Reflexivity. -Qed. - -Lemma prod_derivable_pt : (f1,f2:R->R;x:R) (derivable_pt f1 x)->(derivable_pt f2 x)->(derivable_pt (mult_fct f1 f2) x). -Intros; Generalize (deriv_prod f1 f2 x H H0); Intro; Apply (derive_derivable (mult_fct f1 f2) x ``(derive_pt f1 x)*(f2 x)+(derive_pt f2 x)*(f1 x)`` H1). -Qed. - -Lemma prod_derivable : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (mult_fct f1 f2)). -Unfold derivable; Intros f1 f2 H1 H2 x; Apply prod_derivable_pt; [ Exact (H1 x) | Exact (H2 x)]. -Qed. - -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. -Qed. - -(**********) -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]. -Qed. - -Lemma const_derivable : (a:R) (derivable ([x:R] a)). -Unfold derivable; Unfold derivable_pt; Intros; Exists ``0``; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Unfold Rminus; Rewrite Rplus_Ropp_r; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. -Qed. - -(**********) -Lemma deriv_id : (x:R) (derive_pt ([y:R] y) x)==``1``. -Intro x; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Replace ``(x+h-x)/h-1`` with ``0``. -Rewrite Rabsolu_R0; Assumption. -Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. -Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. -Symmetry; Apply Rplus_Ropp_r. -Assumption. -Qed. - -Lemma diff_id : (derivable ([x:R] x)). -Unfold derivable; Intro x; Unfold derivable_pt; Exists ``1``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``(x+h-x)/h-1`` with ``0``. -Rewrite Rabsolu_R0; Apply Rle_lt_trans with ``(Rabsolu h)``. -Apply Rabsolu_pos. -Assumption. -Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. -Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. -Symmetry; Apply Rplus_Ropp_r. -Assumption. -Qed. - -(**********) -Lemma sum_fct_cte_derive_pt : (f:R->R;t,a:R) (derivable_pt f t) -> (derive_pt ([x:R]``(f x)+a``) t)==(derive_pt f t). -Intros; Generalize (derivable_derive f t H); Intro; Elim H0; Intros l H1; Rewrite H1; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f t l H1); Intros; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``(f (t+h))+a-((f t)+a)`` with ``(f (t+h))-(f t)``; [Apply (H4 h H5 H6) | Ring]. -Qed. - -Lemma sum_fct_cte_derivable_pt : (f:R->R;t,a:R) (derivable_pt f t)->(derivable_pt ([t:R]``(f t)+a``) t). -Unfold derivable_pt; Intros; Elim H; Intros; Exists x; Intros; Elim (H0 eps H1); Intros; Exists x0; Intro h; Replace ``(f (t+h))+a-((f t)+a)`` with ``(f (t+h))-(f t)``; [Exact (H2 h) | Ring]. -Qed. - -Lemma sum_fct_cte_derivable : (f:R->R;a:R) (derivable f)->(derivable ([t:R]``(f t)+a``)). -Unfold derivable; Intros; Apply sum_fct_cte_derivable_pt; Apply (H x). -Qed. - -(**********) -Lemma deriv_Rsqr : (x:R) (derive Rsqr x)==``2*x``. -Intro x; Unfold Rsqr; Unfold derive; Apply (derive_pt_def_0 ([x0:R]``x0*x0``) x); Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. -Assumption. -Replace ``(x+h)*(x+h)`` with ``(Rsqr (x+h))``. -Rewrite Rsqr_plus; Unfold Rminus; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym (Rsqr x)); Repeat Rewrite Rplus_assoc; Unfold Rsqr; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. -Rewrite Rplus_Or; Reflexivity. -Assumption. -Unfold Rsqr; Reflexivity. -Qed. - -Lemma diff_Rsqr : (derivable Rsqr). -Unfold derivable; Intro x; Unfold Rsqr; Unfold derivable_pt; Exists ``2*x``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. -Assumption. -Replace ``(x+h)*(x+h)`` with ``(Rsqr (x+h))``. -Rewrite Rsqr_plus; Unfold Rminus; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym (Rsqr x)); Repeat Rewrite Rplus_assoc; Unfold Rsqr; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. -Rewrite Rplus_Or; Reflexivity. -Assumption. -Unfold Rsqr; Reflexivity. -Qed. - -Lemma Rsqr_derivable_pt : (f:R->R;t:R) (derivable_pt f t) -> (derivable_pt ([x:R](Rsqr (f x))) t). -Unfold Rsqr; Intros; Generalize (prod_derivable_pt f f t H H); Unfold mult_fct; Intro H0; Assumption. -Qed. - -Lemma Rsqr_derivable : (f:R->R) (derivable f)->(derivable ([x:R](Rsqr (f x)))). -Unfold derivable; Intros; Apply (Rsqr_derivable_pt f x (H x)). -Qed. - -(* SQRT *) -Axiom deriv_sqrt : (x:R) ``0<x`` -> (derive sqrt)==[y:R] ``1/(2*(sqrt y))``. - -Lemma eq_fct : (x:R;f1,f2:R->R) f1==f2 -> (f1 x)==(f2 x). -Intros; Rewrite H; Reflexivity. -Qed. - -Lemma diff_sqrt : (x:R) ``0<x`` -> (derivable_pt sqrt x). -Intros; Generalize (deriv_sqrt x H); Unfold derive; Intro; Generalize (eq_fct x ([x:R](derive_pt sqrt x)) ([y:R]``1/(2*(sqrt y))``) H0); Intro; Apply (derive_derivable sqrt x ``1/(2*(sqrt x))`` H1). -Qed. - -(* Composition *) - -Lemma deriv_composition : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> ``(derive_pt (comp g f) x)==(derive_pt g (f x))*(derive_pt f x)``. -Intros; Generalize (derivable_derive f x H); Intro; Generalize -(derivable_derive g (f x) H0); Intro; Elim H1; Clear H1; Intros l1 H1; Elim -H2; Clear H2; Intros l2 H2. -Cut l1==((fct_cte l1) x). -Cut l2==((fct_cte l2) x). -Intros; Rewrite H3 in H2; Rewrite H4 in H1; Rewrite H1; Rewrite H2; -Generalize derive_pt_D_in; Intro; Elim (H5 f (fct_cte l1) x); Intros; Elim -(H5 g (fct_cte l2) (f x)); Intros; Generalize (H9 H2); Intro; Generalize (H7 -H1); Intro; Replace ``(fct_cte l2 x)*(fct_cte l1 x)`` with ``((mult_fct -(fct_cte l1) (fct_cte l2)) x)``. -Elim (H5 (comp g f) (mult_fct (fct_cte l1) (fct_cte l2)) x); Intros; Apply -H12. -Generalize (Dcomp no_cond no_cond (fct_cte l1) (fct_cte l2) f g x); Unfold comp mult_fct no_cond D_in; Unfold Dgf; Intros. -Cut (limit1_in [x0:R]``((g (f x0))-(g (f x)))/(x0-x)`` (D_x [_:R]True/\True x) ``(fct_cte l1 x)*(fct_cte l2 (f x))`` x) -> (limit1_in [x0:R]``((g (f x0))-(g (f x)))/(x0-x)`` (D_x [_:R]True x) ``(fct_cte l1 x)*(fct_cte l2 x)`` x). -Intros; Apply H15; Apply H14. -Assumption. -Assumption. -Unfold D_x limit1_in; Unfold limit_in; Intros; Elim (H15 eps H16); Intros; Exists x0; Elim H17; Intros; Split. -Assumption. -Intros; Apply H19; Elim H20; Intros; Elim H21; Intros; Split. -Split. -Split; Trivial. -Assumption. -Assumption. -Unfold mult_fct fct_cte; Rewrite Rmult_sym; Reflexivity. -Unfold fct_cte; Reflexivity. -Unfold fct_cte; Reflexivity. -Qed. - -Lemma composition_derivable : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derivable_pt (comp g f) x). -Intros; Generalize (deriv_composition f g x H H0); Intro; Apply (derive_derivable (comp g f) x ``(derive_pt g (f x))*(derive_pt f x)`` H1). -Qed. - -Lemma derive_composition : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derive_pt ([x:R]``(g (f x))``) x)==``(derive_pt g (f x))*(derive_pt f x)``. -Intros; Generalize (deriv_composition f g x H H0); Unfold comp; Intro; Assumption. -Qed. - -Lemma composition_derivable_var : (f,g:R->R;x:R) (derivable_pt f x) -> (derivable_pt g (f x)) -> (derivable_pt ([x:R](g (f x))) x). -Intros; Generalize (composition_derivable f g x H H0); Unfold comp; Intro; Assumption. -Qed. - -Lemma diff_comp : (f,g:R->R) (derivable f)->(derivable g)->(derivable (comp g f)). -Intros f g; Unfold derivable; Intros H1 H2 x; Apply (composition_derivable f g x (H1 x) (H2 (f x))). -Qed. - -Lemma Rsqr_derive : (f:R->R;t:R) (derivable_pt f t)->(derive_pt ([x:R](Rsqr (f x))) t)==(Rmult ``2`` (Rmult (derive_pt f t) (f t))). -Intros; Generalize diff_Rsqr; Unfold derivable; Intro H0; Generalize (deriv_composition f Rsqr t H (H0 (f t))); Unfold comp; Intro H1; Rewrite H1; Generalize (deriv_Rsqr (f t)); Unfold derive; Intro H2; Rewrite H2; Rewrite Rmult_assoc; Rewrite <- (Rmult_sym (derive_pt f t)); Reflexivity. -Qed. - -(* SIN and COS *) -Axiom deriv_sin : (derive sin)==cos. - -Lemma diff_sin : (derivable sin). -Unfold derivable; Intro; Generalize deriv_sin; Unfold derive; Intro; Generalize -(eq_fct x ([x:R](derive_pt sin x)) cos H); Intro; Apply (derive_derivable sin x -(cos x) H0). -Qed. - -Lemma diff_cos : (derivable cos). -Unfold derivable; Intro; Cut ([x:R]``(sin (x+PI/2))``)==cos. -Intro; Rewrite <- H; Apply (composition_derivable_var ([x:R]``x+PI/2``) sin x). -Apply (sum_fct_cte_derivable_pt ([x:R]x) x ``PI/2``); Apply diff_id. -Apply diff_sin. -Apply fct_eq; Intro; Symmetry; Rewrite Rplus_sym; Apply cos_sin. -Qed. - -Lemma derive_pt_sin : (x:R) (derive_pt sin x)==(cos x). -Intro; Generalize deriv_sin; Unfold derive; Intro; Apply (eq_fct x [x:R](derive_pt sin x) cos H). -Qed. - -Lemma deriv_cos : (derive cos)==(opp_fct sin). -Unfold opp_fct derive; Apply fct_eq; Intro; Cut ([x:R]``(sin (x+PI/2))``)==cos. -Intro; Rewrite <- H; Rewrite (derive_composition ([x:R]``x+PI/2``) sin x). -Rewrite (derive_pt_sin ``x+PI/2``); Rewrite (sum_fct_cte_derive_pt ([x:R]``x``) x ``PI/2``). -Generalize (deriv_id x); Intro; Unfold derive in H0; Rewrite H0; Rewrite Rmult_1r; Rewrite Rplus_sym; Rewrite sin_cos; Rewrite Ropp_Ropp; Reflexivity. -Apply diff_id. -Apply (sum_fct_cte_derivable_pt ([x:R]x) x ``PI/2``); Apply diff_id. -Apply diff_sin. -Apply fct_eq; Intro; Symmetry; Rewrite Rplus_sym; Apply cos_sin. -Qed. - -Lemma derive_pt_cos : (x:R) (derive_pt cos x)==``-(sin x)``. -Intro; Generalize deriv_cos; Unfold derive; Intro; Unfold opp_fct in H; Apply (eq_fct x [x:R](derive_pt cos x) [x:R]``-(sin x)`` H). -Qed. - -(************************************************************) -(** Local extremum's condition *) -(************************************************************) -Theorem deriv_maximum : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f x)<=(f c)``)->``(derive_pt f c)==0``. -Intros; Case (total_order R0 (derive_pt f c)); Intro. -Generalize (derivable_derive f c H1); Intro; Elim H4; Intros l H5; Rewrite H5 in H3; Generalize (derive_pt_def_1 f c l H5); Intro. -Cut ``0<l/2``. -Intro; Elim (H6 ``l/2`` H7); Intros delta H8. -Cut ``0<(b-c)/2``. -Intro; Cut ``(Rmin delta/2 ((b-c)/2))<>0``. -Intro; Cut ``(Rabsolu (Rmin delta/2 ((b-c)/2)))<delta``. -Intro; Generalize (H8 ``(Rmin delta/2 ((b-c)/2))`` H10 H11); Intro; Cut ``0<(Rmin (delta/2) ((b-c)/2))``. -Intro; Cut ``a<c+(Rmin (delta/2) ((b-c)/2))``. -Cut ``c+(Rmin (delta/2) ((b-c)/2))<b``. -Intros; Generalize (H2 ``c+(Rmin (delta/2) ((b-c)/2))`` H15 H14); Intro; Cut ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))<=0``. -Intro; Cut ``-l<0``. -Intro; Unfold Rminus in H12. -Cut ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l<0``. -Intro; Cut ``(Rabsolu (((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)) < l/2``. -Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l``); Intro. -Replace `` -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)`` with ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))``. -Intro; Generalize (Rlt_compatibility ``-l`` ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``l/2`` H20); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Replace ``-l+l/2`` with ``-(l/2)``. -Intro; Generalize (Rlt_Ropp ``-(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``-(l/2)`` H21); Repeat Rewrite Ropp_Ropp; Intro; Generalize (Rlt_trans ``0`` ``l/2`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` H7 H22); Intro; Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` ``0`` H23 H17)). -Pattern 2 l; Rewrite double_var. -Rewrite Ropp_distr1. -Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l. -Symmetry; Apply Rplus_Or. -Ring. -Intro; Generalize (Rle_sym2 ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` r); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` ``0`` H21 H19)). -Assumption. -Rewrite <- Ropp_O; Replace ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` with ``-(l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2))))``. -Apply Rgt_Ropp; Change ``0<l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2)))``; Apply gt0_plus_ge0_is_gt0; [Assumption | Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Assumption]. -Ring. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Replace ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))`` with ``- (((f c)-(f (c+(Rmin (delta/2) ((b-c)/2)))))/(Rmin (delta/2) ((b-c)/2)))``. -Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos; [Generalize (Rle_compatibility_r ``-(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` ``(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` (f c) H16); Rewrite Rplus_Ropp_r; Intro; Assumption | Left; Apply Rlt_Rinv; Assumption]. -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Repeat Rewrite <- (Rmult_sym ``/(Rmin (delta*/2) ((b-c)*/2))``). -Apply r_Rmult_mult with ``(Rmin (delta*/2) ((b-c)*/2))``. -Repeat Rewrite <- Rmult_assoc. -Rewrite <- Rinv_r_sym. -Repeat Rewrite Rmult_1l. -Ring. -Red; Intro. -Unfold Rdiv in H13; Rewrite H17 in H13; Elim (Rlt_antirefl ``0`` H13). -Red; Intro. -Unfold Rdiv in H13; Rewrite H17 in H13; Elim (Rlt_antirefl ``0`` H13). -Generalize (Rmin_r ``(delta/2)`` ``((b-c)/2)``); Intro; Generalize (Rle_compatibility ``c`` ``(Rmin (delta/2) ((b-c)/2))`` ``(b-c)/2`` H14); Intro; Apply Rle_lt_trans with ``c+(b-c)/2``. -Assumption. -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Replace ``2*(c+(b-c)/2)`` with ``c+b``. -Replace ``2*b`` with ``b+b``. -Apply Rlt_compatibility_r; Assumption. -Ring. -Unfold Rdiv; Rewrite Rmult_Rplus_distr. -Repeat Rewrite (Rmult_sym ``2``). -Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Ring. -Apply aze. -Apply Rlt_trans with c. -Assumption. -Pattern 1 c; Rewrite <- (Rplus_Or c); Apply Rlt_compatibility; Assumption. -Cut ``0<delta/2``. -Intro; Apply (Rmin_stable_in_posreal (mkposreal ``delta/2`` H13) (mkposreal ``(b-c)/2`` H9)). -Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Unfold Rabsolu; Case (case_Rabsolu (Rmin ``delta/2`` ``(b-c)/2``)). -Intro. -Cut ``0<delta/2``. -Intro. -Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H11) (mkposreal ``(b-c)/2`` H9)); Simpl; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rmin (delta/2) ((b-c)/2))`` ``0`` H12 r)). -Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Intro; Apply Rle_lt_trans with ``delta/2``. -Apply Rmin_l. -Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l. -Replace ``2*delta`` with ``delta+delta``. -Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility. -Rewrite Rplus_Or; Apply (cond_pos delta). -Symmetry; Apply double. -Apply aze. -Cut ``0<delta/2``. -Intro; Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H10) (mkposreal ``(b-c)/2`` H9)); Simpl; Intro; Red; Intro; Rewrite H12 in H11; Elim (Rlt_antirefl ``0`` H11). -Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Unfold Rdiv; Apply Rmult_lt_pos. -Generalize (Rlt_compatibility_r ``-c`` c b H0); Rewrite Rplus_Ropp_r; Intro; Assumption. -Apply Rlt_Rinv; Apply Rgt_2_0. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. -Elim H3; Intro. -Symmetry; Assumption. -Generalize (derivable_derive f c H1); Intro; Elim H5; Intros l H6; Rewrite H6 in H4; Generalize (derive_pt_def_1 f c l H6); Intro; Cut ``0< -(l/2)``. -Intro; Elim (H7 ``-(l/2)`` H8); Intros delta H9. -Cut ``0<(c-a)/2``. -Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<0``. -Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<>0``. -Intro; Cut ``(Rabsolu (Rmax (-(delta/2)) ((a-c)/2)))<delta``. -Intro; Generalize (H9 ``(Rmax (-(delta/2)) ((a-c)/2))`` H12 H13); Intro; Cut ``a<c+(Rmax (-(delta/2)) ((a-c)/2))``. -Cut ``c+(Rmax (-(delta/2)) ((a-c)/2))<b``. -Intros; Generalize (H2 ``c+(Rmax (-(delta/2)) ((a-c)/2))`` H16 H15); Intro; Cut ``0<=((f (c+(Rmax (-(delta/2)) ((a-c)/2))))-(f c))/(Rmax (-(delta/2)) ((a-c)/2))``. -Intro; Cut ``0< -l``. -Intro; Unfold Rminus in H14; Cut ``0<((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``. -Intro; Cut ``(Rabsolu (((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l)) < -(l/2)``. -Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``). -Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))+ -l`` ``0`` H20 r)). -Intros; Generalize (Rlt_compatibility_r ``l`` ``(((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2)))+ -l`` ``-(l/2)`` H21); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Replace ``-(l/2)+l`` with ``l/2``. -Cut ``l/2<0``. -Intros; Generalize (Rlt_trans ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))`` ``l/2`` ``0`` H23 H22); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a-c)/2))))-(f c))/(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H18 H24)). -Rewrite <- (Ropp_Ropp ``l/2``); Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Pattern 3 l; Rewrite double_var. -Ring. -Assumption. -Apply ge0_plus_gt0_is_gt0; Assumption. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Unfold Rdiv; Replace ``((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))*/(Rmax ( -(delta*/2)) ((a-c)*/2))`` with ``(-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c)))*/(-(Rmax ( -(delta*/2)) ((a-c)*/2)))``. -Apply Rmult_le_pos. -Generalize (Rle_compatibility ``-(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` ``(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` (f c) H17); Rewrite Rplus_Ropp_l; Replace ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))`` with ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2)))))+(f c)``. -Intro; Assumption. -Ring. -Left; Apply Rlt_Rinv; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Unfold Rdiv. -Rewrite <- Ropp_Rinv. -Rewrite Ropp_mul2. -Reflexivity. -Unfold Rdiv in H12; Assumption. -Generalize (Rlt_compatibility c ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H11); Rewrite Rplus_Or; Intro; Apply Rlt_trans with ``c``; Assumption. -Generalize (RmaxLess2 ``(-(delta/2))`` ``((a-c)/2)``); Intro; Generalize (Rle_compatibility c ``(a-c)/2`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H15); Intro; Apply Rlt_le_trans with ``c+(a-c)/2``. -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Replace ``2*(c+(a-c)/2)`` with ``a+c``. -Rewrite double. -Apply Rlt_compatibility; Assumption. -Ring. -Rewrite <- Rplus_assoc. -Rewrite <- double_var. -Ring. -Assumption. -Unfold Rabsolu; Case (case_Rabsolu (Rmax ``-(delta/2)`` ``(a-c)/2``)). -Intro; Generalize (RmaxLess1 ``-(delta/2)`` ``(a-c)/2``); Intro; Generalize (Rle_Ropp ``-(delta/2)`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H13); Rewrite Ropp_Ropp; Intro; Generalize (Rle_sym2 ``-(Rmax ( -(delta/2)) ((a-c)/2))`` ``delta/2`` H14); Intro; Apply Rle_lt_trans with ``delta/2``. -Assumption. -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l; Rewrite double. -Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility; Rewrite Rplus_Or; Apply (cond_pos delta). -Apply aze. -Cut ``-(delta/2) < 0``. -Cut ``(a-c)/2<0``. -Intros; Generalize (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H14) (mknegreal ``(a-c)/2`` H13)); Simpl; Intro; Generalize (Rle_sym2 ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` r); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H16 H15)). -Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``. -Assumption. -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Rewrite (Ropp_distr2 a c). -Reflexivity. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. -Red; Intro; Rewrite H12 in H11; Elim (Rlt_antirefl ``0`` H11). -Cut ``(a-c)/2<0``. -Intro; Cut ``-(delta/2)<0``. -Intro; Apply (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H12) (mknegreal ``(a-c)/2`` H11)). -Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. -Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``. -Assumption. -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Rewrite (Ropp_distr2 a c). -Reflexivity. -Unfold Rdiv; Apply Rmult_lt_pos; [Generalize (Rlt_compatibility_r ``-a`` a c H); Rewrite Rplus_Ropp_r; Intro; Assumption | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. -Replace ``-(l/2)`` with ``(-l)/2``. -Unfold Rdiv; Apply Rmult_lt_pos. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Apply (Rlt_Rinv ``2`` Rgt_2_0). -Unfold Rdiv; Apply Ropp_mul1. -Qed. - -Theorem deriv_minimum : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f c)<=(f x)``)->``(derive_pt f c)==0``. -Intros; Generalize (opposite_derivable_pt f c H1); Intro; Rewrite <- (Ropp_Ropp (derive_pt f c)); Apply eq_RoppO; Rewrite <- (deriv_opposite f c H1); Apply (deriv_maximum (opp_fct f) a b c H H0 H3); Intros; Unfold opp_fct; Apply Rge_Ropp; Apply Rle_sym1; Apply (H2 x H4 H5). -Qed. - -Theorem deriv_constant2 : (f:R->R;a,b,c:R) ``a<c``->``c<b``->(derivable_pt f c)->((x:R) ``a<x``->``x<b``->``(f x)==(f c)``)->``(derive_pt f c)==0``. -Intros; Apply (deriv_maximum f a b c H H0 H1); Intros; Right; Apply (H2 x H3 H4). -Qed. - -(**********) -Lemma nonneg_derivative_0 : (f:R->R) (derivable f)->(increasing f) -> ((x:R) ``0<=(derive_pt f x)``). -Intros; Unfold increasing in H0; Generalize (derivable_derive f x (H x)); Intro; Elim H1; Intros l H2. -Rewrite H2; Case (total_order R0 l); Intro. -Left; Assumption. -Elim H3; Intro. -Right; Assumption. -Generalize (derive_pt_def_1 f x l H2); Intros; Cut ``0< -(l/2)``. -Intro; Elim (H5 ``-(l/2)`` H6); Intros delta H7; Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``. -Intro; Decompose [and] H8; Intros; Generalize (H7 ``delta/2`` H9 H12); Cut ``0<=((f (x+delta/2))-(f x))/(delta/2)``. -Intro; Cut ``0<=((f (x+delta/2))-(f x))/(delta/2)-l``. -Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``). -Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` H13 r)). -Intros; Generalize (Rlt_compatibility_r l ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``-(l/2)`` H14); Unfold Rminus; Replace ``-(l/2)+l`` with ``l/2``. -Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Intro; Generalize (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``l/2`` H10 H15); Intro; Cut ``l/2<0``. -Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``l/2`` ``0`` H16 H17)). -Rewrite <- Ropp_O in H6; Generalize (Rlt_Ropp ``-0`` ``-(l/2)`` H6); Repeat Rewrite Ropp_Ropp; Intro; Assumption. -Pattern 3 l ; Rewrite double_var. -Ring. -Unfold Rminus; Apply ge0_plus_ge0_is_ge0. -Unfold Rdiv; Apply Rmult_le_pos. -Cut ``x<=(x+(delta*/2))``. -Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` H14); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. -Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. -Left; Apply Rlt_Rinv; Assumption. -Left; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. -Unfold Rdiv; Apply Rmult_le_pos. -Cut ``x<=(x+(delta*/2))``. -Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. -Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. -Left; Apply Rlt_Rinv; Assumption. -Split. -Unfold Rdiv; Apply prod_neq_R0. -Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8). -Apply Rinv_neq_R0; DiscrR. -Split. -Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Unfold Rabsolu; Case (case_Rabsolu ``delta/2``). -Unfold Rdiv; Intro; Generalize (Rlt_monotony_r ``2`` ``delta*/2`` ``0`` Rgt_2_0 r); Rewrite Rmult_Ol; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` delta ``0`` (cond_pos delta) H8)). -DiscrR. -Intro; Unfold Rdiv; Pattern 1 delta; Replace ``(pos delta)`` with ``2*(delta*/2)``. -Replace ``2*(delta*/2)`` with ``delta*/2+delta*/2``. -Pattern 2 delta; Rewrite <- (Rplus_Or ``delta*/2``). -Apply Rlt_compatibility. -Rewrite Rplus_Or. -Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Ring. -Rewrite <- Rmult_assoc. -Apply Rinv_r_simpl_m. -Apply aze. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Generalize (Rlt_monotony_r ``/2`` l ``0`` (Rlt_Rinv ``2`` Rgt_2_0) H4); Rewrite Rmult_Ol; Intro; Assumption. -Qed. - -(**********) -Axiom nonneg_derivative_1 : (f:R->R) (derivable f)->((x:R) ``0<=(derive_pt f x)``) -> (increasing f). - -(**********) -Lemma nonpos_derivative_0 : (f:R->R) (derivable f)->(decreasing f) -> ((x:R) ``(derive_pt f x)<=0``). -Intros; Unfold decreasing in H0; Generalize (derivable_derive f x (H x)); Intro; Elim H1; Intros l H2. -Rewrite H2; Case (total_order l R0); Intro. -Left; Assumption. -Elim H3; Intro. -Right; Assumption. -Generalize (derive_pt_def_1 f x l H2); Intros; Cut ``0< (l/2)``. -Intro; Elim (H5 ``(l/2)`` H6); Intros delta H7; Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``. -Intro; Decompose [and] H8; Intros; Generalize (H7 ``delta/2`` H9 H12); Cut ``((f (x+delta/2))-(f x))/(delta/2)<=0``. -Intro; Cut ``0< -(((f (x+delta/2))-(f x))/(delta/2)-l)``. -Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``). -Intros; Generalize (Rlt_compatibility_r ``-l`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``(l/2)`` H14); Unfold Rminus. -Replace ``(l/2)+ -l`` with ``-(l/2)``. -Replace `` -(((f (x+delta/2))+ -(f x))/(delta/2)+ -l)+ -l`` with ``-(((f (x+delta/2))+ -(f x))/(delta/2))``. -Intro. -Generalize (Rlt_Ropp ``-(((f (x+delta/2))+ -(f x))/(delta/2))`` ``-(l/2)`` H15). -Repeat Rewrite Ropp_Ropp. -Intro. -Generalize (Rlt_trans ``0`` ``l/2`` ``((f (x+delta/2))-(f x))/(delta/2)`` H6 H16); Intro. -Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``0`` H17 H10)). -Ring. -Pattern 3 l; Rewrite double_var. -Ring. -Intros. -Generalize (Rge_Ropp ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` r). -Rewrite Ropp_O. -Intro. -Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``0`` H13 H15)). -Replace ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` with ``(((f (x))-(f (x+delta/2)))/(delta/2)) +l``. -Unfold Rminus. -Apply ge0_plus_gt0_is_gt0. -Unfold Rdiv; Apply Rmult_le_pos. -Cut ``x<=(x+(delta*/2))``. -Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H14); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. -Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. -Left; Apply Rlt_Rinv; Assumption. -Assumption. -Rewrite Ropp_distr2. -Unfold Rminus. -Rewrite (Rplus_sym l). -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Rewrite (Rplus_sym (f x)). -Reflexivity. -Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``. -Rewrite <- Ropp_O. -Apply Rge_Ropp. -Apply Rle_sym1. -Unfold Rdiv; Apply Rmult_le_pos. -Cut ``x<=(x+(delta*/2))``. -Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro. -Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. -Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. -Left; Apply Rlt_Rinv; Assumption. -Unfold Rdiv; Rewrite <- Ropp_mul1. -Rewrite Ropp_distr2. -Reflexivity. -Split. -Unfold Rdiv; Apply prod_neq_R0. -Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8). -Apply Rinv_neq_R0; DiscrR. -Split. -Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Unfold Rabsolu; Case (case_Rabsolu ``delta/2``). -Unfold Rdiv; Intro; Generalize (Rlt_monotony_r ``2`` ``delta*/2`` ``0`` Rgt_2_0 r); Rewrite Rmult_Ol; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` delta ``0`` (cond_pos delta) H8)). -DiscrR. -Intro; Unfold Rdiv; Pattern 1 delta; Replace ``(pos delta)`` with ``2*(delta*/2)``. -Replace ``2*(delta*/2)`` with ``delta*/2+delta*/2``. -Pattern 2 delta; Rewrite <- (Rplus_Or ``delta*/2``). -Apply Rlt_compatibility. -Rewrite Rplus_Or. -Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. -Ring. -Rewrite <- Rmult_assoc. -Apply Rinv_r_simpl_m. -Apply aze. -Unfold Rdiv; Apply Rmult_lt_pos. -Assumption. -Apply Rlt_Rinv; Apply Rgt_2_0. -Qed. - -(**********) -Lemma increasing_decreasing_opp : (f:R->R) (increasing f) -> (decreasing (opp_fct f)). -Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rge_Ropp; Apply Rle_sym1; Assumption. -Qed. - -(**********) -Lemma opp_opp_fct : (f:R->R) (opp_fct (opp_fct f))==f. -Intro; Unfold opp_fct; Apply fct_eq; Intro; Rewrite Ropp_Ropp; Reflexivity. -Qed. - -(**********) -Lemma nonpos_derivative_1 : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)<=0``) -> (decreasing f). -Intros; Rewrite <- (opp_opp_fct f); Apply increasing_decreasing_opp. -Cut (derivable (opp_fct f)). -Cut (x:R)``0<=(derive_pt (opp_fct f) x)``. -Intros; Apply (nonneg_derivative_1 (opp_fct f) H2 H1). -Intros; Rewrite (deriv_opposite f x (H x)); Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H0 x). -Apply (opposite_derivable f H). -Qed. - -(**********) -Axiom positive_derivative : (f:R->R) (derivable f)->((x:R) ``0<(derive_pt f x)``)->(strict_increasing f). - -(**********) -Lemma strictincreasing_strictdecreasing_opp : (f:R->R) (strict_increasing f) -> (strict_decreasing (opp_fct f)). -Unfold strict_increasing strict_decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rlt_Ropp; Assumption. -Qed. - -(**********) -Lemma negative_derivative : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)<0``)->(strict_decreasing f). -Intros; Rewrite <- (opp_opp_fct f); Apply strictincreasing_strictdecreasing_opp. -Cut (derivable (opp_fct f)). -Cut (x:R)``0<(derive_pt (opp_fct f) x)``. -Intros; Apply (positive_derivative (opp_fct f) H2 H1). -Intros; Rewrite (deriv_opposite f x (H x)); Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H0 x). -Apply (opposite_derivable f H). -Qed. - -(**********) -Lemma null_derivative_0 : (f:R->R) (constant f)->((x:R) ``(derive_pt f x)==0``). -Intros; Unfold constant in H; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Rewrite (H x ``x+h``); Unfold Rminus; Unfold Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. -Qed. - -(**********) -Lemma increasing_decreasing : (f:R->R) (increasing f) -> (decreasing f) -> (constant f). -Unfold increasing decreasing constant; Intros; Case (total_order x y); Intro. -Generalize (Rlt_le x y H1); Intro; Apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)). -Elim H1; Intro. -Rewrite H2; Reflexivity. -Generalize (Rlt_le y x H2); Intro; Symmetry; Apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). -Qed. - -(**********) -Lemma null_derivative_1 : (f:R->R) (derivable f)->((x:R) ``(derive_pt f x)==0``)->(constant f). -Intros. -Cut (x:R)``(derive_pt f x) <= 0``. -Cut (x:R)``0 <= (derive_pt f x)``. -Intros. -Generalize (nonneg_derivative_1 f H H1); Intro. -Generalize (nonpos_derivative_1 f H H2); Intro. -Apply increasing_decreasing; Assumption. -Intro. -Right; Symmetry; Apply (H0 x). -Intro; Right; Apply (H0 x). -Qed. - -(**********) -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). -Qed. - -(**********) -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). -Qed. +(*i $Id$ i*) -(**********) -(**********) -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)``. +Require Export Ranalysis1. +Require Export Ranalysis2. +Require Export Ranalysis3. +Require Export Ranalysis4. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v new file mode 100644 index 0000000000..0093c5d288 --- /dev/null +++ b/theories/Reals/Ranalysis1.v @@ -0,0 +1,1189 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require Rbase. +Require Rbasic_fun. +Require R_sqr. +Require Rlimit. +Require Rderiv. +Require DiscrR. +Require Rtrigo. +Require Specif. + +(****************************************************) +(** Basic operations on functions *) +(****************************************************) +Definition plus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)+(f2 x)``. +Definition opp_fct [f:R->R] : R->R := [x:R] ``-(f x)``. +Definition mult_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)*(f2 x)``. +Definition mult_real_fct [a:R;f:R->R] : R->R := [x:R] ``a*(f x)``. +Definition minus_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)-(f2 x)``. +Definition div_fct [f1,f2:R->R] : R->R := [x:R] ``(f1 x)/(f2 x)``. +Definition div_real_fct [a:R;f:R->R] : R->R := [x:R] ``a/(f x)``. +Definition comp [f1,f2:R->R] : R->R := [x:R] ``(f1 (f2 x))``. +Definition inv_fct [f:R->R] : R->R := [x:R]``/(f x)``. + +Definition fct_cte [a:R] : R->R := [x:R]a. +Definition id := [x:R]x. + +(****************************************************) +(** Variations of functions *) +(****************************************************) +Definition increasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f x)<=(f y)``. +Definition decreasing [f:R->R] : Prop := (x,y:R) ``x<=y``->``(f y)<=(f x)``. +Definition strict_increasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f x)<(f y)``. +Definition strict_decreasing [f:R->R] : Prop := (x,y:R) ``x<y``->``(f y)<(f x)``. +Definition constant [f:R->R] : Prop := (x,y:R) ``(f x)==(f y)``. + +(**********) +Axiom fct_eq : (f1,f2:R->R) ((x:R)(f1 x)==(f2 x))->f1==f2. + +(**********) +Definition no_cond : R->Prop := [x:R] True. + +(***************************************************) +(** Definition of continuity as a limit *) +(***************************************************) + +(**********) +Definition continuity_pt [f:R->R; x0:R] : Prop := (continue_in f no_cond x0). +Definition continuity [f:R->R] : Prop := (x:R) (continuity_pt f x). + + +(**********) +Lemma continuity_pt_plus : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (plus_fct f1 f2) x0). +Unfold continuity_pt plus_fct; Unfold continue_in; Intros; Apply limit_plus; Assumption. +Qed. + +Lemma continuity_pt_opp : (f:R->R; x0:R) (continuity_pt f x0) -> (continuity_pt (opp_fct f) x0). +Unfold continuity_pt opp_fct; Unfold continue_in; Intros; Apply limit_Ropp; Assumption. +Qed. + +Lemma continuity_pt_minus : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (minus_fct f1 f2) x0). +Unfold continuity_pt minus_fct; Unfold continue_in; Intros; Apply limit_minus; Assumption. +Qed. + +Lemma continuity_pt_mult : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> (continuity_pt (mult_fct f1 f2) x0). +Unfold continuity_pt mult_fct; Unfold continue_in; Intros; Apply limit_mul; Assumption. +Qed. + +Lemma continuity_pt_const : (f:R->R; x0:R) (constant f) -> (continuity_pt f x0). +Unfold constant continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split; [Apply Rlt_R0_R1 | Intros; Generalize (H x x0); Intro; Rewrite H2; Simpl; Rewrite R_dist_eq; Assumption]. +Qed. + +Lemma continuity_pt_scal : (f:R->R;a:R; x0:R) (continuity_pt f x0) -> (continuity_pt (mult_real_fct a f) x0). +Unfold continuity_pt mult_real_fct; Unfold continue_in; Intros; Apply (limit_mul ([x:R] a) f (D_x no_cond x0) a (f x0) x0). +Unfold limit1_in; Unfold limit_in; Intros; Exists ``1``; Split. +Apply Rlt_R0_R1. +Intros; Rewrite R_dist_eq; Assumption. +Assumption. +Qed. + +Lemma continuity_pt_inv : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (continuity_pt (inv_fct f) x0). +Intros. +Replace (inv_fct f) with [x:R]``/(f x)``. +Unfold continuity_pt; Unfold continue_in; Intros; Apply limit_inv; Assumption. +Unfold inv_fct; Reflexivity. +Qed. + +Lemma div_eq_inv : (f1,f2:R->R) (div_fct f1 f2)==(mult_fct f1 (inv_fct f2)). +Intros; Reflexivity. +Qed. + +Lemma continuity_pt_div : (f1,f2:R->R; x0:R) (continuity_pt f1 x0) -> (continuity_pt f2 x0) -> ~``(f2 x0)==0`` -> (continuity_pt (div_fct f1 f2) x0). +Intros; Rewrite -> (div_eq_inv f1 f2); Apply continuity_pt_mult; [Assumption | Apply continuity_pt_inv; Assumption]. +Qed. + +Lemma continuity_pt_comp : (f1,f2:R->R;x:R) (continuity_pt f1 x) -> (continuity_pt f2 (f1 x)) -> (continuity_pt (comp f2 f1) x). +Unfold continuity_pt; Unfold continue_in; Intros; Unfold comp. +Cut (limit1_in [x0:R](f2 (f1 x0)) (Dgf (D_x no_cond x) (D_x no_cond (f1 x)) f1) +(f2 (f1 x)) x) -> (limit1_in [x0:R](f2 (f1 x0)) (D_x no_cond x) (f2 (f1 x)) x). +Intro; Apply H1. +EApply limit_comp. +Apply H. +Apply H0. +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Assert H3 := (H1 eps H2). +Elim H3; Intros. +Exists x0. +Split. +Elim H4; Intros; Assumption. +Intros; Case (Req_EM (f1 x) (f1 x1)); Intro. +Rewrite H6; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Elim H4; Intros; Apply H8. +Split. +Unfold Dgf D_x no_cond. +Split. +Split. +Trivial. +Elim H5; Unfold D_x no_cond; Intros. +Elim H9; Intros; Assumption. +Split. +Trivial. +Assumption. +Elim H5; Intros; Assumption. +Qed. + +(**********) +Lemma continuity_plus : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (plus_fct f1 f2)). +Unfold continuity; Intros; Apply (continuity_pt_plus f1 f2 x (H x) (H0 x)). +Qed. + +Lemma continuity_opp : (f:R->R) (continuity f)->(continuity (opp_fct f)). +Unfold continuity; Intros; Apply (continuity_pt_opp f x (H x)). +Qed. + +Lemma continuity_minus : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (minus_fct f1 f2)). +Unfold continuity; Intros; Apply (continuity_pt_minus f1 f2 x (H x) (H0 x)). +Qed. + +Lemma continuity_mult : (f1,f2:R->R) (continuity f1)->(continuity f2)->(continuity (mult_fct f1 f2)). +Unfold continuity; Intros; Apply (continuity_pt_mult f1 f2 x (H x) (H0 x)). +Qed. + +Lemma continuity_const : (f:R->R) (constant f) -> (continuity f). +Unfold continuity; Intros; Apply (continuity_pt_const f x H). +Qed. + +Lemma continuity_scal : (f:R->R;a:R) (continuity f) -> (continuity (mult_real_fct a f)). +Unfold continuity; Intros; Apply (continuity_pt_scal f a x (H x)). +Qed. + +Lemma continuity_inv : (f:R->R) (continuity f)->((x:R) ~``(f x)==0``)->(continuity (inv_fct f)). +Unfold continuity; Intros; Apply (continuity_pt_inv f x (H x) (H0 x)). +Qed. + +Lemma continuity_div : (f1,f2:R->R) (continuity f1)->(continuity f2)->((x:R) ~``(f2 x)==0``)->(continuity (div_fct f1 f2)). +Unfold continuity; Intros; Apply (continuity_pt_div f1 f2 x (H x) (H0 x) (H1 x)). +Qed. + +Lemma continuity_comp : (f1,f2:R->R) (continuity f1) -> (continuity f2) -> (continuity (comp f2 f1)). +Unfold continuity; Intros. +Apply (continuity_pt_comp f1 f2 x (H x) (H0 (f1 x))). +Qed. + + +(*****************************************************) +(** Derivative's definition using Landau's kernel *) +(*****************************************************) + +Definition derivable_pt_lim [f:R->R;x,l:R] : Prop := ((eps:R) ``0<eps``->(EXT delta : posreal | ((h:R) ~``h==0``->``(Rabsolu h)<delta`` -> ``(Rabsolu ((((f (x+h))-(f x))/h)-l))<eps``))). + +Definition derivable_pt_abs [f:R->R;x:R] : R -> Prop := [l:R](derivable_pt_lim f x l). + +Definition SigT := Specif.sigT. +Definition derivable_pt [f:R->R;x:R] := (SigT R (derivable_pt_abs f x)). +Definition derivable [f:R->R] := (x:R)(derivable_pt f x). + +Definition derive_pt [f:R->R;x:R;pr:(derivable_pt f x)] := (projT1 ? ? pr). +Definition derive [f:R->R;pr:(derivable f)] := [x:R](derive_pt f x (pr x)). + +(************************************) +(** Class of differential functions *) +(************************************) +Record Differential : Type := mkDifferential { +d1 :> R->R; +cond_diff : (derivable d1) }. + +Record Differential_D2 : Type := mkDifferential_D2 { +d2 :> R->R; +cond_D1 : (derivable d2); +cond_D2 : (derivable (derive d2 cond_D1)) }. + +(**********) +Lemma unicite_step1 : (f:R->R;x,l1,l2:R) (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l1 R0) -> (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l2 R0) -> l1 == l2. +Intros; Apply (single_limit [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l1 l2 R0); Try Assumption. +Unfold adhDa; Intros; Exists ``alp/2``. +Split. +Unfold Rdiv; Apply prod_neq_R0. +Red; Intro; Rewrite H2 in H1; Elim (Rlt_antirefl ? H1). +Apply Rinv_neq_R0; DiscrR. +Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rabsolu_mult. +Replace ``(Rabsolu (/2))`` with ``/2``. +Replace (Rabsolu alp) with alp. +Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1r; Rewrite double; Pattern 1 alp; Replace alp with ``alp+0``; [Idtac | Ring]; Apply Rlt_compatibility; Assumption. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Symmetry; Apply Rabsolu_right; Left; Change ``0</2``; Apply Rlt_Rinv; Apply Rgt_2_0. +Qed. + +Lemma unicite_step2 : (f:R->R;x,l:R) (derivable_pt_lim f x l) -> (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l R0). +Unfold derivable_pt_lim; Intros; Unfold limit1_in; Unfold limit_in; Intros. +Assert H1 := (H eps H0). +Elim H1 ; Intros. +Exists (pos x0). +Split. +Apply (cond_pos x0). +Simpl; Unfold R_dist; Intros. +Elim H3; Intros. +Apply H2; [Assumption |Unfold Rminus in H5; Rewrite Ropp_O in H5; Rewrite Rplus_Or in H5; Assumption]. +Qed. + +Lemma unicite_step3 : (f:R->R;x,l:R) (limit1_in [h:R]``((f (x+h))-(f x))/h`` [h:R]``h<>0`` l R0) -> (derivable_pt_lim f x l). +Unfold limit1_in derivable_pt_lim; Unfold limit_in; Unfold dist; Simpl; Intros. +Elim (H eps H0). +Intros; Elim H1; Intros. +Exists (mkposreal x0 H2). +Simpl; Intros; Unfold R_dist in H3; Apply (H3 h). +Split; [Assumption | Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Assumption]. +Qed. + +Lemma unicite_limite : (f:R->R;x,l1,l2:R) (derivable_pt_lim f x l1) -> (derivable_pt_lim f x l2) -> l1==l2. +Intros. +Assert H1 := (unicite_step2 ? ? ? H). +Assert H2 := (unicite_step2 ? ? ? H0). +Assert H3 := (unicite_step1 ? ? ? ? H1 H2). +Assumption. +Qed. + +Lemma derive_pt_eq : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derive_pt f x pr)==l <-> (derivable_pt_lim f x l). +Intros; Split. +Intro; Assert H1 := (projT2 ? ? pr); Unfold derive_pt in H; Rewrite H in H1; Assumption. +Intro; Assert H1 := (projT2 ? ? pr); Unfold derivable_pt_abs in H1. +Assert H2 := (unicite_limite ? ? ? ? H H1). +Unfold derive_pt; Unfold derivable_pt_abs. +Symmetry; Assumption. +Qed. + +(**********) +Lemma derive_pt_eq_0 : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derivable_pt_lim f x l) -> (derive_pt f x pr)==l. +Intros; Elim (derive_pt_eq f x l pr); Intros. +Apply (H1 H). +Qed. + +(**********) +Lemma derive_pt_eq_1 : (f:R->R;x,l:R;pr:(derivable_pt f x)) (derive_pt f x pr)==l -> (derivable_pt_lim f x l). +Intros; Elim (derive_pt_eq f x l pr); Intros. +Apply (H0 H). +Qed. + + +(********************************************************************) +(** Equivalence of this definition with the one using limit concept *) +(********************************************************************) +Lemma derive_pt_D_in : (f,df:R->R;x:R;pr:(derivable_pt f x)) (D_in f df no_cond x) <-> (derive_pt f x pr)==(df x). +Intros; Split. +Unfold D_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros. +Apply derive_pt_eq_0. +Unfold derivable_pt_lim. +Intros; Elim (H eps H0); Intros alpha H1; Elim H1; Intros; Exists (mkposreal alpha H2); Intros; Generalize (H3 ``x+h``); Intro; Cut ``x+h-x==h``; [Intro; Cut ``(D_x no_cond x (x+h))``/\``(Rabsolu (x+h-x)) < alpha``; [Intro; Generalize (H6 H8); Rewrite H7; Intro; Assumption | Split; [Unfold D_x; Split; [Unfold no_cond; Trivial | Apply Rminus_not_eq_right; Rewrite H7; Assumption] | Rewrite H7; Assumption]] | Ring]. +Intro. +Assert H0 := (derive_pt_eq_1 f x (df x) pr H). +Unfold D_in; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H0 eps H1); Intros alpha H2; Exists (pos alpha); Split. +Apply (cond_pos alpha). +Intros; Elim H3; Intros; Unfold D_x in H4; Elim H4; Intros; Cut ``x0-x<>0``. +Intro; Generalize (H2 ``x0-x`` H8 H5); Replace ``x+(x0-x)`` with x0. +Intro; Assumption. +Ring. +Auto with real. +Qed. + +Lemma derivable_pt_lim_D_in : (f,df:R->R;x:R) (D_in f df no_cond x) <-> (derivable_pt_lim f x (df x)). +Intros; Split. +Unfold D_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros. +Unfold derivable_pt_lim. +Intros; Elim (H eps H0); Intros alpha H1; Elim H1; Intros; Exists (mkposreal alpha H2); Intros; Generalize (H3 ``x+h``); Intro; Cut ``x+h-x==h``; [Intro; Cut ``(D_x no_cond x (x+h))``/\``(Rabsolu (x+h-x)) < alpha``; [Intro; Generalize (H6 H8); Rewrite H7; Intro; Assumption | Split; [Unfold D_x; Split; [Unfold no_cond; Trivial | Apply Rminus_not_eq_right; Rewrite H7; Assumption] | Rewrite H7; Assumption]] | Ring]. +Intro. +Unfold derivable_pt_lim in H. +Unfold D_in; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H eps H0); Intros alpha H2; Exists (pos alpha); Split. +Apply (cond_pos alpha). +Intros. +Elim H1; Intros; Unfold D_x in H3; Elim H3; Intros; Cut ``x0-x<>0``. +Intro; Generalize (H2 ``x0-x`` H7 H4); Replace ``x+(x0-x)`` with x0. +Intro; Assumption. +Ring. +Auto with real. +Qed. + + +(***********************************) +(** derivability -> continuity *) +(***********************************) +(**********) +Lemma derivable_derive : (f:R->R;x:R;pr:(derivable_pt f x)) (EXT l : R | (derive_pt f x pr)==l). +Intros; Exists (projT1 ? ? pr). +Unfold derive_pt; Reflexivity. +Qed. + +Theorem derivable_continuous_pt : (f:R->R;x:R) (derivable_pt f x) -> (continuity_pt f x). +Intros. +Generalize (derivable_derive f x X); Intro. +Elim H; Intros l H1. +Cut l==((fct_cte l) x). +Intro. +Rewrite H0 in H1. +Generalize (derive_pt_D_in f (fct_cte l) x); Intro. +Elim (H2 X); Intros. +Generalize (H4 H1); Intro. +Unfold continuity_pt. +Apply (cont_deriv f (fct_cte l) no_cond x H5). +Unfold fct_cte; Reflexivity. +Qed. + +Theorem derivable_continuous : (f:R->R) (derivable f) -> (continuity f). +Unfold derivable continuity; Intros. +Apply (derivable_continuous_pt f x (X x)). +Qed. + +(****************************************************************) +(** Main rules *) +(****************************************************************) + +Lemma derivable_pt_lim_plus : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (plus_fct f1 f2) x ``l1+l2``). +Intros. +Apply unicite_step3. +Assert H1 := (unicite_step2 ? ? ? H). +Assert H2 := (unicite_step2 ? ? ? H0). +Unfold plus_fct; Replace [h:R]``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h`` with [h:R](Rplus ([h':R]``((f1 (x+h'))-(f1 x))/h'`` h) ([h':R]``((f2 (x+h'))-(f2 x))/h'`` h)). +Apply (limit_plus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). +Apply fct_eq; Intro; Unfold Rdiv; Ring. +Qed. + +Lemma derivable_pt_lim_opp : (f:R->R;x,l:R) (derivable_pt_lim f x l) -> (derivable_pt_lim (opp_fct f) x (Ropp l)). +Intros. +Apply unicite_step3. +Assert H1 := (unicite_step2 ? ? ? H). +Unfold opp_fct. +Replace [h:R]``( -(f (x+h))- -(f x))/h`` with [h:R](Ropp ``((f (x+h))-(f x))/h``). +Apply (limit_Ropp [h:R]``((f (x+h))-(f x))/h``[h:R]``h <> 0`` l ``0`` H1). +Apply fct_eq; Intro; Unfold Rdiv; Ring. +Qed. + +Lemma derivable_pt_lim_minus : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (minus_fct f1 f2) x ``l1-l2``). +Intros. +Apply unicite_step3. +Assert H1 := (unicite_step2 ? ? ? H). +Assert H2 := (unicite_step2 ? ? ? H0). +Unfold minus_fct. +Replace [h:R]``((f1 (x+h))-(f2 (x+h)) - ((f1 x)-(f2 x)))/h`` with [h:R](Rminus ([h':R]``((f1 (x+h'))-(f1 x))/h'`` h) ([h':R]``((f2 (x+h'))-(f2 x))/h'`` h)). +Apply (limit_minus [h':R]``((f1 (x+h'))-(f1 x))/h'`` [h':R]``((f2 (x+h'))-(f2 x))/h'`` [h:R]``h <> 0`` l1 l2 ``0`` H1 H2). +Apply fct_eq; Intro; Unfold Rdiv; Ring. +Qed. + +Lemma derivable_pt_lim_mult : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> (derivable_pt_lim (mult_fct f1 f2) x ``l1*(f2 x)+(f1 x)*l2``). +Intros. +Assert H1 := (derivable_pt_lim_D_in f1 [y:R]l1 x). +Elim H1; Intros. +Assert H4 := (H3 H). +Assert H5 := (derivable_pt_lim_D_in f2 [y:R]l2 x). +Elim H5; Intros. +Assert H8 := (H7 H0). +Clear H1 H2 H3 H5 H6 H7. +Assert H1 := (derivable_pt_lim_D_in (mult_fct f1 f2) [y:R]``l1*(f2 x)+(f1 x)*l2`` x). +Elim H1; Intros. +Clear H1 H3. +Apply H2. +Unfold mult_fct. +Apply (Dmult no_cond [y:R]l1 [y:R]l2 f1 f2 x); Assumption. +Qed. + +Lemma derivable_pt_lim_const : (a,x:R) (derivable_pt_lim (fct_cte a) x ``0``). +Intros; Unfold fct_cte derivable_pt_lim. +Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Unfold Rminus; Rewrite Rplus_Ropp_r; Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Qed. + +Lemma derivable_pt_lim_scal : (f:R->R;a,x,l:R) (derivable_pt_lim f x l) -> (derivable_pt_lim (mult_real_fct a f) x ``a*l``). +Intros. +Assert H0 := (derivable_pt_lim_const a x). +Replace (mult_real_fct a f) with (mult_fct (fct_cte a) f). +Replace ``a*l`` with ``0*(f x)+a*l``; [Idtac | Ring]. +Apply (derivable_pt_lim_mult (fct_cte a) f x ``0`` l); Assumption. +Unfold mult_real_fct mult_fct fct_cte; Reflexivity. +Qed. + +Lemma derivable_pt_lim_id : (x:R) (derivable_pt_lim id x ``1``). +Intro; Unfold derivable_pt_lim. +Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Unfold id; Replace ``(x+h-x)/h-1`` with ``0``. +Rewrite Rabsolu_R0; Apply Rle_lt_trans with ``(Rabsolu h)``. +Apply Rabsolu_pos. +Assumption. +Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. +Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. +Symmetry; Apply Rplus_Ropp_r. +Assumption. +Qed. + +Lemma derivable_pt_lim_Rsqr : (x:R) (derivable_pt_lim Rsqr x ``2*x``). +Intro; Unfold derivable_pt_lim. +Unfold Rsqr; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. +Assumption. +Replace ``(x+h)*(x+h)-x*x`` with ``2*x*h+h*h``; [Idtac | Ring]. +Unfold Rdiv; Rewrite Rmult_Rplus_distrl. +Repeat Rewrite Rmult_assoc. +Repeat Rewrite <- Rinv_r_sym; [Idtac | Assumption]. +Ring. +Qed. + +Lemma derivable_pt_lim_comp : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 (f1 x) l2) -> (derivable_pt_lim (comp f2 f1) x ``l2*l1``). +Intros; Assert H1 := (derivable_pt_lim_D_in f1 [y:R]l1 x). +Elim H1; Intros. +Assert H4 := (H3 H). +Assert H5 := (derivable_pt_lim_D_in f2 [y:R]l2 (f1 x)). +Elim H5; Intros. +Assert H8 := (H7 H0). +Clear H1 H2 H3 H5 H6 H7. +Assert H1 := (derivable_pt_lim_D_in (comp f2 f1) [y:R]``l2*l1`` x). +Elim H1; Intros. +Clear H1 H3; Apply H2. +Unfold comp; Cut (D_in [x0:R](f2 (f1 x0)) [y:R]``l2*l1`` (Dgf no_cond no_cond f1) x) -> (D_in [x0:R](f2 (f1 x0)) [y:R]``l2*l1`` no_cond x). +Intro; Apply H1. +Rewrite Rmult_sym; Apply (Dcomp no_cond no_cond [y:R]l1 [y:R]l2 f1 f2 x); Assumption. +Unfold Dgf D_in no_cond; Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H1 eps H3); Intros. +Exists x0; Intros; Split. +Elim H5; Intros; Assumption. +Intros; Elim H5; Intros; Apply H9; Split. +Unfold D_x; Split. +Split; Trivial. +Elim H6; Intros; Unfold D_x in H10; Elim H10; Intros; Assumption. +Elim H6; Intros; Assumption. +Qed. + +Axiom derivable_pt_lim_sqrt : (x:R) ``0<x`` -> (derivable_pt_lim sqrt x ``/(2*(sqrt x))``). + +Axiom derivable_pt_lim_sin : (x:R) (derivable_pt_lim sin x (cos x)). + +Lemma derivable_pt_lim_cos : (x:R) (derivable_pt_lim cos x ``-(sin x)``). +Intro; Cut (comp sin (plus_fct id (fct_cte ``PI/2``)))==cos. +Intro; Rewrite <- H. +Replace ``-(sin x)`` with (Rmult (cos ``x+PI/2``) (Rplus R1 R0)). +Apply derivable_pt_lim_comp. +Apply derivable_pt_lim_plus. +Apply derivable_pt_lim_id. +Apply derivable_pt_lim_const. +Replace (plus_fct id (fct_cte ``PI/2``) x) with ``x+PI/2``. +Apply derivable_pt_lim_sin. +Unfold plus_fct id fct_cte; Reflexivity. +Rewrite Rplus_Or; Rewrite Rmult_1r; Rewrite sin_cos; Rewrite Ropp_Ropp; Rewrite Rplus_sym; Reflexivity. +Unfold comp plus_fct id fct_cte; Apply fct_eq; Intro. +Rewrite cos_sin; Rewrite Rplus_sym; Reflexivity. +Qed. + +Lemma derivable_pt_plus : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (plus_fct f1 f2) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Elim X0; Intros. +Apply Specif.existT with ``x0+x1``. +Apply derivable_pt_lim_plus; Assumption. +Qed. + +Lemma derivable_pt_opp : (f:R->R;x:R) (derivable_pt f x) -> (derivable_pt (opp_fct f) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Apply Specif.existT with ``-x0``. +Apply derivable_pt_lim_opp; Assumption. +Qed. + +Lemma derivable_pt_minus : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (minus_fct f1 f2) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Elim X0; Intros. +Apply Specif.existT with ``x0-x1``. +Apply derivable_pt_lim_minus; Assumption. +Qed. + +Lemma derivable_pt_mult : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> (derivable_pt (mult_fct f1 f2) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Elim X0; Intros. +Apply Specif.existT with ``x0*(f2 x)+(f1 x)*x1``. +Apply derivable_pt_lim_mult; Assumption. +Qed. + +Lemma derivable_pt_const : (a,x:R) (derivable_pt (fct_cte a) x). +Intros; Unfold derivable_pt. +Apply Specif.existT with ``0``. +Apply derivable_pt_lim_const. +Qed. + +Lemma derivable_pt_scal : (f:R->R;a,x:R) (derivable_pt f x) -> (derivable_pt (mult_real_fct a f) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Apply Specif.existT with ``a*x0``. +Apply derivable_pt_lim_scal; Assumption. +Qed. + +Lemma derivable_pt_id : (x:R) (derivable_pt id x). +Unfold derivable_pt; Intro. +Exists ``1``. +Apply derivable_pt_lim_id. +Qed. + +Lemma derivable_pt_Rsqr : (x:R) (derivable_pt Rsqr x). +Unfold derivable_pt; Intro; Apply Specif.existT with ``2*x``. +Apply derivable_pt_lim_Rsqr. +Qed. + +Lemma derivable_pt_comp : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 (f1 x)) -> (derivable_pt (comp f2 f1) x). +Unfold derivable_pt; Intros. +Elim X; Intros. +Elim X0 ;Intros. +Apply Specif.existT with ``x1*x0``. +Apply derivable_pt_lim_comp; Assumption. +Qed. + +Lemma derivable_pt_sqrt : (x:R) ``0<x`` -> (derivable_pt sqrt x). +Unfold derivable_pt; Intros. +Apply Specif.existT with ``/(2*(sqrt x))``. +Apply derivable_pt_lim_sqrt; Assumption. +Qed. + +Lemma derivable_pt_sin : (x:R) (derivable_pt sin x). +Unfold derivable_pt; Intro. +Apply Specif.existT with (cos x). +Apply derivable_pt_lim_sin. +Qed. + +Lemma derivable_pt_cos : (x:R) (derivable_pt cos x). +Unfold derivable_pt; Intro. +Apply Specif.existT with ``-(sin x)``. +Apply derivable_pt_lim_cos. +Qed. + +Lemma derivable_plus : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (plus_fct f1 f2)). +Unfold derivable; Intros. +Apply (derivable_pt_plus ? ? x (X ?) (X0 ?)). +Qed. + +Lemma derivable_opp : (f:R->R) (derivable f) -> (derivable (opp_fct f)). +Unfold derivable; Intros. +Apply (derivable_pt_opp ? x (X ?)). +Qed. + +Lemma derivable_minus : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (minus_fct f1 f2)). +Unfold derivable; Intros. +Apply (derivable_pt_minus ? ? x (X ?) (X0 ?)). +Qed. + +Lemma derivable_mult : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (mult_fct f1 f2)). +Unfold derivable; Intros. +Apply (derivable_pt_mult ? ? x (X ?) (X0 ?)). +Qed. + +Lemma derivable_const : (a:R) (derivable (fct_cte a)). +Unfold derivable; Intros. +Apply derivable_pt_const. +Qed. + +Lemma derivable_scal : (f:R->R;a:R) (derivable f) -> (derivable (mult_real_fct a f)). +Unfold derivable; Intros. +Apply (derivable_pt_scal ? a x (X ?)). +Qed. + +Lemma derivable_id : (derivable id). +Unfold derivable; Intro; Apply derivable_pt_id. +Qed. + +Lemma derivable_Rsqr : (derivable Rsqr). +Unfold derivable; Intro; Apply derivable_pt_Rsqr. +Qed. + +Lemma derivable_comp : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> (derivable (comp f2 f1)). +Unfold derivable; Intros. +Apply (derivable_pt_comp ? ? x (X ?) (X0 ?)). +Qed. + +Lemma derivable_sin : (derivable sin). +Unfold derivable; Intro; Apply derivable_pt_sin. +Qed. + +Lemma derivable_cos : (derivable cos). +Unfold derivable; Intro; Apply derivable_pt_cos. +Qed. + +Lemma derive_pt_plus : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (plus_fct f1 f2) x (derivable_pt_plus ? ? ? pr1 pr2)) == (derive_pt f1 x pr1) + (derive_pt f2 x pr2)``. +Intros. +Assert H := (derivable_derive f1 x pr1). +Assert H0 := (derivable_derive f2 x pr2). +Assert H1 := (derivable_derive (plus_fct f1 f2) x (derivable_pt_plus ? ? ? pr1 pr2)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Elim H1; Clear H1; Intros l H1. +Rewrite H; Rewrite H0; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +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_plus; Assumption. +Qed. + +Lemma derive_pt_opp : (f:R->R;x:R;pr1:(derivable_pt f x)) ``(derive_pt (opp_fct f) x (derivable_pt_opp ? ? pr1)) == -(derive_pt f x pr1)``. +Intros. +Assert H := (derivable_derive f x pr1). +Assert H0 := (derivable_derive (opp_fct f) x (derivable_pt_opp ? ? pr1)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Rewrite H; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +Unfold derive_pt in H; Rewrite H in H3. +Apply derivable_pt_lim_opp; Assumption. +Qed. + +Lemma derive_pt_minus : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (minus_fct f1 f2) x (derivable_pt_minus ? ? ? pr1 pr2)) == (derive_pt f1 x pr1) - (derive_pt f2 x pr2)``. +Intros. +Assert H := (derivable_derive f1 x pr1). +Assert H0 := (derivable_derive f2 x pr2). +Assert H1 := (derivable_derive (minus_fct f1 f2) x (derivable_pt_minus ? ? ? pr1 pr2)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Elim H1; Clear H1; Intros l H1. +Rewrite H; Rewrite H0; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +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_minus; Assumption. +Qed. + +Lemma derive_pt_mult : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x)) ``(derive_pt (mult_fct f1 f2) x (derivable_pt_mult ? ? ? pr1 pr2)) == (derive_pt f1 x pr1)*(f2 x) + (f1 x)*(derive_pt f2 x pr2)``. +Intros. +Assert H := (derivable_derive f1 x pr1). +Assert H0 := (derivable_derive f2 x pr2). +Assert H1 := (derivable_derive (mult_fct f1 f2) x (derivable_pt_mult ? ? ? pr1 pr2)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Elim H1; Clear H1; Intros l H1. +Rewrite H; Rewrite H0; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +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_mult; Assumption. +Qed. + +Lemma derive_pt_const : (a,x:R) (derive_pt (fct_cte a) x (derivable_pt_const a x)) == R0. +Intros. +Apply derive_pt_eq_0. +Apply derivable_pt_lim_const. +Qed. + +Lemma derive_pt_scal : (f:R->R;a,x:R;pr:(derivable_pt f x)) ``(derive_pt (mult_real_fct a f) x (derivable_pt_scal ? ? ? pr)) == a * (derive_pt f x pr)``. +Intros. +Assert H := (derivable_derive f x pr). +Assert H0 := (derivable_derive (mult_real_fct a f) x (derivable_pt_scal ? ? ? pr)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Rewrite H; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr). +Unfold derive_pt in H; Rewrite H in H3. +Apply derivable_pt_lim_scal; Assumption. +Qed. + +Lemma derive_pt_id : (x:R) (derive_pt id x (derivable_pt_id ?))==R1. +Intros. +Apply derive_pt_eq_0. +Apply derivable_pt_lim_id. +Qed. + +Lemma derive_pt_Rsqr : (x:R) (derive_pt Rsqr x (derivable_pt_Rsqr ?)) == ``2*x``. +Intros. +Apply derive_pt_eq_0. +Apply derivable_pt_lim_Rsqr. +Qed. + +Lemma derive_pt_comp : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 (f1 x))) ``(derive_pt (comp f2 f1) x (derivable_pt_comp ? ? ? pr1 pr2)) == (derive_pt f2 (f1 x) pr2) * (derive_pt f1 x pr1)``. +Intros. +Assert H := (derivable_derive f1 x pr1). +Assert H0 := (derivable_derive f2 (f1 x) pr2). +Assert H1 := (derivable_derive (comp f2 f1) x (derivable_pt_comp ? ? ? pr1 pr2)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Elim H1; Clear H1; Intros l H1. +Rewrite H; Rewrite H0; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +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_comp; Assumption. +Qed. + +Lemma derive_pt_sqrt : (x:R;pr:``0<x``) ``(derive_pt sqrt x (derivable_pt_sqrt ? pr)) == /(2*(sqrt x))``. +Intros. +Apply derive_pt_eq_0. +Apply derivable_pt_lim_sqrt; Assumption. +Qed. + +Lemma derive_pt_sin : (x:R) ``(derive_pt sin x (derivable_pt_sin ?))==(cos x)``. +Intros; Apply derive_pt_eq_0. +Apply derivable_pt_lim_sin. +Qed. + +Lemma derive_pt_cos : (x:R) ``(derive_pt cos x (derivable_pt_cos ?))==-(sin x)``. +Intros; Apply derive_pt_eq_0. +Apply derivable_pt_lim_cos. +Qed. + +Lemma pr_nu : (f:R->R;x:R;pr1,pr2:(derivable_pt f x)) (derive_pt f x pr1)==(derive_pt f x pr2). +Intros. +Unfold derivable_pt in pr1. +Unfold derivable_pt in pr2. +Elim pr1; Intros. +Elim pr2; Intros. +Unfold derivable_pt_abs in p. +Unfold derivable_pt_abs in p0. +Simpl. +Apply (unicite_limite f x x0 x1 p p0). +Qed. + + +(************************************************************) +(** Local extremum's condition *) +(************************************************************) + +Theorem deriv_maximum : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f x)<=(f c)``)->``(derive_pt f c pr)==0``. +Intros; Case (total_order R0 (derive_pt f c pr)); Intro. +Assert H3 := (derivable_derive f c pr). +Elim H3; Intros l H4; Rewrite H4 in H2. +Assert H5 := (derive_pt_eq_1 f c l pr H4). +Cut ``0<l/2``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]]. +Elim (H5 ``l/2`` H6); Intros delta H7. +Cut ``0<(b-c)/2``. +Intro; Cut ``(Rmin delta/2 ((b-c)/2))<>0``. +Intro; Cut ``(Rabsolu (Rmin delta/2 ((b-c)/2)))<delta``. +Intro. +Assert H11 := (H7 ``(Rmin delta/2 ((b-c)/2))`` H9 H10). +Cut ``0<(Rmin (delta/2) ((b-c)/2))``. +Intro; Cut ``a<c+(Rmin (delta/2) ((b-c)/2))``. +Intro; Cut ``c+(Rmin (delta/2) ((b-c)/2))<b``. +Intro; Assert H15 := (H1 ``c+(Rmin (delta/2) ((b-c)/2))`` H13 H14). +Cut ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))<=0``. +Intro; Cut ``-l<0``. +Intro; Unfold Rminus in H11. +Cut ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l<0``. +Intro; Cut ``(Rabsolu (((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)) < l/2``. +Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l``); Intro. +Replace `` -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)`` with ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))``. +Intro; Generalize (Rlt_compatibility ``-l`` ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``l/2`` H19); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Replace ``-l+l/2`` with ``-(l/2)``. +Intro; Generalize (Rlt_Ropp ``-(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``-(l/2)`` H20); Repeat Rewrite Ropp_Ropp; Intro; Generalize (Rlt_trans ``0`` ``l/2`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` H6 H21); Intro; Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` ``0`` H22 H16)). +Pattern 2 l; Rewrite double_var. +Ring. +Ring. +Intro. +Assert H20 := (Rle_sym2 ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` r). +Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H20 H18)). +Assumption. +Rewrite <- Ropp_O; Replace ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` with ``-(l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2))))``. +Apply Rgt_Ropp; Change ``0<l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))-(f c))/(Rmin (delta/2) ((b+ -c)/2)))``; Apply gt0_plus_ge0_is_gt0; [Assumption | Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Assumption]. +Ring. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Replace ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))`` with ``- (((f c)-(f (c+(Rmin (delta/2) ((b-c)/2)))))/(Rmin (delta/2) ((b-c)/2)))``. +Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos; [Generalize (Rle_compatibility_r ``-(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` ``(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` (f c) H15); Rewrite Rplus_Ropp_r; Intro; Assumption | Left; Apply Rlt_Rinv; Assumption]. +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Repeat Rewrite <- (Rmult_sym ``/(Rmin (delta*/2) ((b-c)*/2))``). +Apply r_Rmult_mult with ``(Rmin (delta*/2) ((b-c)*/2))``. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_r_sym. +Repeat Rewrite Rmult_1l. +Ring. +Red; Intro. +Unfold Rdiv in H12; Rewrite H16 in H12; Elim (Rlt_antirefl ``0`` H12). +Red; Intro. +Unfold Rdiv in H12; Rewrite H16 in H12; Elim (Rlt_antirefl ``0`` H12). +Assert H14 := (Rmin_r ``(delta/2)`` ``((b-c)/2)``). +Assert H15 := (Rle_compatibility ``c`` ``(Rmin (delta/2) ((b-c)/2))`` ``(b-c)/2`` H14). +Apply Rle_lt_trans with ``c+(b-c)/2``. +Assumption. +Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Replace ``2*(c+(b-c)/2)`` with ``c+b``. +Replace ``2*b`` with ``b+b``. +Apply Rlt_compatibility_r; Assumption. +Ring. +Unfold Rdiv; Rewrite Rmult_Rplus_distr. +Repeat Rewrite (Rmult_sym ``2``). +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Ring. +Apply aze. +Apply Rlt_trans with c. +Assumption. +Pattern 1 c; Rewrite <- (Rplus_Or c); Apply Rlt_compatibility; Assumption. +Cut ``0<delta/2``. +Intro; Apply (Rmin_stable_in_posreal (mkposreal ``delta/2`` H12) (mkposreal ``(b-c)/2`` H8)). +Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rabsolu; Case (case_Rabsolu (Rmin ``delta/2`` ``(b-c)/2``)). +Intro. +Cut ``0<delta/2``. +Intro. +Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H10) (mkposreal ``(b-c)/2`` H8)); Simpl; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rmin (delta/2) ((b-c)/2))`` ``0`` H11 r)). +Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Intro; Apply Rle_lt_trans with ``delta/2``. +Apply Rmin_l. +Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l. +Replace ``2*delta`` with ``delta+delta``. +Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility. +Rewrite Rplus_Or; Apply (cond_pos delta). +Symmetry; Apply double. +Apply aze. +Cut ``0<delta/2``. +Intro; Generalize (Rmin_stable_in_posreal (mkposreal ``delta/2`` H9) (mkposreal ``(b-c)/2`` H8)); Simpl; Intro; Red; Intro; Rewrite H11 in H10; Elim (Rlt_antirefl ``0`` H10). +Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rdiv; Apply Rmult_lt_pos. +Generalize (Rlt_compatibility_r ``-c`` c b H0); Rewrite Rplus_Ropp_r; Intro; Assumption. +Apply Rlt_Rinv; Apply Rgt_2_0. +Elim H2; Intro. +Symmetry; Assumption. +Generalize (derivable_derive f c pr); Intro; Elim H4; Intros l H5. +Rewrite H5 in H3; Generalize (derive_pt_eq_1 f c l pr H5); Intro; Cut ``0< -(l/2)``. +Intro; Elim (H6 ``-(l/2)`` H7); Intros delta H9. +Cut ``0<(c-a)/2``. +Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<0``. +Intro; Cut ``(Rmax (-(delta/2)) ((a-c)/2))<>0``. +Intro; Cut ``(Rabsolu (Rmax (-(delta/2)) ((a-c)/2)))<delta``. +Intro; Generalize (H9 ``(Rmax (-(delta/2)) ((a-c)/2))`` H11 H12); Intro; Cut ``a<c+(Rmax (-(delta/2)) ((a-c)/2))``. +Cut ``c+(Rmax (-(delta/2)) ((a-c)/2))<b``. +Intros; Generalize (H1 ``c+(Rmax (-(delta/2)) ((a-c)/2))`` H15 H14); Intro; Cut ``0<=((f (c+(Rmax (-(delta/2)) ((a-c)/2))))-(f c))/(Rmax (-(delta/2)) ((a-c)/2))``. +Intro; Cut ``0< -l``. +Intro; Unfold Rminus in H13; Cut ``0<((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``. +Intro; Cut ``(Rabsolu (((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l)) < -(l/2)``. +Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2))+ -l``). +Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))+ -l`` ``0`` H19 r)). +Intros; Generalize (Rlt_compatibility_r ``l`` ``(((f (c+(Rmax (-(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax (-(delta/2)) ((a+ -c)/2)))+ -l`` ``-(l/2)`` H20); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Replace ``-(l/2)+l`` with ``l/2``. +Cut ``l/2<0``. +Intros; Generalize (Rlt_trans ``((f (c+(Rmax ( -(delta/2)) ((a+ -c)/2))))+ -(f c))/(Rmax ( -(delta/2)) ((a+ -c)/2))`` ``l/2`` ``0`` H22 H21); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (c+(Rmax ( -(delta/2)) ((a-c)/2))))-(f c))/(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H17 H23)). +Rewrite <- (Ropp_Ropp ``l/2``); Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Pattern 3 l; Rewrite double_var. +Ring. +Assumption. +Apply ge0_plus_gt0_is_gt0; Assumption. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Unfold Rdiv; Replace ``((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))*/(Rmax ( -(delta*/2)) ((a-c)*/2))`` with ``(-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c)))*/(-(Rmax ( -(delta*/2)) ((a-c)*/2)))``. +Apply Rmult_le_pos. +Generalize (Rle_compatibility ``-(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` ``(f (c+(Rmax (-(delta*/2)) ((a-c)*/2))))`` (f c) H16); Rewrite Rplus_Ropp_l; Replace ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2))))-(f c))`` with ``-((f (c+(Rmax ( -(delta*/2)) ((a-c)*/2)))))+(f c)``. +Intro; Assumption. +Ring. +Left; Apply Rlt_Rinv; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Unfold Rdiv. +Rewrite <- Ropp_Rinv. +Rewrite Ropp_mul2. +Reflexivity. +Unfold Rdiv in H11; Assumption. +Generalize (Rlt_compatibility c ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H10); Rewrite Rplus_Or; Intro; Apply Rlt_trans with ``c``; Assumption. +Generalize (RmaxLess2 ``(-(delta/2))`` ``((a-c)/2)``); Intro; Generalize (Rle_compatibility c ``(a-c)/2`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H14); Intro; Apply Rlt_le_trans with ``c+(a-c)/2``. +Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Replace ``2*(c+(a-c)/2)`` with ``a+c``. +Rewrite double. +Apply Rlt_compatibility; Assumption. +Ring. +Rewrite <- Rplus_assoc. +Rewrite <- double_var. +Ring. +Assumption. +Unfold Rabsolu; Case (case_Rabsolu (Rmax ``-(delta/2)`` ``(a-c)/2``)). +Intro; Generalize (RmaxLess1 ``-(delta/2)`` ``(a-c)/2``); Intro; Generalize (Rle_Ropp ``-(delta/2)`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` H12); Rewrite Ropp_Ropp; Intro; Generalize (Rle_sym2 ``-(Rmax ( -(delta/2)) ((a-c)/2))`` ``delta/2`` H13); Intro; Apply Rle_lt_trans with ``delta/2``. +Assumption. +Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l; Rewrite double. +Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility; Rewrite Rplus_Or; Apply (cond_pos delta). +Apply aze. +Cut ``-(delta/2) < 0``. +Cut ``(a-c)/2<0``. +Intros; Generalize (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H13) (mknegreal ``(a-c)/2`` H12)); Simpl; Intro; Generalize (Rle_sym2 ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` r); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``(Rmax ( -(delta/2)) ((a-c)/2))`` ``0`` H15 H14)). +Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``. +Assumption. +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Rewrite (Ropp_distr2 a c). +Reflexivity. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. +Red; Intro; Rewrite H11 in H10; Elim (Rlt_antirefl ``0`` H10). +Cut ``(a-c)/2<0``. +Intro; Cut ``-(delta/2)<0``. +Intro; Apply (Rmax_stable_in_negreal (mknegreal ``-(delta/2)`` H11) (mknegreal ``(a-c)/2`` H10)). +Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. +Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp ``(a-c)/2``); Apply Rlt_Ropp; Replace ``-((a-c)/2)`` with ``(c-a)/2``. +Assumption. +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Rewrite (Ropp_distr2 a c). +Reflexivity. +Unfold Rdiv; Apply Rmult_lt_pos; [Generalize (Rlt_compatibility_r ``-a`` a c H); Rewrite Rplus_Ropp_r; Intro; Assumption | Apply (Rlt_Rinv ``2`` Rgt_2_0)]. +Replace ``-(l/2)`` with ``(-l)/2``. +Unfold Rdiv; Apply Rmult_lt_pos. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Apply (Rlt_Rinv ``2`` Rgt_2_0). +Unfold Rdiv; Apply Ropp_mul1. +Qed. + +Theorem deriv_minimum : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f c)<=(f x)``)->``(derive_pt f c pr)==0``. +Intros. +Rewrite <- (Ropp_Ropp (derive_pt f c pr)). +Apply eq_RoppO. +Rewrite <- (derive_pt_opp f c pr). +Cut (x:R)(``a<x``->``x<b``->``((opp_fct f) x)<=((opp_fct f) c)``). +Intro. +Apply (deriv_maximum (opp_fct f) a b c (derivable_pt_opp ? ? pr) H H0 H2). +Intros; Unfold opp_fct; Apply Rge_Ropp; Apply Rle_sym1. +Apply (H1 x H2 H3). +Qed. + +Theorem deriv_constant2 : (f:R->R;a,b,c:R;pr:(derivable_pt f c)) ``a<c``->``c<b``->((x:R) ``a<x``->``x<b``->``(f x)==(f c)``)->``(derive_pt f c pr)==0``. +Intros. +EApply deriv_maximum with a b; Try Assumption. +Intros; Right; Apply (H1 x H2 H3). +Qed. + +(**********) +Lemma nonneg_derivative_0 : (f:R->R;pr:(derivable f)) (increasing f) -> ((x:R) ``0<=(derive_pt f x (pr x))``). +Intros; Unfold increasing in H. +Assert H0 := (derivable_derive f x (pr x)). +Elim H0; Intros l H1. +Rewrite H1; Case (total_order R0 l); Intro. +Left; Assumption. +Elim H2; Intro. +Right; Assumption. +Assert H4 := (derive_pt_eq_1 f x l (pr x) H1). +Cut ``0< -(l/2)``. +Intro; Elim (H4 ``-(l/2)`` H5); Intros delta H6. +Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``. +Intro; Decompose [and] H7; Intros; Generalize (H6 ``delta/2`` H8 H11); Cut ``0<=((f (x+delta/2))-(f x))/(delta/2)``. +Intro; Cut ``0<=((f (x+delta/2))-(f x))/(delta/2)-l``. +Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``). +Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` H12 r)). +Intros; Generalize (Rlt_compatibility_r l ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``-(l/2)`` H13); Unfold Rminus; Replace ``-(l/2)+l`` with ``l/2``. +Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Intro; Generalize (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``l/2`` H9 H14); Intro; Cut ``l/2<0``. +Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``l/2`` ``0`` H15 H16)). +Rewrite <- Ropp_O in H5; Generalize (Rlt_Ropp ``-0`` ``-(l/2)`` H5); Repeat Rewrite Ropp_Ropp; Intro; Assumption. +Pattern 3 l ; Rewrite double_var. +Ring. +Unfold Rminus; Apply ge0_plus_ge0_is_ge0. +Unfold Rdiv; Apply Rmult_le_pos. +Cut ``x<=(x+(delta*/2))``. +Intro; Generalize (H x ``x+(delta*/2)`` H12); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. +Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. +Left; Apply Rlt_Rinv; Assumption. +Left; Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Unfold Rdiv; Apply Rmult_le_pos. +Cut ``x<=(x+(delta*/2))``. +Intro; Generalize (H x ``x+(delta*/2)`` H9); Intro; Generalize (Rle_compatibility ``-(f x)`` ``(f x)`` ``(f (x+delta*/2))`` H12); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. +Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. +Left; Apply Rlt_Rinv; Assumption. +Split. +Unfold Rdiv; Apply prod_neq_R0. +Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H7; Elim (Rlt_antirefl ``0`` H7). +Apply Rinv_neq_R0; DiscrR. +Split. +Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Replace ``(Rabsolu delta/2)`` with ``delta/2``. +Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Rewrite (Rmult_sym ``2``). +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]. +Rewrite Rmult_1r. +Rewrite double. +Pattern 1 (pos delta); Rewrite <- Rplus_Or. +Apply Rlt_compatibility; Apply (cond_pos delta). +Symmetry; Apply Rabsolu_right. +Left; Change ``0<delta/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rdiv; Rewrite <- Ropp_mul1; Apply Rmult_lt_pos. +Apply Rlt_anti_compatibility with l. +Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Assumption. +Apply Rlt_Rinv; Apply Rgt_2_0. +Qed. + +(**********) +Axiom nonneg_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``0<=(derive_pt f x (pr x))``) -> (increasing f). + +(**********) +Lemma nonpos_derivative_0 : (f:R->R;pr:(derivable f)) (decreasing f) -> ((x:R) ``(derive_pt f x (pr x))<=0``). +Intros; Assert H0 :=H; Unfold decreasing in H0; Generalize (derivable_derive f x (pr x)); Intro; Elim H1; Intros l H2. +Rewrite H2; Case (total_order l R0); Intro. +Left; Assumption. +Elim H3; Intro. +Right; Assumption. +Generalize (derive_pt_eq_1 f x l (pr x) H2); Intros; Cut ``0< (l/2)``. +Intro; Elim (H5 ``(l/2)`` H6); Intros delta H7; Cut ``delta/2<>0``/\``0<delta/2``/\``(Rabsolu delta/2)<delta``. +Intro; Decompose [and] H8; Intros; Generalize (H7 ``delta/2`` H9 H12); Cut ``((f (x+delta/2))-(f x))/(delta/2)<=0``. +Intro; Cut ``0< -(((f (x+delta/2))-(f x))/(delta/2)-l)``. +Intro; Unfold Rabsolu; Case (case_Rabsolu ``((f (x+delta/2))-(f x))/(delta/2)-l``). +Intros; Generalize (Rlt_compatibility_r ``-l`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``(l/2)`` H14); Unfold Rminus. +Replace ``(l/2)+ -l`` with ``-(l/2)``. +Replace `` -(((f (x+delta/2))+ -(f x))/(delta/2)+ -l)+ -l`` with ``-(((f (x+delta/2))+ -(f x))/(delta/2))``. +Intro. +Generalize (Rlt_Ropp ``-(((f (x+delta/2))+ -(f x))/(delta/2))`` ``-(l/2)`` H15). +Repeat Rewrite Ropp_Ropp. +Intro. +Generalize (Rlt_trans ``0`` ``l/2`` ``((f (x+delta/2))-(f x))/(delta/2)`` H6 H16); Intro. +Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``0`` H17 H10)). +Ring. +Pattern 3 l; Rewrite double_var. +Ring. +Intros. +Generalize (Rge_Ropp ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` r). +Rewrite Ropp_O. +Intro. +Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` ``0`` H13 H15)). +Replace ``-(((f (x+delta/2))-(f x))/(delta/2)-l)`` with ``(((f (x))-(f (x+delta/2)))/(delta/2)) +l``. +Unfold Rminus. +Apply ge0_plus_gt0_is_gt0. +Unfold Rdiv; Apply Rmult_le_pos. +Cut ``x<=(x+(delta*/2))``. +Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H14); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. +Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. +Left; Apply Rlt_Rinv; Assumption. +Assumption. +Rewrite Ropp_distr2. +Unfold Rminus. +Rewrite (Rplus_sym l). +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Rewrite Ropp_distr1. +Rewrite Ropp_Ropp. +Rewrite (Rplus_sym (f x)). +Reflexivity. +Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``. +Rewrite <- Ropp_O. +Apply Rge_Ropp. +Apply Rle_sym1. +Unfold Rdiv; Apply Rmult_le_pos. +Cut ``x<=(x+(delta*/2))``. +Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro. +Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. +Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. +Left; Apply Rlt_Rinv; Assumption. +Unfold Rdiv; Rewrite <- Ropp_mul1. +Rewrite Ropp_distr2. +Reflexivity. +Split. +Unfold Rdiv; Apply prod_neq_R0. +Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8). +Apply Rinv_neq_R0; DiscrR. +Split. +Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rabsolu; Case (case_Rabsolu ``delta/2``). +Unfold Rdiv; Intro; Generalize (Rlt_monotony_r ``2`` ``delta*/2`` ``0`` Rgt_2_0 +r); Rewrite Rmult_Ol; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r; Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` delta ``0`` (cond_pos delta) H8)). +DiscrR. +Intro; Unfold Rdiv; Pattern 1 delta; Replace ``(pos delta)`` with ``2*(delta*/2)``. +Replace ``2*(delta*/2)`` with ``delta*/2+delta*/2``. +Pattern 2 delta; Rewrite <- (Rplus_Or ``delta*/2``). +Apply Rlt_compatibility. +Rewrite Rplus_Or. +Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. +Ring. +Rewrite <- Rmult_assoc. +Apply Rinv_r_simpl_m. +Apply aze. +Unfold Rdiv; Apply Rmult_lt_pos. +Assumption. +Apply Rlt_Rinv; Apply Rgt_2_0. +Qed. + +(**********) +Lemma increasing_decreasing_opp : (f:R->R) (increasing f) -> (decreasing (opp_fct f)). +Unfold increasing decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rge_Ropp; Apply Rle_sym1; Assumption. +Qed. + +(**********) +Lemma opp_opp_fct : (f:R->R) (opp_fct (opp_fct f))==f. +Intro; Unfold opp_fct; Apply fct_eq; Intro; Rewrite Ropp_Ropp; Reflexivity. +Qed. + + + +(**********) +Lemma nonpos_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<=0``) -> (decreasing f). +Intros; Rewrite <- (opp_opp_fct f); Apply increasing_decreasing_opp. +Cut (x:R)``0<=(derive_pt (opp_fct f) x ((derivable_opp f pr) x))``. +Intros. +Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H0). +Intro. +Assert H0 := (derive_pt_opp f x (pr x)). +Cut ``(derive_pt (opp_fct f) x (derivable_pt_opp f x (pr x)))==(derive_pt (opp_fct f) x (derivable_opp f pr x))``. +Intro. +Rewrite <- H1. +Rewrite H0. +Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x). +Apply pr_nu. +Qed. + +(**********) +Axiom positive_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``0<(derive_pt f x (pr x))``)->(strict_increasing f). + +(**********) +Lemma strictincreasing_strictdecreasing_opp : (f:R->R) (strict_increasing f) -> +(strict_decreasing (opp_fct f)). +Unfold strict_increasing strict_decreasing opp_fct; Intros; Generalize (H x y H0); Intro; Apply Rlt_Ropp; Assumption. +Qed. + +(**********) +Lemma negative_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<0``)->(strict_decreasing f). +Intros; Rewrite <- (opp_opp_fct f); Apply strictincreasing_strictdecreasing_opp. +Cut (x:R)``0<(derive_pt (opp_fct f) x (derivable_opp f pr x))``. +Intros; EApply positive_derivative; Apply H0. +Intro. +Assert H0 := (derive_pt_opp f x (pr x)). +Cut ``(derive_pt (opp_fct f) x (derivable_pt_opp f x (pr x)))==(derive_pt (opp_fct f) x (derivable_opp f pr x))``. +Intro. +Rewrite <- H1; Rewrite H0. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x). +Apply pr_nu. +Qed. + +(**********) +Lemma null_derivative_0 : (f:R->R;pr:(derivable f)) (constant f)->((x:R) ``(derive_pt f x (pr x))==0``). +Intros. +Unfold constant in H. +Apply derive_pt_eq_0. +Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Simpl; Intros. +Rewrite (H x ``x+h``); Unfold Rminus; Unfold Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Qed. + +(**********) +Lemma increasing_decreasing : (f:R->R) (increasing f) -> (decreasing f) -> (constant f). +Unfold increasing decreasing constant; Intros; Case (total_order x y); Intro. +Generalize (Rlt_le x y H1); Intro; Apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)). +Elim H1; Intro. +Rewrite H2; Reflexivity. +Generalize (Rlt_le y x H2); Intro; Symmetry; Apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). +Qed. + +(**********) +Lemma null_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))==0``)->(constant f). +Intros. +Cut (x:R)``(derive_pt f x (pr x)) <= 0``. +Cut (x:R)``0 <= (derive_pt f x (pr x))``. +Intros. +Assert H2 := (nonneg_derivative_1 f pr H0). +Assert H3 := (nonpos_derivative_1 f pr H1). +Apply increasing_decreasing; Assumption. +Intro; Right; Symmetry; Apply (H x). +Intro; Right; Apply (H x). +Qed. + +(**********) +Axiom derive_increasing_interv_ax : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> (((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr 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 (pr 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;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<(derive_pt f t (pr 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 pr H); Intro. +Elim H4; Intros H5 _; Apply (H5 H0 x y H1 H2 H3). +Qed. + +(**********) +Lemma derive_increasing_interv_var : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr 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 pr H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3). +Qed. + +(**********) +(**********) +Axiom IAF : (f,g:R->R;a,b:R;pr1:(derivable f);pr2:(derivable g)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt g c (pr2 c))<=(derive_pt f c (pr1 c))``) -> ``(g b)-(g a)<=(f b)-(f a)``. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v new file mode 100644 index 0000000000..c5a6bb4ceb --- /dev/null +++ b/theories/Reals/Ranalysis2.v @@ -0,0 +1,305 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require Rbase. +Require Rbasic_fun. +Require R_sqr. +Require Rlimit. +Require Rderiv. +Require DiscrR. +Require Rtrigo. +Require Ranalysis1. +Require Omega. + +(**********) +Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``. +Intros; Unfold Rdiv Rminus Rsqr. +Repeat Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_Rplus_distr; Repeat Rewrite Rinv_Rmult; Try Assumption. +Replace ``l1*(f2 x)*(/(f2 x)*/(f2 x))`` with ``l1*/(f2 x)*((f2 x)*/(f2 x))``; [Idtac | Ring]. +Replace ``l1*(/(f2 x)*/(f2 (x+h)))*(f2 x)`` with ``l1*/(f2 (x+h))*((f2 x)*/(f2 x))``; [Idtac | Ring]. +Replace ``l1*(/(f2 x)*/(f2 (x+h)))* -(f2 (x+h))`` with ``-(l1*/(f2 x)*((f2 (x+h))*/(f2 (x+h))))``; [Idtac | Ring]. +Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*((f2 (x+h))*/h)`` with ``(f1 x)*/(f2 x)*/h*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring]. +Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*( -(f2 x)*/h)`` with ``-((f1 x)*/(f2 (x+h))*/h*((f2 x)*/(f2 x)))``; [Idtac | Ring]. +Replace ``(l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))*(f2 (x+h)))`` with ``l2*(f1 x)*/(f2 x)*/(f2 x)*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring]. +Replace ``l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))* -(f2 x)`` with ``-(l2*(f1 x)*/(f2 x)*/(f2 (x+h))*((f2 x)*/(f2 x)))``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try Assumption Orelse Ring. +Apply prod_neq_R0; Assumption. +Qed. + +Lemma Rmin_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0 < (Rmin x y)``. +Intros; Unfold Rmin. +Case (total_order_Rle x y); Intro; Assumption. +Qed. + +Lemma Rgt_8_0 : ``0 < 8``. +Cut ~(O=(8)); [Intro H; Generalize (lt_INR_0 (8) (neq_O_lt (8) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H0; Assumption | Discriminate]. +Qed. + +Lemma Rgt_4_0 : ``0 < 4``. +Cut ~(O=(4)); [Intro H; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H0; Assumption | Discriminate]. +Qed. + +Lemma maj_term1 : (x,h,eps,l1,alp_f2:R;eps_f2,alp_f1d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f1d``->``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < (Rabsolu ((eps*(f2 x))/8))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f1d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) < eps/4``. +Intros. +Assert H7 := (H3 h H6). +Assert H8 := (H2 h H4 H5). +Apply Rle_lt_trans with ``2/(Rabsolu (f2 x))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony_r. +Apply Rabsolu_pos. +Rewrite Rabsolu_Rinv; [Left; Exact H7 | Assumption]. +Apply Rlt_le_trans with ``2/(Rabsolu (f2 x))*(Rabsolu ((eps*(f2 x))/8))``. +Apply Rlt_monotony. +Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption]. +Exact H8. +Right; Unfold Rdiv. +Repeat Rewrite Rabsolu_mult. +Rewrite Rabsolu_Rinv; DiscrR. +Replace ``(Rabsolu 8)`` with ``8``. +Replace ``8`` with ``2*4``; [Idtac | Ring]. +Rewrite Rinv_Rmult; [Idtac | DiscrR | DiscrR]. +Replace ``2*/(Rabsolu (f2 x))*((Rabsolu eps)*(Rabsolu (f2 x))*(/2*/4))`` with ``(Rabsolu eps)*/4*(2*/2)*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))``; [Idtac | Ring]. +Replace (Rabsolu eps) with eps. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_8_0. +Qed. + +Lemma maj_term2 : (x,h,eps,l1,alp_f2,alp_f2t2:R;eps_f2:posreal;f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2t2``->``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``)-> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2t2`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``l1<>0`` -> ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) < eps/4``. +Intros. +Assert H8 := (H3 h H6). +Assert H9 := (H2 h H5). +Apply Rle_lt_trans with ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Rewrite Rabsolu_mult; Apply Rle_monotony. +Apply Rabsolu_pos. +Rewrite <- (Rabsolu_Ropp ``(f2 x)-(f2 (x+h))``); Rewrite Ropp_distr2. +Left; Apply H9. +Apply Rlt_le_trans with ``(Rabsolu (2*l1/((f2 x)*(f2 x))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption Orelse DiscrR. +Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Apply prod_neq_R0; Try Assumption Orelse DiscrR. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption. +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Rewrite (Rmult_sym ``2``). +Replace ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; Try Assumption. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H8; Exact H8. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Right. +Unfold Rsqr Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*((Rabsolu l1)*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*(eps*((Rabsolu (f2 x))*(Rabsolu (f2 x)))*(/4*/2*/(Rabsolu l1)))`` with ``eps*/4*((Rabsolu l1)*/(Rabsolu l1))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try (Apply Rabsolu_no_R0; Assumption) Orelse DiscrR. +Ring. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_8_0. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Qed. + +Lemma maj_term3 : (x,h,eps,l2,alp_f2:R;eps_f2,alp_f2d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f2d``->``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < (Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) < eps/4``. +Intros. +Assert H8 := (H2 h H4 H5). +Assert H9 := (H3 h H6). +Apply Rle_lt_trans with ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony. +Apply Rabsolu_pos. +Left; Apply H8. +Apply Rlt_le_trans with ``(Rabsolu (2*(f1 x)/((f2 x)*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption. +Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption. +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Rewrite (Rmult_sym ``2``). +Replace ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; Assumption Orelse Idtac. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H9; Exact H9. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Right. +Unfold Rsqr Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))))`` with ``eps*/4*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_8_0. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Qed. + +Lemma maj_term4 : (x,h,eps,l2,alp_f2,alp_f2c:R;eps_f2:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2c`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``l2<>0`` -> ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x)))) < eps/4``. +Intros. +Assert H9 := (H2 h H5). +Assert H10 := (H3 h H6). +Apply Rle_lt_trans with ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony. +Apply Rabsolu_pos. +Left; Apply H9. +Apply Rlt_le_trans with ``(Rabsolu (2*l2*(f1 x)/((Rsqr (f2 x))*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Assumption Orelse Idtac. +Red; Intro H11; Rewrite H11 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Repeat Apply prod_neq_R0. +DiscrR. +Assumption. +Assumption. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse (Unfold Rsqr; Apply prod_neq_R0; Assumption). +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 x)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*((Rabsolu (/(f2 x)))*2)))``; [Idtac | Ring]. +Replace ``(Rabsolu l2)*(Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*(((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Unfold Rsqr; Apply prod_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; [Idtac | Assumption | Assumption]. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H10; Exact H10. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Right; Unfold Rsqr Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))*/(Rabsolu l2)))`` with ``eps*/4*((Rabsolu l2)*/(Rabsolu l2))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_2_0. +Symmetry; Apply Rabsolu_right; Left; Apply Rgt_8_0. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Apply prod_neq_R0; Assumption Orelse DiscrR. +Apply prod_neq_R0; Assumption. +Qed. + +Lemma D_x_no_cond : (x,a:R) ``a<>0`` -> (D_x no_cond x ``x+a``). +Intros. +Unfold D_x no_cond. +Split. +Trivial. +Apply Rminus_not_eq. +Unfold Rminus. +Rewrite Ropp_distr1. +Rewrite <- Rplus_assoc. +Rewrite Rplus_Ropp_r. +Rewrite Rplus_Ol. +Apply Ropp_neq; Assumption. +Qed. + +Lemma Rabsolu_4 : (a,b,c,d:R) ``(Rabsolu (a+b+c+d)) <= (Rabsolu a) + (Rabsolu b) + (Rabsolu c) + (Rabsolu d)``. +Intros. +Apply Rle_trans with ``(Rabsolu (a+b)) + (Rabsolu (c+d))``. +Replace ``a+b+c+d`` with ``(a+b)+(c+d)``; [Apply Rabsolu_triang | Ring]. +Apply Rle_trans with ``(Rabsolu a) + (Rabsolu b) + (Rabsolu (c+d))``. +Apply Rle_compatibility_r. +Apply Rabsolu_triang. +Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility. +Apply Rabsolu_triang. +Qed. + +Lemma Rlt_4 : (a,b,c,d,e,f,g,h:R) ``a < b`` -> ``c < d`` -> ``e < f `` -> ``g < h`` -> ``a+c+e+g < b+d+f+h``. +Intros; Apply Rlt_trans with ``b+c+e+g``. +Repeat Apply Rlt_compatibility_r; Assumption. +Repeat Rewrite Rplus_assoc; Apply Rlt_compatibility. +Apply Rlt_trans with ``d+e+g``. +Rewrite Rplus_assoc; Apply Rlt_compatibility_r; Assumption. +Rewrite Rplus_assoc; Apply Rlt_compatibility; Apply Rlt_trans with ``f+g``. +Apply Rlt_compatibility_r; Assumption. +Apply Rlt_compatibility; Assumption. +Qed. + +Lemma Rmin_2 : (a,b,c:R) ``a < b`` -> ``a < c`` -> ``a < (Rmin b c)``. +Intros; Unfold Rmin; Case (total_order_Rle b c); Intro; Assumption. +Qed. + +Lemma quadruple : (x:R) ``4*x == x + x + x + x``. +Intro; Ring. +Qed. + +Lemma quadruple_var : (x:R) `` x == x/4 + x/4 + x/4 + x/4``. +Intro; Rewrite <- quadruple. +Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m; DiscrR. +Reflexivity. +Qed. + +(**********) +Lemma continuous_neq_0 : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (EXT eps : posreal | (h:R) ``(Rabsolu h) < eps`` -> ~``(f (x0+h))==0``). +Intros; Unfold continuity_pt in H; Unfold continue_in in H; Unfold limit1_in in H; Unfold limit_in in H; Elim (H ``(Rabsolu ((f x0)/2))``). +Intros; Elim H1; Intros. +Exists (mkposreal x H2). +Intros; Assert H5 := (H3 ``x0+h``). +Cut ``(dist R_met (x0+h) x0) < x`` -> ``(dist R_met (f (x0+h)) (f x0)) < (Rabsolu ((f x0)/2))``. +Unfold dist; Simpl; Unfold R_dist; Replace ``x0+h-x0`` with h. +Intros; Assert H7 := (H6 H4). +Red; Intro. +Rewrite H8 in H7; Unfold Rminus in H7; Rewrite Rplus_Ol in H7; Rewrite Rabsolu_Ropp in H7; Unfold Rdiv in H7; Rewrite Rabsolu_mult in H7; Pattern 1 ``(Rabsolu (f x0)) `` in H7; Rewrite <- Rmult_1r in H7. +Cut ``0<(Rabsolu (f x0))``. +Intro; Assert H10 := (Rlt_monotony_contra ? ? ? H9 H7). +Cut ``(Rabsolu (/2))==/2``. +Intro; Rewrite H11 in H10; Assert H12 := (Rlt_monotony ``2`` ? ? Rgt_2_0 H10); Rewrite Rmult_1r in H12; Rewrite <- Rinv_r_sym in H12; [Idtac | DiscrR]. +Cut (Rlt (IZR `1`) (IZR `2`)). +Unfold IZR; Unfold INR convert; Simpl; Intro; Elim (Rlt_antirefl ``1`` (Rlt_trans ? ? ? H13 H12)). +Apply IZR_lt; Omega. +Unfold Rabsolu; Case (case_Rabsolu ``/2``); Intro. +Assert H11 := (Rlt_monotony ``2`` ? ? Rgt_2_0 r); Rewrite Rmult_Or in H11; Rewrite <- Rinv_r_sym in H11; [Idtac | DiscrR]. +Elim (Rlt_antirefl ``0`` (Rlt_trans ? ? ? Rlt_R0_R1 H11)). +Reflexivity. +Apply (Rabsolu_pos_lt ? H0). +Ring. +Assert H6 := (Req_EM ``x0`` ``x0+h``); Elim H6; Intro. +Intro; Rewrite <- H7; Unfold dist R_met; Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt. +Unfold Rdiv; Apply prod_neq_R0; [Assumption | Apply Rinv_neq_R0; DiscrR]. +Intro; Apply H5. +Split. +Unfold D_x no_cond. +Split; Trivial Orelse Assumption. +Assumption. +Change ``0 < (Rabsolu ((f x0)/2))``. +Apply Rabsolu_pos_lt; Unfold Rdiv; Apply prod_neq_R0. +Assumption. +Apply Rinv_neq_R0; DiscrR. +Qed. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v new file mode 100644 index 0000000000..2a12b2f45c --- /dev/null +++ b/theories/Reals/Ranalysis3.v @@ -0,0 +1,606 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require Rbase. +Require Rbasic_fun. +Require R_sqr. +Require Rlimit. +Require Rderiv. +Require DiscrR. +Require Rtrigo. +Require Ranalysis1. +Require Ranalysis2. + + +(* Division *) +Theorem derivable_pt_lim_div : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> ~``(f2 x)==0``-> (derivable_pt_lim (div_fct f1 f2) x ``(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))``). +Intros. +Cut (derivable_pt f2 x); [Intro | Unfold derivable_pt; Apply Specif.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. +Assert H3 := (derivable_continuous_pt ? ? X). +Unfold continuity_pt in H3; Unfold continue_in in H3; Unfold limit1_in in H3; Unfold limit_in in H3; Unfold dist in H3. +Simpl in H3; Unfold R_dist in H3. +Elim (H3 ``(Rabsolu (f2 x))/2``); [Idtac | Unfold Rdiv; Change ``0 < (Rabsolu (f2 x))*/2``; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]]. +Clear H3; Intros alp_f2 H3. +Cut (x0:R) ``(Rabsolu (x0-x)) < alp_f2`` ->``(Rabsolu ((f2 x0)-(f2 x))) < (Rabsolu (f2 x))/2``. +Intro H4. +Cut (a:R) ``(Rabsolu (a-x)) < alp_f2``->``(Rabsolu (f2 x))/2 < (Rabsolu (f2 a))``. +Intro H5. +Cut (a:R) ``(Rabsolu (a)) < (Rmin eps_f2 alp_f2)`` -> ``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``. +Intro Maj. +Unfold derivable_pt_lim; Intros. +Elim (H ``(Rabsolu ((eps*(f2 x))/8))``); [Idtac | Unfold Rdiv; Change ``0 < (Rabsolu (eps*(f2 x)*/8))``; Apply Rabsolu_pos_lt; Repeat Apply prod_neq_R0; [Red; Intro H7; Rewrite H7 in H6; Elim (Rlt_antirefl ? H6) | Assumption | Apply Rinv_neq_R0; DiscrR]]. +Intros alp_f1d H7. +Case (Req_EM (f1 x) R0); Intro. +Case (Req_EM l1 R0); Intro. +(***********************************) +(* Cas n° 1 *) +(* (f1 x)=0 l1 =0 *) +(***********************************) +Cut ``0 < (Rmin eps_f2 (Rmin alp_f2 alp_f1d))``; [Intro | Repeat Apply Rmin_pos; [Apply (cond_pos eps_f2) | Elim H3; Intros; Assumption | Apply (cond_pos alp_f1d)]]. +Exists (mkposreal (Rmin eps_f2 (Rmin alp_f2 alp_f1d)) H10). +Simpl; Intros. +Assert H13 := (Rlt_le_trans ? ? ? H12 (Rmin_r ? ?)). +Assert H14 := (Rlt_le_trans ? ? ? H12 (Rmin_l ? ?)). +Assert H15 := (Rlt_le_trans ? ? ? H13 (Rmin_r ? ?)). +Assert H16 := (Rlt_le_trans ? ? ? H13 (Rmin_l ? ?)). +Assert H17 := (H7 ? H11 H15). +Rewrite formule; [Idtac | Assumption | Assumption | Apply H2; Apply H14]. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite H8. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite H8. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite H9. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Try Assumption Orelse Apply H2. +Apply H14. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +(***********************************) +(* Cas n° 2 *) +(* (f1 x)=0 l1<>0 *) +(***********************************) +Assert H10 := (derivable_continuous_pt ? ? X). +Unfold continuity_pt in H10. +Unfold continue_in in H10. +Unfold limit1_in in H10. +Unfold limit_in in H10. +Unfold dist in H10. +Simpl in H10. +Unfold R_dist in H10. +Elim (H10 ``(Rabsolu (eps*(Rsqr (f2 x)))/(8*l1))``); [Idtac | Change ``0<(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``; Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; [Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6) | Assumption | Assumption | Apply Rinv_neq_R0; Apply prod_neq_R0; [DiscrR | Assumption]]]. +Clear H10; Intros alp_f2t2 H10. +Cut (a:R) ``(Rabsolu a) < alp_f2t2`` -> ``(Rabsolu ((f2 (x+a)) - (f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Intro H11. +Cut ``0 < (Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2))``. +Intro. +Exists (mkposreal (Rmin (Rmin eps_f2 alp_f1d) (Rmin alp_f2 alp_f2t2)) H12). +Simpl. +Intros. +Assert H15 := (Rlt_le_trans ? ? ? H14 (Rmin_r ? ?)). +Assert H16 := (Rlt_le_trans ? ? ? H14 (Rmin_l ? ?)). +Assert H17 := (Rlt_le_trans ? ? ? H15 (Rmin_l ? ?)). +Assert H18 := (Rlt_le_trans ? ? ? H15 (Rmin_r ? ?)). +Assert H19 := (Rlt_le_trans ? ? ? H16 (Rmin_l ? ?)). +Assert H20 := (Rlt_le_trans ? ? ? H16 (Rmin_r ? ?)). +Clear H14 H15 H16. +Rewrite formule; Try Assumption. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite H8. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite H8. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +Apply H2; Assumption. +Repeat Apply Rmin_pos. +Apply (cond_pos eps_f2). +Apply (cond_pos alp_f1d). +Elim H3; Intros; Assumption. +Elim H10; Intros; Assumption. +Intros. +Elim H10; Intros. +Case (Req_EM a R0); Intro. +Rewrite H14; Rewrite Rplus_Or. +Unfold Rminus; Rewrite Rplus_Ropp_r. +Rewrite Rabsolu_R0. +Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc. +Repeat Apply prod_neq_R0; Try Assumption. +Red; Intro; Rewrite H15 in H6; Elim (Rlt_antirefl ? H6). +Apply Rinv_neq_R0; Apply prod_neq_R0; [DiscrR | Assumption]. +Apply H13. +Split. +Apply D_x_no_cond; Assumption. +Replace ``x+a-x`` with a; [Assumption | Ring]. +(***********************************) +(* Cas n° 3 *) +(* (f1 x)<>0 l1=0 l2=0 *) +(***********************************) +Case (Req_EM l1 R0); Intro. +Case (Req_EM l2 R0); Intro. +Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``); [Idtac | Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; [Assumption | Assumption | Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6) | Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption]]. +Intros alp_f2d H12. +Cut ``0 < (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d))``. +Intro. +Exists (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)) H11). +Simpl. +Intros. +Assert H15 := (Rlt_le_trans ? ? ? H14 (Rmin_l ? ?)). +Assert H16 := (Rlt_le_trans ? ? ? H14 (Rmin_r ? ?)). +Assert H17 := (Rlt_le_trans ? ? ? H15 (Rmin_l ? ?)). +Assert H18 := (Rlt_le_trans ? ? ? H15 (Rmin_r ? ?)). +Assert H19 := (Rlt_le_trans ? ? ? H16 (Rmin_l ? ?)). +Assert H20 := (Rlt_le_trans ? ? ? H16 (Rmin_r ? ?)). +Clear H15 H16. +Rewrite formule; Try Assumption. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite H10. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite H9. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Assumption Orelse Idtac. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +Apply H2; Assumption. +Repeat Apply Rmin_pos. +Apply (cond_pos eps_f2). +Elim H3; Intros; Assumption. +Apply (cond_pos alp_f1d). +Apply (cond_pos alp_f2d). +(***********************************) +(* Cas n° 4 *) +(* (f1 x)<>0 l1=0 l2<>0 *) +(***********************************) +Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``); [Idtac | Apply Rabsolu_pos_lt; Unfold Rsqr Rdiv; Repeat Rewrite Rinv_Rmult; Repeat Apply prod_neq_R0; Try Assumption Orelse DiscrR]. +Intros alp_f2d H11. +Assert H12 := (derivable_continuous_pt ? ? X). +Unfold continuity_pt in H12. +Unfold continue_in in H12. +Unfold limit1_in in H12. +Unfold limit_in in H12. +Unfold dist in H12. +Simpl in H12. +Unfold R_dist in H12. +Elim (H12 ``(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``). +Intros alp_f2c H13. +Cut ``0 < (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2c)))``. +Intro. +Exists (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2c))) H14). +Simpl; Intros. +Assert H17 := (Rlt_le_trans ? ? ? H16 (Rmin_l ? ?)). +Assert H18 := (Rlt_le_trans ? ? ? H16 (Rmin_r ? ?)). +Assert H19 := (Rlt_le_trans ? ? ? H18 (Rmin_r ? ?)). +Assert H20 := (Rlt_le_trans ? ? ? H19 (Rmin_l ? ?)). +Assert H21 := (Rlt_le_trans ? ? ? H19 (Rmin_r ? ?)). +Assert H22 := (Rlt_le_trans ? ? ? H18 (Rmin_l ? ?)). +Assert H23 := (Rlt_le_trans ? ? ? H17 (Rmin_l ? ?)). +Assert H24 := (Rlt_le_trans ? ? ? H17 (Rmin_r ? ?)). +Clear H16 H17 H18 H19. +Cut (a:R) ``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Intro. +Rewrite formule; Try Assumption. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term4 x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite H9. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +Apply H2; Assumption. +Intros. +Case (Req_EM a R0); Intro. +Rewrite H17; Rewrite Rplus_Or. +Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0. +Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr. +Repeat Rewrite Rinv_Rmult; Try Assumption. +Repeat Apply prod_neq_R0; Try Assumption. +Red; Intro H18; Rewrite H18 in H6; Elim (Rlt_antirefl ? H6). +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; Assumption. +Apply Rinv_neq_R0; Assumption. +DiscrR. +Apply prod_neq_R0; [DiscrR | Assumption]. +Elim H13; Intros. +Apply H19. +Split. +Apply D_x_no_cond; Assumption. +Replace ``x+a-x`` with a; [Assumption | Ring]. +Repeat Apply Rmin_pos. +Apply (cond_pos eps_f2). +Elim H3; Intros; Assumption. +Apply (cond_pos alp_f1d). +Apply (cond_pos alp_f2d). +Elim H13; Intros; Assumption. +Change ``0 < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Apply Rabsolu_pos_lt. +Unfold Rsqr Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Apply prod_neq_R0; Try Assumption. +Red; Intro H13; Rewrite H13 in H6; Elim (Rlt_antirefl ? H6). +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; Assumption. +Apply Rinv_neq_R0; Assumption. +Apply prod_neq_R0; [DiscrR | Assumption]. +Red; Intro H11; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6). +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; Assumption. +(***********************************) +(* Cas n° 5 *) +(* (f1 x)<>0 l1<>0 l2=0 *) +(***********************************) +Case (Req_EM l2 R0); Intro. +Assert H11 := (derivable_continuous_pt ? ? X). +Unfold continuity_pt in H11. +Unfold continue_in in H11. +Unfold limit1_in in H11. +Unfold limit_in in H11. +Unfold dist in H11. +Simpl in H11. +Unfold R_dist in H11. +Elim (H11 ``(Rabsolu (eps*(Rsqr (f2 x)))/(8*l1))``). +Clear H11; Intros alp_f2t2 H11. +Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``). +Intros alp_f2d H12. +Cut ``0 < (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2t2)))``. +Intro. +Exists (mkposreal (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d (Rmin alp_f2d alp_f2t2))) H13). +Simpl. +Intros. +Cut (a:R) ``(Rabsolu a)<alp_f2t2`` -> ``(Rabsolu ((f2 (x+a))-(f2 x)))<(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Intro. +Assert H17 := (Rlt_le_trans ? ? ? H15 (Rmin_l ? ?)). +Assert H18 := (Rlt_le_trans ? ? ? H15 (Rmin_r ? ?)). +Assert H19 := (Rlt_le_trans ? ? ? H17 (Rmin_r ? ?)). +Assert H20 := (Rlt_le_trans ? ? ? H17 (Rmin_l ? ?)). +Assert H21 := (Rlt_le_trans ? ? ? H18 (Rmin_r ? ?)). +Assert H22 := (Rlt_le_trans ? ? ? H18 (Rmin_l ? ?)). +Assert H23 := (Rlt_le_trans ? ? ? H21 (Rmin_l ? ?)). +Assert H24 := (Rlt_le_trans ? ? ? H21 (Rmin_r ? ?)). +Clear H15 H17 H18 H21. +Rewrite formule; Try Assumption. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite H10. +Unfold Rdiv; Repeat Rewrite Rmult_Or Orelse Rewrite Rmult_Ol. +Rewrite Rabsolu_R0; Rewrite Rmult_Ol. +Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_4_0]. +Rewrite <- Rabsolu_mult. +Apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +Apply H2; Assumption. +Intros. +Case (Req_EM a R0); Intro. +Rewrite H17; Rewrite Rplus_Or; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Rewrite Rinv_Rmult; Try DiscrR Orelse Assumption. +Unfold Rsqr. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H18; Rewrite H18 in H6; Elim (Rlt_antirefl ? H6)). +Elim H11; Intros. +Apply H19. +Split. +Apply D_x_no_cond; Assumption. +Replace ``x+a-x`` with a; [Assumption | Ring]. +Repeat Apply Rmin_pos. +Apply (cond_pos eps_f2). +Elim H3; Intros; Assumption. +Apply (cond_pos alp_f1d). +Apply (cond_pos alp_f2d). +Elim H11; Intros; Assumption. +Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult; Try DiscrR Orelse Assumption. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H12; Rewrite H12 in H6; Elim (Rlt_antirefl ? H6)). +Change ``0 < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult; Try DiscrR Orelse Assumption. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H12; Rewrite H12 in H6; Elim (Rlt_antirefl ? H6)). +(***********************************) +(* Cas n° 6 *) +(* (f1 x)<>0 l1<>0 l2<>0 *) +(***********************************) +Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``). +Intros alp_f2d H11. +Assert H12 := (derivable_continuous_pt ? ? X). +Unfold continuity_pt in H12. +Unfold continue_in in H12. +Unfold limit1_in in H12. +Unfold limit_in in H12. +Unfold dist in H12. +Simpl in H12. +Unfold R_dist in H12. +Elim (H12 ``(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``). +Intros alp_f2c H13. +Elim (H12 ``(Rabsolu (eps*(Rsqr (f2 x)))/(8*l1))``). +Intros alp_f2t2 H14. +Cut ``0 < (Rmin (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)) (Rmin alp_f2c alp_f2t2))``. +Intro. +Exists (mkposreal (Rmin (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)) (Rmin alp_f2c alp_f2t2)) H15). +Simpl. +Intros. +Assert H18 := (Rlt_le_trans ? ? ? H17 (Rmin_l ? ?)). +Assert H19 := (Rlt_le_trans ? ? ? H17 (Rmin_r ? ?)). +Assert H20 := (Rlt_le_trans ? ? ? H18 (Rmin_l ? ?)). +Assert H21 := (Rlt_le_trans ? ? ? H18 (Rmin_r ? ?)). +Assert H22 := (Rlt_le_trans ? ? ? H19 (Rmin_l ? ?)). +Assert H23 := (Rlt_le_trans ? ? ? H19 (Rmin_r ? ?)). +Assert H24 := (Rlt_le_trans ? ? ? H20 (Rmin_l ? ?)). +Assert H25 := (Rlt_le_trans ? ? ? H20 (Rmin_r ? ?)). +Assert H26 := (Rlt_le_trans ? ? ? H21 (Rmin_l ? ?)). +Assert H27 := (Rlt_le_trans ? ? ? H21 (Rmin_r ? ?)). +Clear H17 H18 H19 H20 H21. +Cut (a:R) ``(Rabsolu a) < alp_f2t2`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Cut (a:R) ``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Intros. +Rewrite formule; Try Assumption. +Apply Rle_lt_trans with ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) + (Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) + (Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) + (Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))))``. +Unfold Rminus. +Rewrite <- (Rabsolu_Ropp ``(f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))+ -(f2 x))/h+ -l2)``). +Apply Rabsolu_4. +Repeat Rewrite Rabsolu_mult. +Apply Rlt_le_trans with ``eps/4+eps/4+eps/4+eps/4``. +Cut ``(Rabsolu (/(f2 (x+h))))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < eps/4``. +Cut ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((f2 x)-(f2 (x+h)))) < eps/4``. +Cut ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < eps/4``. +Cut ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu ((f2 (x+h))-(f2 x))) < eps/4``. +Intros. +Apply Rlt_4; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term4 x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term3 x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term2 x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Rewrite <- Rabsolu_mult. +Apply (maj_term1 x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); Try Assumption. +Apply H2; Assumption. +Apply Rmin_2; Assumption. +Right; Symmetry; Apply quadruple_var. +Apply H2; Assumption. +Intros. +Case (Req_EM a R0); Intro. +Rewrite H18; Rewrite Rplus_Or; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H28; Rewrite H28 in H6; Elim (Rlt_antirefl ? H6)). +Apply prod_neq_R0; [DiscrR | Assumption]. +Apply prod_neq_R0; [DiscrR | Assumption]. +Assumption. +Elim H13; Intros. +Apply H20. +Split. +Apply D_x_no_cond; Assumption. +Replace ``x+a-x`` with a; [Assumption | Ring]. +Intros. +Case (Req_EM a R0); Intro. +Rewrite H18; Rewrite Rplus_Or; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H28; Rewrite H28 in H6; Elim (Rlt_antirefl ? H6)). +DiscrR. +Assumption. +Elim H14; Intros. +Apply H20. +Split. +Unfold D_x no_cond; Split. +Trivial. +Apply Rminus_not_eq_right. +Replace ``x+a-x`` with a; [Assumption | Ring]. +Replace ``x+a-x`` with a; [Assumption | Ring]. +Repeat Apply Rmin_pos. +Apply (cond_pos eps_f2). +Elim H3; Intros; Assumption. +Apply (cond_pos alp_f1d). +Apply (cond_pos alp_f2d). +Elim H13; Intros; Assumption. +Elim H14; Intros; Assumption. +Change ``0 < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``; Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult; Try DiscrR Orelse Assumption. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H14; Rewrite H14 in H6; Elim (Rlt_antirefl ? H6)). +Change ``0 < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``; Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H13; Rewrite H13 in H6; Elim (Rlt_antirefl ? H6)). +Apply prod_neq_R0; [DiscrR | Assumption]. +Apply prod_neq_R0; [DiscrR | Assumption]. +Assumption. +Apply Rabsolu_pos_lt. +Unfold Rdiv Rsqr; Rewrite Rinv_Rmult; [Idtac | DiscrR | Assumption]. +Repeat Apply prod_neq_R0; Assumption Orelse (Apply Rinv_neq_R0; Assumption) Orelse (Apply Rinv_neq_R0; DiscrR) Orelse (Red; Intro H11; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6)). +Intros. +Unfold Rdiv. +Apply Rlt_monotony_contra with ``(Rabsolu (f2 (x+a)))``. +Apply Rabsolu_pos_lt; Apply H2. +Apply Rlt_le_trans with (Rmin eps_f2 alp_f2). +Assumption. +Apply Rmin_l. +Rewrite <- Rinv_r_sym. +Apply Rlt_monotony_contra with (Rabsolu (f2 x)). +Apply Rabsolu_pos_lt; Assumption. +Rewrite Rmult_1r. +Rewrite (Rmult_sym (Rabsolu (f2 x))). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Apply Rlt_monotony_contra with ``/2``. +Apply Rlt_Rinv; Apply Rgt_2_0. +Repeat Rewrite (Rmult_sym ``/2``). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r. +Unfold Rdiv in H5; Apply H5. +Replace ``x+a-x`` with a. +Assert H7 := (Rlt_le_trans ? ? ? H6 (Rmin_r ? ?)); Assumption. +Ring. +DiscrR. +Apply Rabsolu_no_R0; Assumption. +Apply Rabsolu_no_R0; Apply H2. +Assert H7 := (Rlt_le_trans ? ? ? H6 (Rmin_l ? ?)); Assumption. +Intros. +Assert H6 := (H4 a H5). +Rewrite <- (Rabsolu_Ropp ``(f2 a)-(f2 x)``) in H6. +Rewrite Ropp_distr2 in H6. +Assert H7 := (Rle_lt_trans ? ? ? (Rabsolu_triang_inv ? ?) H6). +Apply Rlt_anti_compatibility with ``-(Rabsolu (f2 a)) + (Rabsolu (f2 x))/2``. +Rewrite Rplus_assoc. +Rewrite <- double_var. +Do 2 Rewrite (Rplus_sym ``-(Rabsolu (f2 a))``). +Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or. +Unfold Rminus in H7; Assumption. +Intros. +Case (Req_EM x x0); Intro. +Rewrite <- H5; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Elim H3; Intros. +Apply H7. +Split. +Unfold D_x no_cond; Split. +Trivial. +Assumption. +Assumption. +Qed. + +Lemma derivable_pt_div : (f1,f2:R->R;x:R) (derivable_pt f1 x) -> (derivable_pt f2 x) -> ``(f2 x)<>0`` -> (derivable_pt (div_fct f1 f2) x). +Unfold derivable_pt. +Intros. +Elim X; Intros. +Elim X0; Intros. +Apply Specif.existT with ``(x0*(f2 x)-x1*(f1 x))/(Rsqr (f2 x))``. +Apply derivable_pt_lim_div; Assumption. +Qed. + +Lemma derivable_div : (f1,f2:R->R) (derivable f1) -> (derivable f2) -> ((x:R)``(f2 x)<>0``) -> (derivable (div_fct f1 f2)). +Unfold derivable; Intros. +Apply (derivable_pt_div ? ? ? (X x) (X0 x) (H x)). +Qed. + +Lemma derive_pt_div : (f1,f2:R->R;x:R;pr1:(derivable_pt f1 x);pr2:(derivable_pt f2 x);na:``(f2 x)<>0``) ``(derive_pt (div_fct f1 f2) x (derivable_pt_div ? ? ? pr1 pr2 na)) == ((derive_pt f1 x pr1)*(f2 x)-(derive_pt f2 x pr2)*(f1 x))/(Rsqr (f2 x))``. +Intros. +Assert H := (derivable_derive f1 x pr1). +Assert H0 := (derivable_derive f2 x pr2). +Assert H1 := (derivable_derive (div_fct f1 f2) x (derivable_pt_div ? ? ? pr1 pr2 na)). +Elim H; Clear H; Intros l1 H. +Elim H0; Clear H0; Intros l2 H0. +Elim H1; Clear H1; Intros l H1. +Rewrite H; Rewrite H0; Apply derive_pt_eq_0. +Assert H3 := (projT2 ? ? pr1). +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. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v new file mode 100644 index 0000000000..9bbcabc2ca --- /dev/null +++ b/theories/Reals/Ranalysis4.v @@ -0,0 +1,459 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require Rbase. +Require Rbasic_fun. +Require R_sqr. +Require Rlimit. +Require Rderiv. +Require DiscrR. +Require Rtrigo. +Require Ranalysis1. +Require Ranalysis2. +Require Ranalysis3. + +(**********) +Lemma derivable_pt_inv : (f:R->R;x:R) ``(f x)<>0`` -> (derivable_pt f x) -> (derivable_pt (inv_fct f) x). +Intros; Cut (derivable_pt (div_fct (fct_cte R1) f) x) -> (derivable_pt (inv_fct f) x). +Intro; Apply X0. +Apply derivable_pt_div. +Apply derivable_pt_const. +Assumption. +Assumption. +Unfold div_fct inv_fct fct_cte; Intro. +Replace [x:R]``/(f x)`` with [x:R]``1/(f x)``; [Assumption | Apply fct_eq; Intro; Unfold Rdiv; Rewrite Rmult_1l; Reflexivity]. +Qed. + +(**********) +Lemma pr_nu_var : (f,g:R->R;x:R;pr1:(derivable_pt f x);pr2:(derivable_pt g x)) f==g -> (derive_pt f x pr1) == (derive_pt g x pr2). +Unfold derivable_pt derive_pt; Intros. +Elim pr1; Intros. +Elim pr2; Intros. +Simpl. +Rewrite H in p. +Apply unicite_limite with g x; Assumption. +Qed. + +(**********) +Lemma derivable_inv : (f:R->R) ((x:R)``(f x)<>0``)->(derivable f)->(derivable (inv_fct f)). +Intros. +Unfold derivable; Intro. +Apply derivable_pt_inv. +Apply (H x). +Apply (X x). +Qed. + +Lemma derive_pt_inv : (f:R->R;x:R;pr:(derivable_pt f x);na:``(f x)<>0``) (derive_pt (inv_fct f) x (derivable_pt_inv f x na pr)) == ``-(derive_pt f x pr)/(Rsqr (f x))``. +Intros; Replace (derive_pt (inv_fct f) x (derivable_pt_inv f x na pr)) with (derive_pt (div_fct (fct_cte R1) f) x (derivable_pt_div (fct_cte R1) f x (derivable_pt_const R1 x) pr na)). +Rewrite derive_pt_div; Rewrite derive_pt_const; Unfold fct_cte; Rewrite Rmult_Ol; Rewrite Rmult_1r; Unfold Rminus; Rewrite Rplus_Ol; Reflexivity. +Apply pr_nu_var. +Unfold div_fct fct_cte inv_fct; Apply fct_eq. +Intro; Unfold Rdiv; Rewrite Rmult_1l; Reflexivity. +Qed. + +(**********) +Tactic Definition IntroHypG trm := +Match trm With +|[(plus_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2 + |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2 + | _ -> Idtac) +|[(minus_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2 + |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2 + | _ -> Idtac) +|[(mult_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2 + |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2 + | _ -> Idtac) +|[(div_fct ?1 ?2)] -> Let aux = ?2 In + (Match Context With + |[_:(x0:R)``(aux x0)<>0``|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2 + |[_:(x0:R)``(aux x0)<>0``|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2 + |[|-(derivable ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1; IntroHypG ?2 | Try Assumption] + |[|-(continuity ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1; IntroHypG ?2 | Try Assumption] + | _ -> Idtac) +|[(comp ?1 ?2)] -> + (Match Context With + |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2 + |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2 + | _ -> Idtac) +|[(opp_fct ?1)] -> + (Match Context With + |[|-(derivable ?)] -> IntroHypG ?1 + |[|-(continuity ?)] -> IntroHypG ?1 + | _ -> Idtac) +|[(inv_fct ?1)] -> Let aux = ?1 In + (Match Context With + |[_:(x0:R)``(aux x0)<>0``|-(derivable ?)] -> IntroHypG ?1 + |[_:(x0:R)``(aux x0)<>0``|-(continuity ?)] -> IntroHypG ?1 + |[|-(derivable ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1 | Try Assumption] + |[|-(continuity ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1| Try Assumption] + | _ -> Idtac) +|[cos] -> Idtac +|[sin] -> Idtac +|[Rsqr] -> Idtac +|[id] -> Idtac +|[(fct_cte ?)] -> Idtac +|[?1] -> Let p = ?1 In + (Match Context With + |[_:(derivable p)|- ?] -> Idtac + |[|-(derivable p)] -> Idtac + |[|-(derivable ?)] -> Cut True -> (derivable p); [Intro HYPPD; Cut (derivable p); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac] + | [_:(continuity p)|- ?] -> Idtac + |[|-(continuity p)] -> Idtac + |[|-(continuity ?)] -> Cut True -> (continuity p); [Intro HYPPD; Cut (continuity p); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac] + | _ -> Idtac). + +(**********) +Tactic Definition IntroHypL trm pt := +Match trm With +|[(plus_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + | _ -> Idtac) +|[(minus_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + | _ -> Idtac) +|[(mult_fct ?1 ?2)] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + | _ -> Idtac) +|[(div_fct ?1 ?2)] -> Let aux = ?2 In + (Match Context With + |[_:``(aux pt)<>0``|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[_:``(aux pt)<>0``|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[_:``(aux pt)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt + |[id:(x0:R)``(aux x0)<>0``|-(derivable_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt + |[id:(x0:R)``(aux x0)<>0``|-(continuity_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt + |[id:(x0:R)``(aux x0)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt + |[|-(derivable_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption] + |[|-(continuity_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption] + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption] + | _ -> Idtac) +|[(comp ?1 ?2)] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt + |[|-(continuity_pt ? ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt + | _ -> Idtac) +|[(opp_fct ?1)] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt + |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt + | _ -> Idtac) +|[(inv_fct ?1)] -> Let aux = ?1 In + (Match Context With + |[_:``(aux pt)<>0``|-(derivable_pt ? ?)] -> IntroHypL ?1 pt + |[_:``(aux pt)<>0``|-(continuity_pt ? ?)] -> IntroHypL ?1 pt + |[_:``(aux pt)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt + |[id:(x0:R)``(aux x0)<>0``|-(derivable_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt + |[id:(x0:R)``(aux x0)<>0``|-(continuity_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt + |[id:(x0:R)``(aux x0)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt + |[|-(derivable_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt | Try Assumption] + |[|-(continuity_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt| Try Assumption] + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt | Try Assumption] + | _ -> Idtac) +|[cos] -> Idtac +|[sin] -> Idtac +|[Rsqr] -> Idtac +|[id] -> Idtac +|[(fct_cte ?)] -> Idtac +|[sqrt] -> + (Match Context With + |[|-(derivable_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption] + |[|-(continuity_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption] + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``0<pt``; [Intro | Try Assumption] + | _ -> Idtac) +|[?1] -> Let p = ?1 In + (Match Context With + |[_:(derivable_pt p pt)|- ?] -> Idtac + |[|-(derivable_pt p pt)] -> Idtac + |[|-(derivable_pt ? ?)] -> Cut True -> (derivable_pt p pt); [Intro HYPPD; Cut (derivable_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac] + |[_:(continuity_pt p pt)|- ?] -> Idtac + |[|-(continuity_pt p pt)] -> Idtac + |[|-(continuity_pt ? ?)] -> Cut True -> (continuity_pt p pt); [Intro HYPPD; Cut (continuity_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac] + |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut True -> (derivable_pt p pt); [Intro HYPPD; Cut (derivable_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac] + | _ -> Idtac). + +(**********) +Recursive Tactic Definition IsDiff_glob := +Match Context With + (* fonctions de base *) + [|-(derivable Rsqr)] -> Apply derivable_Rsqr + |[|-(derivable id)] -> Apply derivable_id + |[|-(derivable (fct_cte ?))] -> Apply derivable_const + |[|-(derivable sin)] -> Apply derivable_sin + |[|-(derivable cos)] -> Apply derivable_cos + (* regles de differentiabilite *) + (* PLUS *) + |[|-(derivable (plus_fct ?1 ?2))] -> Apply (derivable_plus ?1 ?2); IsDiff_glob + (* MOINS *) + |[|-(derivable (minus_fct ?1 ?2))] -> Apply (derivable_minus ?1 ?2); IsDiff_glob + (* OPPOSE *) + |[|-(derivable (opp_fct ?1))] -> Apply (derivable_opp ?1); IsDiff_glob + (* MULTIPLICATION PAR UN SCALAIRE *) + |[|-(derivable (mult_real_fct ?1 ?2))] -> Apply (derivable_scal ?2 ?1); IsDiff_glob + (* MULTIPLICATION *) + |[|-(derivable (mult_fct ?1 ?2))] -> Apply (derivable_mult ?1 ?2); IsDiff_glob + (* DIVISION *) + |[|-(derivable (div_fct ?1 ?2))] -> Apply (derivable_div ?1 ?2); [IsDiff_glob | IsDiff_glob | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp] + (* INVERSION *) + |[|-(derivable (inv_fct ?1))] -> Apply (derivable_inv ?1); [Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp | IsDiff_glob] + (* COMPOSITION *) + |[|-(derivable (comp ?1 ?2))] -> Apply (derivable_comp ?2 ?1); IsDiff_glob + |[_:(derivable ?1)|-(derivable ?1)] -> Assumption + |[|-True->(derivable ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_glob + | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp. + +(**********) +Recursive Tactic Definition IsDiff_pt := +Match Context With + (* fonctions de base *) + [|-(derivable_pt Rsqr ?)] -> Apply derivable_pt_Rsqr +|[|-(derivable_pt id ?1)] -> Apply (derivable_pt_id ?1) +|[|-(derivable_pt (fct_cte ?) ?)] -> Apply derivable_pt_const +|[|-(derivable_pt sin ?)] -> Apply derivable_pt_sin +|[|-(derivable_pt cos ?)] -> Apply derivable_pt_cos +|[|-(derivable_pt sqrt ?1)] -> Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte + (* regles de differentiabilite *) + (* PLUS *) +|[|-(derivable_pt (plus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_plus ?1 ?2 ?3); IsDiff_pt + (* MOINS *) +|[|-(derivable_pt (minus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_minus ?1 ?2 ?3); IsDiff_pt + (* OPPOSE *) +|[|-(derivable_pt (opp_fct ?1) ?2)] -> Apply (derivable_pt_opp ?1 ?2); IsDiff_pt + (* MULTIPLICATION PAR UN SCALAIRE *) +|[|-(derivable_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (derivable_pt_scal ?2 ?1 ?3); IsDiff_pt + (* MULTIPLICATION *) +|[|-(derivable_pt (mult_fct ?1 ?2) ?3)] -> Apply (derivable_pt_mult ?1 ?2 ?3); IsDiff_pt + (* DIVISION *) + |[|-(derivable_pt (div_fct ?1 ?2) ?3)] -> Apply (derivable_pt_div ?1 ?2 ?3); [IsDiff_pt | IsDiff_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte] + (* INVERSION *) + |[|-(derivable_pt (inv_fct ?1) ?2)] -> Apply (derivable_pt_inv ?1 ?2); [Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte | IsDiff_pt] + (* COMPOSITION *) +|[|-(derivable_pt (comp ?1 ?2) ?3)] -> Apply (derivable_pt_comp ?2 ?1 ?3); IsDiff_pt +|[_:(derivable_pt ?1 ?2)|-(derivable_pt ?1 ?2)] -> Assumption +|[_:(derivable ?1) |- (derivable_pt ?1 ?2)] -> Cut (derivable ?1); [Intro HypDDPT; Apply HypDDPT | Assumption] +|[|-True->(derivable_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_pt +| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp. + +(**********) +Recursive Tactic Definition IsCont_glob := +Match Context With + (* fonctions de base *) + [|-(continuity Rsqr)] -> Apply derivable_continuous; Apply derivable_Rsqr + |[|-(continuity id)] -> Apply derivable_continuous; Apply derivable_id + |[|-(continuity (fct_cte ?))] -> Apply derivable_continuous; Apply derivable_const + |[|-(continuity sin)] -> Apply derivable_continuous; Apply derivable_sin + |[|-(continuity cos)] -> Apply derivable_continuous; Apply derivable_cos + (* regles de continuite *) + (* PLUS *) +|[|-(continuity (plus_fct ?1 ?2))] -> Apply (continuity_plus ?1 ?2); Try IsCont_glob Orelse Assumption + (* MOINS *) +|[|-(continuity (minus_fct ?1 ?2))] -> Apply (continuity_minus ?1 ?2); Try IsCont_glob Orelse Assumption + (* OPPOSE *) +|[|-(continuity (opp_fct ?1))] -> Apply (continuity_opp ?1); Try IsCont_glob Orelse Assumption + (* INVERSE *) +|[|-(continuity (inv_fct ?1))] -> Apply (continuity_inv ?1); Try IsCont_glob Orelse Assumption + (* MULTIPLICATION PAR UN SCALAIRE *) +|[|-(continuity (mult_real_fct ?1 ?2))] -> Apply (contintuity_scal ?2 ?1); Try IsCont_glob Orelse Assumption + (* MULTIPLICATION *) +|[|-(continuity (mult_fct ?1 ?2))] -> Apply (continuity_mult ?1 ?2); Try IsCont_glob Orelse Assumption + (* DIVISION *) + |[|-(continuity (div_fct ?1 ?2))] -> Apply (continuity_div ?1 ?2); [Try IsCont_glob Orelse Assumption | Try IsCont_glob Orelse Assumption | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte] + (* COMPOSITION *) + |[|-(continuity (comp ?1 ?2))] -> Apply (continuity_comp ?2 ?1); Try IsCont_glob Orelse Assumption + |[_:(continuity ?1)|-(continuity ?1)] -> Assumption + |[|-True->(continuity ?)] -> Intro HypTruE; Clear HypTruE; IsCont_glob + |[_:(derivable ?1)|-(continuity ?1)] -> Apply derivable_continuous; Assumption + | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp. + +(**********) +Recursive Tactic Definition IsCont_pt := +Match Context With + (* fonctions de base *) + [|-(continuity_pt Rsqr ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_Rsqr +|[|-(continuity_pt id ?1)] -> Apply derivable_continuous_pt; Apply (derivable_pt_id ?1) +|[|-(continuity_pt (fct_cte ?) ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_const +|[|-(continuity_pt sin ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_sin +|[|-(continuity_pt cos ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_cos +|[|-(derivable_pt sqrt ?1)] -> Apply derivable_continuous_pt; Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte + (* regles de differentiabilite *) + (* PLUS *) +|[|-(continuity_pt (plus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_plus ?1 ?2 ?3); IsCont_pt + (* MOINS *) +|[|-(continuity_pt (minus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_minus ?1 ?2 ?3); IsCont_pt + (* OPPOSE *) +|[|-(continuity_pt (opp_fct ?1) ?2)] -> Apply (continuity_pt_opp ?1 ?2); IsCont_pt + (* MULTIPLICATION PAR UN SCALAIRE *) +|[|-(continuity_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (continuity_pt_scal ?2 ?1 ?3); IsCont_pt + (* MULTIPLICATION *) +|[|-(continuity_pt (mult_fct ?1 ?2) ?3)] -> Apply (continuity_pt_mult ?1 ?2 ?3); IsCont_pt + (* DIVISION *) + |[|-(continuity_pt (div_fct ?1 ?2) ?3)] -> Apply (continuity_pt_div ?1 ?2 ?3); [IsCont_pt | IsCont_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte] + (* INVERSION *) + |[|-(continuity_pt (inv_fct ?1) ?2)] -> Apply (continuity_pt_inv ?1 ?2); [IsCont_pt | Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte] + (* COMPOSITION *) +|[|-(continuity_pt (comp ?1 ?2) ?3)] -> Apply (continuity_pt_comp ?2 ?1 ?3); IsCont_pt +|[_:(continuity_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Assumption +|[_:(continuity ?1) |- (continuity_pt ?1 ?2)] -> Cut (continuity ?1); [Intro HypDDPT; Apply HypDDPT | Assumption] +|[_:(derivable_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Apply derivable_continuous_pt; Assumption +|[_:(derivable ?1)|-(continuity_pt ?1 ?2)] -> Cut (continuity ?1); [Intro HypDDPT; Apply HypDDPT | Apply derivable_continuous; Assumption] +|[|-True->(continuity_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsCont_pt +| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp. + +(**********) +Recursive Tactic Definition RewTerm trm := +Match trm With +| [(Rplus ?1 ?2)] -> Let p1= (RewTerm ?1) And p2 = (RewTerm ?2) In + (Match p1 With + [(fct_cte ?3)] -> + (Match p2 With + | [(fct_cte ?4)] -> '(fct_cte (Rplus ?3 ?4)) + | _ -> '(plus_fct p1 p2)) + | _ -> '(plus_fct p1 p2)) +| [(Rminus ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In + (Match p1 With + [(fct_cte ?3)] -> + (Match p2 With + | [(fct_cte ?4)] -> '(fct_cte (Rminus ?3 ?4)) + | _ -> '(minus_fct p1 p2)) + | _ -> '(minus_fct p1 p2)) +| [(Rdiv ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In + (Match p1 With + [(fct_cte ?3)] -> + (Match p2 With + | [(fct_cte ?4)] -> '(fct_cte (Rdiv ?3 ?4)) + | _ -> '(div_fct p1 p2)) + | _ -> + (Match p2 With + | [(fct_cte ?4)] -> '(mult_fct p1 (fct_cte (Rinv ?4))) + | _ -> '(div_fct p1 p2))) +| [(Rmult ?1 (Rinv ?2))] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In + (Match p1 With + [(fct_cte ?3)] -> + (Match p2 With + | [(fct_cte ?4)] -> '(fct_cte (Rdiv ?3 ?4)) + | _ -> '(div_fct p1 p2)) + | _ -> + (Match p2 With + | [(fct_cte ?4)] -> '(mult_fct p1 (fct_cte (Rinv ?4))) + | _ -> '(div_fct p1 p2))) +| [(Rmult ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In + (Match p1 With + [(fct_cte ?3)] -> + (Match p2 With + | [(fct_cte ?4)] -> '(fct_cte (Rmult ?3 ?4)) + | _ -> '(mult_fct p1 p2)) + | _ -> '(mult_fct p1 p2)) +| [(Ropp ?1)] -> Let p = (RewTerm ?1) In + (Match p With + [(fct_cte ?2)] -> '(fct_cte (Ropp ?2)) + | _ -> '(opp_fct p)) +| [(Rinv ?1)] -> Let p = (RewTerm ?1) In + (Match p With + [(fct_cte ?2)] -> '(fct_cte (Rinv ?2)) + | _ -> '(inv_fct p)) +| [(?1 PI)] -> '?1 +| [(?1 ?2)] -> Let p = (RewTerm ?2) In + (Match p With + | [(fct_cte ?3)] -> '(fct_cte (?1 ?3)) + | _ -> '(comp ?1 p)) +| [PI] -> 'id +| [?1]-> '(fct_cte ?1). + +(**********) +Recursive Tactic Definition ConsProof trm pt := +Match trm With +| [(plus_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_plus ?1 ?2 pt p1 p2) +| [(minus_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_minus ?1 ?2 pt p1 p2) +| [(mult_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_mult ?1 ?2 pt p1 p2) +| [(div_fct ?1 ?2)] -> + (Match Context With + |[id:~((?2 pt)==R0) |- ?] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_div ?1 ?2 pt p1 p2 id) + | _ -> 'False) +| [(inv_fct ?1)] -> + (Match Context With + |[id:~((?1 pt)==R0) |- ?] -> Let p1 = (ConsProof ?1 pt) In '(derivable_pt_inv ?1 pt p1 id) + | _ -> 'False) +| [(comp ?1 ?2)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In Let p1 = (ConsProof ?1 pt_f1) And p2 = (ConsProof ?2 pt) In '(derivable_pt_comp ?2 ?1 pt p2 p1) +| [(opp_fct ?1)] -> Let p1 = (ConsProof ?1 pt) In '(derivable_pt_opp ?1 pt p1) +| [sin] -> '(derivable_pt_sin pt) +| [cos] -> '(derivable_pt_cos pt) +| [id] -> '(derivable_pt_id pt) +| [Rsqr] -> '(derivable_pt_Rsqr pt) +| [sqrt] -> + (Match Context With + |[id:(Rlt R0 pt) |- ?] -> '(derivable_pt_sqrt pt id) + | _ -> 'False) +| [(fct_cte ?1)] -> '(derivable_pt_const ?1 pt) +| [?1] -> Let aux = ?1 In + (Match Context With + [ id : (derivable_pt aux pt) |- ?] -> 'id + |[ id : (derivable aux) |- ?] -> '(id pt) + | _ -> 'False). + +(**********) +Recursive Tactic Definition SimplifyDerive trm pt := +Match trm With +| [(plus_fct ?1 ?2)] -> Try Rewrite derive_pt_plus; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt +| [(minus_fct ?1 ?2)] -> Try Rewrite derive_pt_minus; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt +| [(mult_fct ?1 ?2)] -> Try Rewrite derive_pt_mult; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt +| [(div_fct ?1 ?2)] -> Try Rewrite derive_pt_div; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt +| [(comp ?1 ?2)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In Try Rewrite derive_pt_comp; SimplifyDerive ?1 pt_f1; SimplifyDerive ?2 pt +| [(opp_fct ?1)] -> Try Rewrite derive_pt_opp; SimplifyDerive ?1 pt +| [(inv_fct ?1)] -> Try Rewrite derive_pt_inv; SimplifyDerive ?1 pt +| [(fct_cte ?1)] -> Try Rewrite derive_pt_const +| [id] -> Try Rewrite derive_pt_id +| [sin] -> Try Rewrite derive_pt_sin +| [cos] -> Try Rewrite derive_pt_cos +| [Rsqr] -> Try Rewrite derive_pt_Rsqr +| [sqrt] -> Try Rewrite derive_pt_sqrt +| [?1] -> Let aux = ?1 In + (Match Context With + [ id : (eqT ? (derive_pt aux pt ?2) ?); H : (derivable aux) |- ? ] -> Try Replace (derive_pt aux pt (H pt)) with (derive_pt aux pt ?2); [Rewrite id | Apply pr_nu] + |[ id : (eqT ? (derive_pt aux pt ?2) ?); H : (derivable_pt aux pt) |- ? ] -> Try Replace (derive_pt aux pt H) with (derive_pt aux pt ?2); [Rewrite id | Apply pr_nu] + | _ -> Idtac ) +| _ -> Idtac. + +(**********) +Tactic Definition Regularity () := +Match Context With +| [|-(derivable_pt ?1 ?2)] -> +Let trm = Eval Cbv Beta in (?1 PI) In +Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (derivable_pt aux ?2); IsDiff_pt) Orelse IsDiff_pt +| [|-(derivable ?1)] -> +Let trm = Eval Cbv Beta in (?1 PI) In +Let aux = (RewTerm trm) In IntroHypG aux; Try (Change (derivable aux); IsDiff_glob) Orelse IsDiff_glob +| [|-(continuity ?1)] -> +Let trm = Eval Cbv Beta in (?1 PI) In +Let aux = (RewTerm trm) In IntroHypG aux; Try (Change (continuity aux); IsCont_glob) Orelse IsCont_glob +| [|-(continuity_pt ?1 ?2)] -> +Let trm = Eval Cbv Beta in (?1 PI) In +Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (continuity_pt aux ?2); IsCont_pt) Orelse IsCont_pt +| [|-(eqT ? (derive_pt ?1 ?2 ?3) ?4)] -> +Let trm = Eval Cbv Beta in (?1 PI) In +Let aux = (RewTerm trm) In +IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt. + +(**********) +Tactic Definition Reg () := Regularity (). |