diff options
Diffstat (limited to 'theories7/Reals/Ranalysis2.v')
| -rw-r--r-- | theories7/Reals/Ranalysis2.v | 302 |
1 files changed, 302 insertions, 0 deletions
diff --git a/theories7/Reals/Ranalysis2.v b/theories7/Reals/Ranalysis2.v new file mode 100644 index 00000000..35fa58d5 --- /dev/null +++ b/theories7/Reals/Ranalysis2.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* 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: Ranalysis2.v,v 1.1.2.1 2004/07/16 19:31:33 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +Require Ranalysis1. +V7only [Import R_scope.]. Open Local Scope R_scope. + +(**********) +Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``. +Intros; Unfold Rdiv Rminus Rsqr. +Repeat Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_Rplus_distr; Repeat Rewrite Rinv_Rmult; Try Assumption. +Replace ``l1*(f2 x)*(/(f2 x)*/(f2 x))`` with ``l1*/(f2 x)*((f2 x)*/(f2 x))``; [Idtac | Ring]. +Replace ``l1*(/(f2 x)*/(f2 (x+h)))*(f2 x)`` with ``l1*/(f2 (x+h))*((f2 x)*/(f2 x))``; [Idtac | Ring]. +Replace ``l1*(/(f2 x)*/(f2 (x+h)))* -(f2 (x+h))`` with ``-(l1*/(f2 x)*((f2 (x+h))*/(f2 (x+h))))``; [Idtac | Ring]. +Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*((f2 (x+h))*/h)`` with ``(f1 x)*/(f2 x)*/h*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring]. +Replace ``(f1 x)*(/(f2 x)*/(f2 (x+h)))*( -(f2 x)*/h)`` with ``-((f1 x)*/(f2 (x+h))*/h*((f2 x)*/(f2 x)))``; [Idtac | Ring]. +Replace ``(l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))*(f2 (x+h)))`` with ``l2*(f1 x)*/(f2 x)*/(f2 x)*((f2 (x+h))*/(f2 (x+h)))``; [Idtac | Ring]. +Replace ``l2*(f1 x)*(/(f2 x)*/(f2 x)*/(f2 (x+h)))* -(f2 x)`` with ``-(l2*(f1 x)*/(f2 x)*/(f2 (x+h))*((f2 x)*/(f2 x)))``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try Assumption Orelse Ring. +Apply prod_neq_R0; Assumption. +Qed. + +Lemma Rmin_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0 < (Rmin x y)``. +Intros; Unfold Rmin. +Case (total_order_Rle x y); Intro; Assumption. +Qed. + +Lemma maj_term1 : (x,h,eps,l1,alp_f2:R;eps_f2,alp_f1d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f1d``->``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < (Rabsolu ((eps*(f2 x))/8))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f1d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) < eps/4``. +Intros. +Assert H7 := (H3 h H6). +Assert H8 := (H2 h H4 H5). +Apply Rle_lt_trans with ``2/(Rabsolu (f2 x))*(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony_r. +Apply Rabsolu_pos. +Rewrite Rabsolu_Rinv; [Left; Exact H7 | Assumption]. +Apply Rlt_le_trans with ``2/(Rabsolu (f2 x))*(Rabsolu ((eps*(f2 x))/8))``. +Apply Rlt_monotony. +Unfold Rdiv; Apply Rmult_lt_pos; [Sup0 | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption]. +Exact H8. +Right; Unfold Rdiv. +Repeat Rewrite Rabsolu_mult. +Rewrite Rabsolu_Rinv; DiscrR. +Replace ``(Rabsolu 8)`` with ``8``. +Replace ``8`` with ``2*4``; [Idtac | Ring]. +Rewrite Rinv_Rmult; [Idtac | DiscrR | DiscrR]. +Replace ``2*/(Rabsolu (f2 x))*((Rabsolu eps)*(Rabsolu (f2 x))*(/2*/4))`` with ``(Rabsolu eps)*/4*(2*/2)*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))``; [Idtac | Ring]. +Replace (Rabsolu eps) with eps. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Symmetry; Apply Rabsolu_right; Left; Sup. +Qed. + +Lemma maj_term2 : (x,h,eps,l1,alp_f2,alp_f2t2:R;eps_f2:posreal;f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2t2``->``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``)-> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2t2`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``l1<>0`` -> ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))))) < eps/4``. +Intros. +Assert H8 := (H3 h H6). +Assert H9 := (H2 h H5). +Apply Rle_lt_trans with ``(Rabsolu (l1/((f2 x)*(f2 (x+h)))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Rewrite Rabsolu_mult; Apply Rle_monotony. +Apply Rabsolu_pos. +Rewrite <- (Rabsolu_Ropp ``(f2 x)-(f2 (x+h))``); Rewrite Ropp_distr2. +Left; Apply H9. +Apply Rlt_le_trans with ``(Rabsolu (2*l1/((f2 x)*(f2 x))))*(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption Orelse DiscrR. +Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Apply prod_neq_R0; Try Assumption Orelse DiscrR. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption. +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Rewrite (Rmult_sym ``2``). +Replace ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu l1)*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; Try Assumption. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H8; Exact H8. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Right. +Unfold Rsqr Rdiv. +Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*((Rabsolu l1)*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*(eps*((Rabsolu (f2 x))*(Rabsolu (f2 x)))*(/4*/2*/(Rabsolu l1)))`` with ``eps*/4*((Rabsolu l1)*/(Rabsolu l1))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try (Apply Rabsolu_no_R0; Assumption) Orelse DiscrR. +Ring. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Symmetry; Apply Rabsolu_right; Left; Sup. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Qed. + +Lemma maj_term3 : (x,h,eps,l2,alp_f2:R;eps_f2,alp_f2d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f2d``->``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2)) < (Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2))) < eps/4``. +Intros. +Assert H8 := (H2 h H4 H5). +Assert H9 := (H3 h H6). +Apply Rle_lt_trans with ``(Rabsolu ((f1 x)/((f2 x)*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony. +Apply Rabsolu_pos. +Left; Apply H8. +Apply Rlt_le_trans with ``(Rabsolu (2*(f1 x)/((f2 x)*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*eps)/(8*(f1 x))))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Try Assumption. +Red; Intro H10; Rewrite H10 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption. +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Rewrite (Rmult_sym ``2``). +Replace ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*(Rabsolu (/(f2 x))))*2`` with ``(Rabsolu (f1 x))*((Rabsolu (/(f2 x)))*((Rabsolu (/(f2 x)))*2))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; Assumption Orelse Idtac. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H9; Exact H9. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Right. +Unfold Rsqr Rdiv. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))))`` with ``eps*/4*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Symmetry; Apply Rabsolu_right; Left; Sup. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Qed. + +Lemma maj_term4 : (x,h,eps,l2,alp_f2,alp_f2c:R;eps_f2:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((a:R)``(Rabsolu a) < alp_f2c`` -> ``(Rabsolu ((f2 (x+a))-(f2 x))) < (Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f2c`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(f1 x)<>0`` -> ``l2<>0`` -> ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x)))) < eps/4``. +Intros. +Assert H9 := (H2 h H5). +Assert H10 := (H3 h H6). +Apply Rle_lt_trans with ``(Rabsolu ((l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Rewrite Rabsolu_mult. +Apply Rle_monotony. +Apply Rabsolu_pos. +Left; Apply H9. +Apply Rlt_le_trans with ``(Rabsolu (2*l2*(f1 x)/((Rsqr (f2 x))*(f2 x))))*(Rabsolu (((Rsqr (f2 x))*(f2 x)*eps)/(8*(f1 x)*l2)))``. +Apply Rlt_monotony_r. +Apply Rabsolu_pos_lt. +Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Assumption Orelse Idtac. +Red; Intro H11; Rewrite H11 in H; Elim (Rlt_antirefl ? H). +Apply Rinv_neq_R0; Apply prod_neq_R0. +Apply prod_neq_R0. +DiscrR. +Assumption. +Assumption. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult; Try Assumption Orelse (Unfold Rsqr; Apply prod_neq_R0; Assumption). +Repeat Rewrite Rabsolu_mult. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 x)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*((Rabsolu (/(f2 x)))*2)))``; [Idtac | Ring]. +Replace ``(Rabsolu l2)*(Rabsolu (f1 x))*((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))`` with ``(Rabsolu l2)*((Rabsolu (f1 x))*(((Rabsolu (/(Rsqr (f2 x))))*(Rabsolu (/(f2 (x+h)))))))``; [Idtac | Ring]. +Repeat Apply Rlt_monotony. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Assumption. +Apply Rabsolu_pos_lt; Apply Rinv_neq_R0; Unfold Rsqr; Apply prod_neq_R0; Assumption. +Repeat Rewrite Rabsolu_Rinv; [Idtac | Assumption | Assumption]. +Rewrite <- (Rmult_sym ``2``). +Unfold Rdiv in H10; Exact H10. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Right; Unfold Rsqr Rdiv. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Repeat Rewrite Rabsolu_mult. +Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. +Replace (Rabsolu eps) with eps. +Replace ``(Rabsolu (8))`` with ``8``. +Replace ``(Rabsolu 2)`` with ``2``. +Replace ``8`` with ``4*2``; [Idtac | Ring]. +Rewrite Rinv_Rmult; DiscrR. +Replace ``2*(Rabsolu l2)*((Rabsolu (f1 x))*(/(Rabsolu (f2 x))*/(Rabsolu (f2 x))*/(Rabsolu (f2 x))))*((Rabsolu (f2 x))*(Rabsolu (f2 x))*(Rabsolu (f2 x))*eps*(/4*/2*/(Rabsolu (f1 x))*/(Rabsolu l2)))`` with ``eps*/4*((Rabsolu l2)*/(Rabsolu l2))*((Rabsolu (f1 x))*/(Rabsolu (f1 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*((Rabsolu (f2 x))*/(Rabsolu (f2 x)))*(2*/2)``; [Idtac | Ring]. +Repeat Rewrite <- Rinv_r_sym; Try DiscrR Orelse (Apply Rabsolu_no_R0; Assumption). +Ring. +Symmetry; Apply Rabsolu_right; Left; Sup0. +Symmetry; Apply Rabsolu_right; Left; Sup. +Symmetry; Apply Rabsolu_right; Left; Assumption. +Apply prod_neq_R0; Assumption Orelse DiscrR. +Apply prod_neq_R0; Assumption. +Qed. + +Lemma D_x_no_cond : (x,a:R) ``a<>0`` -> (D_x no_cond x ``x+a``). +Intros. +Unfold D_x no_cond. +Split. +Trivial. +Apply Rminus_not_eq. +Unfold Rminus. +Rewrite Ropp_distr1. +Rewrite <- Rplus_assoc. +Rewrite Rplus_Ropp_r. +Rewrite Rplus_Ol. +Apply Ropp_neq; Assumption. +Qed. + +Lemma Rabsolu_4 : (a,b,c,d:R) ``(Rabsolu (a+b+c+d)) <= (Rabsolu a) + (Rabsolu b) + (Rabsolu c) + (Rabsolu d)``. +Intros. +Apply Rle_trans with ``(Rabsolu (a+b)) + (Rabsolu (c+d))``. +Replace ``a+b+c+d`` with ``(a+b)+(c+d)``; [Apply Rabsolu_triang | Ring]. +Apply Rle_trans with ``(Rabsolu a) + (Rabsolu b) + (Rabsolu (c+d))``. +Apply Rle_compatibility_r. +Apply Rabsolu_triang. +Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility. +Apply Rabsolu_triang. +Qed. + +Lemma Rlt_4 : (a,b,c,d,e,f,g,h:R) ``a < b`` -> ``c < d`` -> ``e < f `` -> ``g < h`` -> ``a+c+e+g < b+d+f+h``. +Intros; Apply Rlt_trans with ``b+c+e+g``. +Repeat Apply Rlt_compatibility_r; Assumption. +Repeat Rewrite Rplus_assoc; Apply Rlt_compatibility. +Apply Rlt_trans with ``d+e+g``. +Rewrite Rplus_assoc; Apply Rlt_compatibility_r; Assumption. +Rewrite Rplus_assoc; Apply Rlt_compatibility; Apply Rlt_trans with ``f+g``. +Apply Rlt_compatibility_r; Assumption. +Apply Rlt_compatibility; Assumption. +Qed. + +Lemma Rmin_2 : (a,b,c:R) ``a < b`` -> ``a < c`` -> ``a < (Rmin b c)``. +Intros; Unfold Rmin; Case (total_order_Rle b c); Intro; Assumption. +Qed. + +Lemma quadruple : (x:R) ``4*x == x + x + x + x``. +Intro; Ring. +Qed. + +Lemma quadruple_var : (x:R) `` x == x/4 + x/4 + x/4 + x/4``. +Intro; Rewrite <- quadruple. +Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m; DiscrR. +Reflexivity. +Qed. + +(**********) +Lemma continuous_neq_0 : (f:R->R; x0:R) (continuity_pt f x0) -> ~``(f x0)==0`` -> (EXT eps : posreal | (h:R) ``(Rabsolu h) < eps`` -> ~``(f (x0+h))==0``). +Intros; Unfold continuity_pt in H; Unfold continue_in in H; Unfold limit1_in in H; Unfold limit_in in H; Elim (H ``(Rabsolu ((f x0)/2))``). +Intros; Elim H1; Intros. +Exists (mkposreal x H2). +Intros; Assert H5 := (H3 ``x0+h``). +Cut ``(dist R_met (x0+h) x0) < x`` -> ``(dist R_met (f (x0+h)) (f x0)) < (Rabsolu ((f x0)/2))``. +Unfold dist; Simpl; Unfold R_dist; Replace ``x0+h-x0`` with h. +Intros; Assert H7 := (H6 H4). +Red; Intro. +Rewrite H8 in H7; Unfold Rminus in H7; Rewrite Rplus_Ol in H7; Rewrite Rabsolu_Ropp in H7; Unfold Rdiv in H7; Rewrite Rabsolu_mult in H7; Pattern 1 ``(Rabsolu (f x0)) `` in H7; Rewrite <- Rmult_1r in H7. +Cut ``0<(Rabsolu (f x0))``. +Intro; Assert H10 := (Rlt_monotony_contra ? ? ? H9 H7). +Cut ``(Rabsolu (/2))==/2``. +Assert Hyp:``0<2``. +Sup0. +Intro; Rewrite H11 in H10; Assert H12 := (Rlt_monotony ``2`` ? ? Hyp H10); Rewrite Rmult_1r in H12; Rewrite <- Rinv_r_sym in H12; [Idtac | DiscrR]. +Cut (Rlt (IZR `1`) (IZR `2`)). +Unfold IZR; Unfold INR convert; Simpl; Intro; Elim (Rlt_antirefl ``1`` (Rlt_trans ? ? ? H13 H12)). +Apply IZR_lt; Omega. +Unfold Rabsolu; Case (case_Rabsolu ``/2``); Intro. +Assert Hyp:``0<2``. +Sup0. +Assert H11 := (Rlt_monotony ``2`` ? ? Hyp r); Rewrite Rmult_Or in H11; Rewrite <- Rinv_r_sym in H11; [Idtac | DiscrR]. +Elim (Rlt_antirefl ``0`` (Rlt_trans ? ? ? Rlt_R0_R1 H11)). +Reflexivity. +Apply (Rabsolu_pos_lt ? H0). +Ring. +Assert H6 := (Req_EM ``x0`` ``x0+h``); Elim H6; Intro. +Intro; Rewrite <- H7; Unfold dist R_met; Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos_lt. +Unfold Rdiv; Apply prod_neq_R0; [Assumption | Apply Rinv_neq_R0; DiscrR]. +Intro; Apply H5. +Split. +Unfold D_x no_cond. +Split; Trivial Orelse Assumption. +Assumption. +Change ``0 < (Rabsolu ((f x0)/2))``. +Apply Rabsolu_pos_lt; Unfold Rdiv; Apply prod_neq_R0. +Assumption. +Apply Rinv_neq_R0; DiscrR. +Qed. |