*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2270 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 80 insertions, 0 deletions

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 39cca741c4..19ac6d97b6 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -37,6 +37,10 @@ Lemma Rsqr_gt_0_0 : (x:R) ``0<(Rsqr x)`` -> ~``x==0``.
 Intros; Red; Intro; Rewrite H0 in H; Rewrite Rsqr_O in H; Elim (Rlt_antirefl ``0`` H).
 Save.
 
+Lemma Rsqr_pos_lt : (x:R) ~(x==R0)->``0<(Rsqr x)``.
+Intros; Case (total_order R0 x); Intro; [Unfold Rsqr; Apply Rmult_lt_pos; Assumption | Elim H0; Intro; [Elim H; Symmetry; Exact H1 | Rewrite Rsqr_neg; Generalize (Rlt_Ropp x ``0`` H1); Rewrite Ropp_O; Intro; Unfold Rsqr; Apply Rmult_lt_pos; Assumption]].
+Save.
+
 Lemma Rsqr_div : (x,y:R) ~``y==0`` -> ``(Rsqr (x/y))==(Rsqr x)/(Rsqr y)``.
 Intros; Unfold Rsqr; Field; Repeat Apply prod_neq_R0; Assumption.
 Save.
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 78e0876a02..45e03ca7aa 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1581,4 +1581,31 @@ end.
 
 Theorem INR_eq_INR2 : (n:nat) (INR n)==(INR2 n).
 Induction n; [Unfold INR INR2; Reflexivity | Intros; Unfold INR INR2; Fold INR INR2; Rewrite H; Case n0; [Reflexivity | Intros; Ring]].
+Save.
+
+(*****************************************************)
+(*          Some properties of Rmin and Rmax         *)
+(*****************************************************)
+Lemma Rmin_l : (x,y:R) ``(Rmin x y)<=x``.
+Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real].
+Save.
+  
+Lemma Rmin_r : (x,y:R) ``(Rmin x y)<=y``.
+Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Assumption | Auto with real].
+Save.
+
+Lemma Rmin_stable_in_posreal : (x,y:posreal) ``0<(Rmin x y)``.
+Intros; Apply Rmin_Rgt_r; Split; [Apply (cond_pos x) | Apply (cond_pos y)].
+Save.
+
+Lemma Rmax_l : (x,y:R) ``x<=(Rmax x y)``.
+Intros; Unfold Rmax; Case (total_order_Rle x y); Intro H1; [Assumption | Right; Reflexivity].
+Save.
+
+Lemma Rmax_r : (x,y:R) ``y<=(Rmax x y)``.
+Intros; Unfold Rmax; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real].
+Save.
+
+Lemma Rmax_stable_in_negreal : (x,y:negreal) ``(Rmax x y)<0``.
+Intros; Unfold Rmax; Case (total_order_Rle x y); Intro; [Apply (cond_neg y) | Apply (cond_neg x)].
 Save.
\ No newline at end of file
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 3ebeccfdd9..974c411dc2 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -581,3 +581,52 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros;
  Intro;Exact (H2 (f x2) (conj (Dg (f x2)) (Rlt (R_dist (f x2) l) x)
             H6 H7)).
 Save.
+
+(*********)
+Lemma limit_inv : (f:R->R)(D:R->Prop)(l:R)(x0:R) (limit1_in f D l x0)->~(l==R0)->(limit1_in [x:R](Rinv (f x)) D (Rinv l) x0).
+Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H ``(Rabsolu l)/2``).
+Intros delta1 H2; Elim (H ``eps*((Rsqr l)/2)``).
+Intros delta2 H3; Elim H2; Elim H3; Intros; Exists (Rmin delta1 delta2); Split.
+Unfold Rmin; Case (total_order_Rle delta1 delta2); Intro; Assumption.
+Intro; Generalize (H5 x); Clear H5; Intro H5; Generalize (H7 x); Clear H7; Intro H7; Intro H10; Elim H10; Intros; Cut (D x)/\``(Rabsolu (x-x0))<delta1``.
+Cut (D x)/\``(Rabsolu (x-x0))<delta2``.
+Intros; Generalize (H5 H11); Clear H5; Intro H5; Generalize (H7 H12); Clear H7; Intro H7; Generalize (Rabsolu_triang_inv l (f x)); Intro; Rewrite Rabsolu_minus_sym in H7; Generalize (Rle_lt_trans ``(Rabsolu l)-(Rabsolu (f x))`` ``(Rabsolu (l-(f x)))`` ``(Rabsolu l)/2`` H13 H7); Intro; Generalize (Rlt_compatibility ``(Rabsolu (f x))-(Rabsolu l)/2`` ``(Rabsolu l)-(Rabsolu (f x))`` ``(Rabsolu l)/2`` H14); Replace ``(Rabsolu (f x))-(Rabsolu l)/2+((Rabsolu l)-(Rabsolu (f x)))`` with ``(Rabsolu l)/2``.
+Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Intro; Cut ~``(f x)==0``.
+Intro; Replace ``/(f x)+ -/l`` with ``(l-(f x))*/(l*(f x))``.
+Rewrite Rabsolu_mult; Rewrite Rabsolu_Rinv.
+Cut ``/(Rabsolu (l*(f x)))<2/(Rsqr l)``.
+Intro; Rewrite Rabsolu_minus_sym in H5; Cut ``0<=/(Rabsolu (l*(f x)))``.
+Intro; Generalize (Rmult_lt2 ``(Rabsolu (l-(f x)))`` ``eps*(Rsqr l)/2`` ``/(Rabsolu (l*(f x)))`` ``2/(Rsqr l)`` (Rabsolu_pos ``l-(f x)``) H18 H5 H17); Replace ``eps*(Rsqr l)/2*2/(Rsqr l)`` with ``eps``.
+Intro; Assumption.
+Unfold Rdiv; Unfold Rsqr; Rewrite Rinv_Rmult.
+Field.
+Repeat Apply prod_neq_R0; [DiscrR | Assumption | Assumption].
+Assumption.
+Assumption.
+Left; Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply prod_neq_R0; Assumption.
+Rewrite Rmult_sym; Rewrite Rabsolu_mult; Rewrite Rinv_Rmult.
+Rewrite (Rsqr_abs l); Unfold Rsqr; Unfold Rdiv; Rewrite Rinv_Rmult.
+Repeat Rewrite <- Rmult_assoc; Apply Rlt_monotony_r.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption.
+Apply Rlt_monotony_contra with ``(Rabsolu (f x))*(Rabsolu l)*/2``.
+Repeat Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
+Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*/(Rabsolu (f x))`` with ``(Rabsolu l)/2``.
+Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*(2*/(Rabsolu l))`` with ``(Rabsolu (f x))``.
+Assumption.
+Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]].
+Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]].
+Apply Rabsolu_no_R0; Assumption.
+Apply Rabsolu_no_R0; Assumption.
+Apply Rabsolu_no_R0; Assumption.
+Apply Rabsolu_no_R0; Assumption.
+Apply prod_neq_R0; Assumption.
+Field; Repeat Apply prod_neq_R0; Assumption.
+Red; Intro; Rewrite H16 in H15; Rewrite Rabsolu_R0 in H15; Cut ``0<(Rabsolu l)/2``.
+Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rabsolu l)/2`` ``0`` H17 H15)).
+Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
+Unfold Rdiv; Field; DiscrR.
+Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_r]].
+Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_l]].
+Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos; [Assumption | Apply Rsqr_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
+Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
+Save.