diff options
Diffstat (limited to 'theories7/Reals/Ranalysis1.v')
| -rw-r--r-- | theories7/Reals/Ranalysis1.v | 1046 |
1 files changed, 1046 insertions, 0 deletions
diff --git a/theories7/Reals/Ranalysis1.v b/theories7/Reals/Ranalysis1.v new file mode 100644 index 00000000..8cb4c358 --- /dev/null +++ b/theories7/Reals/Ranalysis1.v @@ -0,0 +1,1046 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Ranalysis1.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +Require Export Rlimit. +Require Export Rderiv. +V7only [Import R_scope.]. Open Local Scope R_scope. +Implicit Variable Type f:R->R. + +(****************************************************) +(** 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)``. + +V8Infix "+" plus_fct : Rfun_scope. +V8Notation "- x" := (opp_fct x) : Rfun_scope. +V8Infix "*" mult_fct : Rfun_scope. +V8Infix "-" minus_fct : Rfun_scope. +V8Infix "/" div_fct : Rfun_scope. +Notation Local "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity) + : Rfun_scope + V8only (at level 20, right associativity). +V8Notation "/ x" := (inv_fct x) : Rfun_scope. + +Delimits Scope Rfun_scope with F. + +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)``. + +(**********) +Definition no_cond : R->Prop := [x:R] True. + +(**********) +Definition constant_D_eq [f:R->R;D:R->Prop;c:R] : Prop := (x:R) (D x) -> (f x)==c. + +(***************************************************) +(** 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). + +Arguments Scope continuity_pt [Rfun_scope R_scope]. +Arguments Scope continuity [Rfun_scope]. + +(**********) +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 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)). + +Arguments Scope derivable_pt_lim [Rfun_scope R_scope]. +Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope]. +Arguments Scope derivable_pt [Rfun_scope R_scope]. +Arguments Scope derivable [Rfun_scope]. +Arguments Scope derive_pt [Rfun_scope R_scope _]. +Arguments Scope derive [Rfun_scope _]. + +Definition antiderivative [f,g:R->R;a,b:R] : Prop := ((x:R)``a<=x<=b``->(EXT pr : (derivable_pt g x) | (f x)==(derive_pt g x pr)))/\``a<=b``. +(************************************) +(** 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``. +Sup0. +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; Sup0. +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. +Cut (h:R)``((f1 (x+h))+(f2 (x+h))-((f1 x)+(f2 x)))/h``==``((f1 (x+h))-(f1 x))/h+((f2 (x+h))-(f2 x))/h``. +Intro. +Generalize(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). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H4 eps H5); Intros. +Exists x0. +Elim H6; Intros. +Split. +Assumption. +Intros; Rewrite H3; Apply H8; Assumption. +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. +Cut (h:R) ``( -(f (x+h))- -(f x))/h``==(Ropp ``((f (x+h))-(f x))/h``). +Intro. +Generalize (limit_Ropp [h:R]``((f (x+h))-(f x))/h``[h:R]``h <> 0`` l ``0`` H1). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H2 eps H3); Intros. +Exists x0. +Elim H4; Intros. +Split. +Assumption. +Intros; Rewrite H0; Apply H6; Assumption. +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. +Cut (h:R)``((f1 (x+h))-(f1 x))/h-((f2 (x+h))-(f2 x))/h``==``((f1 (x+h))-(f2 (x+h))-((f1 x)-(f2 x)))/h``. +Intro. +Generalize (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). +Unfold limit1_in; Unfold limit_in; Unfold dist; Simpl; Unfold R_dist; Intros. +Elim (H4 eps H5); Intros. +Exists x0. +Elim H6; Intros. +Split. +Assumption. +Intros; Rewrite <- H3; Apply H8; Assumption. +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. + +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_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 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. + +(* Pow *) +Definition pow_fct [n:nat] : R->R := [y:R](pow y n). + +Lemma derivable_pt_lim_pow_pos : (x:R;n:nat) (lt O n) -> (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``). +Intros. +Induction n. +Elim (lt_n_n ? H). +Cut n=O\/(lt O n). +Intro; Elim H0; Intro. +Rewrite H1; Simpl. +Replace [y:R]``y*1`` with (mult_fct id (fct_cte R1)). +Replace ``1*1`` with ``1*(fct_cte R1 x)+(id x)*0``. +Apply derivable_pt_lim_mult. +Apply derivable_pt_lim_id. +Apply derivable_pt_lim_const. +Unfold fct_cte id; Ring. +Reflexivity. +Replace [y:R](pow y (S n)) with [y:R]``y*(pow y n)``. +Replace (pred (S n)) with n; [Idtac | Reflexivity]. +Replace [y:R]``y*(pow y n)`` with (mult_fct id [y:R](pow y n)). +Pose f := [y:R](pow y n). +Replace ``(INR (S n))*(pow x n)`` with (Rplus (Rmult R1 (f x)) (Rmult (id x) (Rmult (INR n) (pow x (pred n))))). +Apply derivable_pt_lim_mult. +Apply derivable_pt_lim_id. +Unfold f; Apply Hrecn; Assumption. +Unfold f. +Pattern 1 5 n; Replace n with (S (pred n)). +Unfold id; Rewrite S_INR; Simpl. +Ring. +Symmetry; Apply S_pred with O; Assumption. +Unfold mult_fct id; Reflexivity. +Reflexivity. +Inversion H. +Left; Reflexivity. +Right. +Apply lt_le_trans with (1). +Apply lt_O_Sn. +Assumption. +Qed. + +Lemma derivable_pt_lim_pow : (x:R; n:nat) (derivable_pt_lim [y:R](pow y n) x ``(INR n)*(pow x (pred n))``). +Intros. +Induction n. +Simpl. +Rewrite Rmult_Ol. +Replace [_:R]``1`` with (fct_cte R1); [Apply derivable_pt_lim_const | Reflexivity]. +Apply derivable_pt_lim_pow_pos. +Apply lt_O_Sn. +Qed. + +Lemma derivable_pt_pow : (n:nat;x:R) (derivable_pt [y:R](pow y n) x). +Intros; Unfold derivable_pt. +Apply Specif.existT with ``(INR n)*(pow x (pred n))``. +Apply derivable_pt_lim_pow. +Qed. + +Lemma derivable_pow : (n:nat) (derivable [y:R](pow y n)). +Intro; Unfold derivable; Intro; Apply derivable_pt_pow. +Qed. + +Lemma derive_pt_pow : (n:nat;x:R) (derive_pt [y:R](pow y n) x (derivable_pt_pow n x))==``(INR n)*(pow x (pred n))``. +Intros; Apply derive_pt_eq_0. +Apply derivable_pt_lim_pow. +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; Sup0]]. +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``. +Sup0. +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. +DiscrR. +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; Sup0]. +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; Sup0]. +Intro; Apply Rle_lt_trans with ``delta/2``. +Apply Rmin_l. +Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. +Sup0. +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. +DiscrR. +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; Sup0]. +Unfold Rdiv; Apply Rmult_lt_pos. +Generalize (Rlt_compatibility_r ``-c`` c b H0); Rewrite Rplus_Ropp_r; Intro; Assumption. +Apply Rlt_Rinv; Sup0. +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``. +Sup0. +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``. +Sup0. +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). +DiscrR. +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) | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]]. +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) | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]]. +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 | Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]]. +Replace ``-(l/2)`` with ``(-l)/2``. +Unfold Rdiv; Apply Rmult_lt_pos. +Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. +Assert Hyp : ``0<2``; [Sup0 | Apply (Rlt_Rinv ``2`` Hyp)]. +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; Sup0]. +Replace ``(Rabsolu delta/2)`` with ``delta/2``. +Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. +Sup0. +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; Sup0]. +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; Sup0. +Qed. |