diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-07 09:42:02 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-07 09:42:02 +0000 |
commit | cd356fdc8fc2f3271873eb8cddcbb4359dedfb41 (patch) | |
tree | bc721961fd4bedd1ba23fd3fecda2e596d5224e1 /theories/Reals | |
parent | 1a443c7b9e270dd8a3329524caa04c8ce62e19d7 (diff) |
Affaiblissement des hypotheses dans TAF_gen
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3095 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
-rw-r--r-- | theories/Reals/TAF.v | 46 |
1 files changed, 36 insertions, 10 deletions
diff --git a/theories/Reals/TAF.v b/theories/Reals/TAF.v index 34f5235bc..c50714100 100644 --- a/theories/Reals/TAF.v +++ b/theories/Reals/TAF.v @@ -15,11 +15,11 @@ Require Ranalysis1. Require Rtopology. (* Théorème des accroissements finis généralisés *) -Theorem TAF_gen : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> (continuity f) -> (continuity g) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)). +Theorem TAF_gen : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)). Intros; Assert H2 := (Rlt_le ? ? H). Pose h := [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)``. Cut (c:R)``a<c<b``->(derivable_pt h c). -Intro; Cut (continuity h). +Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt h c)). Intro; Assert H4 := (continuity_ab_maj h a b H2 H3). Assert H5 := (continuity_ab_min h a b H2 H3). Elim H4; Intros Mx H6. @@ -91,12 +91,12 @@ Rewrite H8 in H10; Rewrite <- H14 in H10; Elim H10; Reflexivity. Intros; Unfold h; Replace (derive_pt [y:R]``((g b)-(g a))*(f y)-((f b)-(f a))*(g y)`` c (X c P)) with (derive_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c (derivable_pt_minus ? ? ? (derivable_pt_mult ? ? ? (derivable_pt_const ``(g b)-(g a)`` c) (pr1 c P)) (derivable_pt_mult ? ? ? (derivable_pt_const ``(f b)-(f a)`` c) (pr2 c P)))); [Idtac | Apply pr_nu]. Rewrite derive_pt_minus; Do 2 Rewrite derive_pt_mult; Do 2 Rewrite derive_pt_const; Do 2 Rewrite Rmult_Ol; Do 2 Rewrite Rplus_Ol; Reflexivity. Unfold h; Ring. -Intros; Unfold h; Change (continuity(minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g))). -Apply continuity_minus; Apply continuity_mult. -Apply derivable_continuous; Apply derivable_const. -Apply H0. -Apply derivable_continuous; Apply derivable_const. -Apply H1. +Intros; Unfold h; Change (continuity_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c). +Apply continuity_pt_minus; Apply continuity_pt_mult. +Apply derivable_continuous_pt; Apply derivable_const. +Apply H0; Apply H3. +Apply derivable_continuous_pt; Apply derivable_const. +Apply H1; Apply H3. Intros; Change (derivable_pt (minus_fct (mult_fct (fct_cte ``(g b)-(g a)``) f) (mult_fct (fct_cte ``(f b)-(f a)``) g)) c). Apply derivable_pt_minus; Apply derivable_pt_mult. Apply derivable_pt_const. @@ -109,8 +109,8 @@ Qed. Lemma 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``). Intros; Cut (c:R)``a<c<b``->(derivable_pt f c); [Intro | Intros; Apply pr]. Cut (c:R)``a<c<b``->(derivable_pt id c); [Intro | Intros; Apply derivable_pt_id]. -Cut (continuity f); [Intro | Apply derivable_continuous; Apply pr]. -Cut (continuity id); [Intro | Apply derivable_continuous; Apply derivable_id]. +Cut ((c:R)``a<=c<=b``->(continuity_pt f c)); [Intro | Intros; Apply derivable_continuous_pt; Apply pr]. +Cut ((c:R)``a<=c<=b``->(continuity_pt id c)); [Intro | Intros; Apply derivable_continuous_pt; Apply derivable_id]. Assert H2 := (TAF_gen f id a b X X0 H H0 H1). Elim H2; Intros c H3; Elim H3; Intros. Exists c; Split. @@ -119,6 +119,32 @@ Rewrite H5 in H4; Rewrite (derive_pt_id c) in H4; Rewrite Rmult_1r in H4; Rewrit Apply x. Qed. +Theorem TAF_cor1 : (f,f':R->R;a,b:R) ``a<b`` -> ((c:R)``a<=c<=b``->(derivable_pt_lim f c (f' c))) -> (EXT c:R | ``(f b)-(f a)==(f' c)*(b-a)``/\``a<c<b``). +Intros; Cut ((c:R)``a<=c<=b``->(derivable_pt f c)). +Intro; Cut ((c:R)``a<c<b``->(derivable_pt f c)). +Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt f c)). +Intro; Cut ((c:R)``a<=c<=b``->(derivable_pt id c)). +Intro; Cut ((c:R)``a<c<b``->(derivable_pt id c)). +Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt id c)). +Intro; Elim (TAF_gen f id a b X0 X2 H H1 H2); Intros; Elim H3; Clear H3; Intros; Exists x; Split. +Cut (derive_pt id x (X2 x x0))==R1. +Cut (derive_pt f x (X0 x x0))==(f' x). +Intros; Rewrite H4 in H3; Rewrite H5 in H3; Unfold id in H3; Rewrite Rmult_1r in H3; Rewrite Rmult_sym; Symmetry; Assumption. +Apply derive_pt_eq_0; Apply H0; Elim x0; Intros; Split; Left; Assumption. +Apply derive_pt_eq_0; Apply derivable_pt_lim_id. +Assumption. +Intros; Apply derivable_continuous_pt; Apply X1; Assumption. +Intros; Apply derivable_pt_id. +Intros; Apply derivable_pt_id. +Intros; Apply derivable_continuous_pt; Apply X; Assumption. +Intros; Elim H1; Intros; Apply X; Split; Left; Assumption. +Intros; Unfold derivable_pt; Apply Specif.existT with (f' c); Apply H0; Apply H1. +Qed. + +Lemma TAF_cor2 : (f,f':(R->R); a,b:R) ``a < b`` -> ((x:R)``a <= x`` -> ``x <= b``->(derivable_pt_lim f x (f' x))) -> (EXT c:R | ``a<=c``/\``c<=b``/\``(f b)==(f a) + (f' c)*(b-a)``). +Intros; Assert H1 : (EXT c:R | ``(f b) -(f a) == (f' c)*(b-a)``/\``a<c<b``); [Apply TAF_cor1; [Apply H | Intros; Elim H1; Intros; Apply (H0 ? H2 H3)] | Elim H1; Intros; Exists x; Elim H2; Intros; Elim H4; Intros; Split; [Left; Assumption | Split; [Left; Assumption | Rewrite <- H3; Ring]]]. +Qed. + (*** Corollaires ***) (**********) |