diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-31 14:34:11 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-31 14:34:11 +0000 |
commit | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (patch) | |
tree | d9a5b0cd2730f4a31755ed2cdc0a3e571caab88a /theories/Reals/Ranalysis1.v | |
parent | 48d01894776c4381d50c33f42d9c3ad50ef106fd (diff) |
MAJ pour TAF
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Ranalysis1.v')
-rw-r--r-- | theories/Reals/Ranalysis1.v | 298 |
1 files changed, 1 insertions, 297 deletions
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 13b9c5b5e..71c0da760 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -1019,300 +1019,4 @@ 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 TAF : (f:R->R;a,b:R;pr:(derivable f)) ``a<b`` -> (EXT c : R | ``((f b)-(f a))==(derive_pt f c (pr c))*(b-a)``/\``a<c<b``). - -(**********) -Lemma nonneg_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``0<=(derive_pt f x (pr x))``) -> (increasing f). -Intros. -Unfold increasing. -Intros. -Case (total_order_T x y); Intro. -Elim s; Intro. -Apply Rle_anti_compatibility with ``-(f x)``. -Rewrite Rplus_Ropp_l; Rewrite Rplus_sym. -Assert H1 := (TAF f ? ? pr a). -Elim H1; Intros. -Elim H2; Intros. -Unfold Rminus in H3. -Rewrite H3. -Apply Rmult_le_pos. -Apply H. -Apply Rle_anti_compatibility with x. -Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring]. -Rewrite b; Right; Reflexivity. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H0 r)). -Qed. - -(**********) -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 nonpos_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``(derive_pt f x (pr x))<=0``) -> (decreasing f). -Intros. -Cut (h:R)``-(-(f h))==(f h)``. -Intro. -Generalize (increasing_decreasing_opp (opp_fct f)). -Unfold decreasing. -Unfold opp_fct. -Intros. -Rewrite <- (H0 x); Rewrite <- (H0 y). -Apply H1. -Cut (x:R)``0<=(derive_pt (opp_fct f) x ((derivable_opp f pr) x))``. -Intros. -Replace [x:R]``-(f x)`` with (opp_fct f); [Idtac | Reflexivity]. -Apply (nonneg_derivative_1 (opp_fct f) (derivable_opp f pr) H3). -Intro. -Assert H3 := (derive_pt_opp f x0 (pr x0)). -Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``. -Intro. -Rewrite <- H4. -Rewrite H3. -Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Apply (H x0). -Apply pr_nu. -Assumption. -Intro; Ring. -Qed. - -(**********) -Lemma positive_derivative : (f:R->R;pr:(derivable f)) ((x:R) ``0<(derive_pt f x (pr x))``)->(strict_increasing f). -Intros. -Unfold strict_increasing. -Intros. -Apply Rlt_anti_compatibility with ``-(f x)``. -Rewrite Rplus_Ropp_l; Rewrite Rplus_sym. -Assert H1 := (TAF f ? ? pr H0). -Elim H1; Intros. -Elim H2; Intros. -Unfold Rminus in H3. -Rewrite H3. -Apply Rmult_lt_pos. -Apply H. -Apply Rlt_anti_compatibility with x. -Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring]. -Qed. - -(**********) -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. -Cut (h:R)``- (-(f h))==(f h)``. -Intros. -Generalize (strictincreasing_strictdecreasing_opp (opp_fct f)). -Unfold strict_decreasing opp_fct. -Intros. -Rewrite <- (H0 x). -Rewrite <- (H0 y). -Apply H1; [Idtac | Assumption]. -Cut (x:R)``0<(derive_pt (opp_fct f) x (derivable_opp f pr x))``. -Intros; EApply positive_derivative; Apply H3. -Intro. -Assert H3 := (derive_pt_opp f x0 (pr x0)). -Cut ``(derive_pt (opp_fct f) x0 (derivable_pt_opp f x0 (pr x0)))==(derive_pt (opp_fct f) x0 (derivable_opp f pr x0))``. -Intro. -Rewrite <- H4; Rewrite H3. -Rewrite <- Ropp_O; Apply Rlt_Ropp; Apply (H x0). -Apply pr_nu. -Intro; Ring. -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. - -(**********) -Lemma 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)``)). -Intros. -Split; Intros. -Apply Rlt_anti_compatibility with ``-(f x)``. -Rewrite Rplus_Ropp_l; Rewrite Rplus_sym. -Assert H4 := (TAF f ? ? pr H3). -Elim H4; Intros. -Elim H5; Intros. -Unfold Rminus in H6. -Rewrite H6. -Apply Rmult_lt_pos. -Apply H0. -Elim H7; Intros. -Split. -Elim H1; Intros. -Apply Rle_lt_trans with x; Assumption. -Elim H2; Intros. -Apply Rlt_le_trans with y; Assumption. -Apply Rlt_anti_compatibility with x. -Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Assumption | Ring]. -Apply Rle_anti_compatibility with ``-(f x)``. -Rewrite Rplus_Ropp_l; Rewrite Rplus_sym. -Assert H4 := (TAF f ? ? pr H3). -Elim H4; Intros. -Elim H5; Intros. -Unfold Rminus in H6. -Rewrite H6. -Apply Rmult_le_pos. -Apply H0. -Elim H7; Intros. -Split. -Elim H1; Intros. -Apply Rle_lt_trans with x; Assumption. -Elim H2; Intros. -Apply Rlt_le_trans with y; Assumption. -Apply Rle_anti_compatibility with x. -Rewrite Rplus_Or; Replace ``x+(y+ -x)`` with y; [Left; Assumption | Ring]. -Qed. - -(**********) -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. - -(**********) -(**********) -Theorem IAF : (f:R->R;a,b,k:R;pr:(derivable f)) ``a<=b`` -> ((c:R) ``a<=c<=b`` -> ``(derive_pt f c (pr c))<=k``) -> ``(f b)-(f a)<=k*(b-a)``. -Intros. -Case (total_order_T a b); Intro. -Elim s; Intro. -Assert H1 := (TAF f ? ? pr a0). -Elim H1; Intros. -Elim H2; Intros. -Rewrite H3. -Do 2 Rewrite <- (Rmult_sym ``(b-a)``). -Apply Rle_monotony. -Apply Rle_anti_compatibility with ``a``; Rewrite Rplus_Or. -Replace ``a+(b-a)`` with b; [Assumption | Ring]. -Apply H0. -Elim H4; Intros. -Split; Left; Assumption. -Rewrite b0. -Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r. -Rewrite Rmult_Or; Right; Reflexivity. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)). -Qed. +Qed.
\ No newline at end of file |