From 8b26fd6ba739d4f49fae99ed764b086022e44b50 Mon Sep 17 00:00:00 2001
From: desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 31 Jul 2002 14:34:11 +0000
Subject: MAJ pour TAF

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Ranalysis1.v | 298 +-------------------------------------------
 theories/Reals/Reals.v      |   1 +
 2 files changed, 2 insertions(+), 297 deletions(-)

(limited to 'theories')

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
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index e94f9e1cb..41909f94e 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -29,6 +29,7 @@ Require Export Rcomplet.
 Require Export Alembert_compl.
 Require Export Rtrigo_fun.
 Require Export Ranalysis.
+Require Export TAF.
 Require Export DiscrR.
 Require Export SplitRmult.
 Require Export SplitAbsolu.
-- 
cgit v1.2.3