diff options
Diffstat (limited to 'theories7/Reals/Rlimit.v')
| -rw-r--r-- | theories7/Reals/Rlimit.v | 539 |
1 files changed, 539 insertions, 0 deletions
diff --git a/theories7/Reals/Rlimit.v b/theories7/Reals/Rlimit.v new file mode 100644 index 00000000..3308b2e3 --- /dev/null +++ b/theories7/Reals/Rlimit.v @@ -0,0 +1,539 @@ +(************************************************************************) +(* 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: Rlimit.v,v 1.1.2.1 2004/07/16 19:31:35 herbelin Exp $ i*) + +(*********************************************************) +(* Definition of the limit *) +(* *) +(*********************************************************) + +Require Rbase. +Require Rfunctions. +Require Classical_Prop. +Require Fourier. +V7only [Import R_scope.]. Open Local Scope R_scope. + +(*******************************) +(* Calculus *) +(*******************************) +(*********) +Lemma eps2_Rgt_R0:(eps:R)(Rgt eps R0)-> + (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0). +Intros;Fourier. +Qed. + +(*********) +Lemma eps2:(eps:R)(Rplus (Rmult eps (Rinv (Rplus R1 R1))) + (Rmult eps (Rinv (Rplus R1 R1))))==eps. +Intro esp. +Assert H := (double_var esp). +Unfold Rdiv in H. +Symmetry; Exact H. +Qed. + +(*********) +Lemma eps4:(eps:R) + (Rplus (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) ))) + (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) ))))== + (Rmult eps (Rinv (Rplus R1 R1))). +Intro eps. +Replace ``2+2`` with ``2*2``. +Pattern 3 eps; Rewrite double_var. +Rewrite (Rmult_Rplus_distrl ``eps/2`` ``eps/2`` ``/2``). +Unfold Rdiv. +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_Rmult. +Reflexivity. +DiscrR. +DiscrR. +Ring. +Qed. + +(*********) +Lemma Rlt_eps2_eps:(eps:R)(Rgt eps R0)-> + (Rlt (Rmult eps (Rinv (Rplus R1 R1))) eps). +Intros. +Pattern 2 eps; Rewrite <- Rmult_1r. +Repeat Rewrite (Rmult_sym eps). +Apply Rlt_monotony_r. +Exact H. +Apply Rlt_monotony_contra with ``2``. +Fourier. +Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. +Fourier. +DiscrR. +Qed. + +(*********) +Lemma Rlt_eps4_eps:(eps:R)(Rgt eps R0)-> + (Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps). +Intros. +Replace ``2+2`` with ``4``. +Pattern 2 eps; Rewrite <- Rmult_1r. +Repeat Rewrite (Rmult_sym eps). +Apply Rlt_monotony_r. +Exact H. +Apply Rlt_monotony_contra with ``4``. +Replace ``4`` with ``2*2``. +Apply Rmult_lt_pos; Fourier. +Ring. +Rewrite Rmult_1r; Rewrite <- Rinv_r_sym. +Fourier. +DiscrR. +Ring. +Qed. + +(*********) +Lemma prop_eps:(r:R)((eps:R)(Rgt eps R0)->(Rlt r eps))->(Rle r R0). +Intros;Elim (total_order r R0); Intro. +Apply Rlt_le; Assumption. +Elim H0; Intro. +Apply eq_Rle; Assumption. +Clear H0;Generalize (H r H1); Intro;Generalize (Rlt_antirefl r); + Intro;ElimType False; Auto. +Qed. + +(*********) +Definition mul_factor := [l,l':R](Rinv (Rplus R1 (Rplus (Rabsolu l) + (Rabsolu l')))). + +(*********) +Lemma mul_factor_wd : (l,l':R) + ~(Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))==R0. +Intros;Rewrite (Rplus_sym R1 (Rplus (Rabsolu l) (Rabsolu l'))); + Apply tech_Rplus. +Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))). +Cut (Rle R0 (Rabsolu (Rplus l l'))). +Exact (Rle_trans ? ? ?). +Exact (Rabsolu_pos (Rplus l l')). +Exact (Rabsolu_triang ? ?). +Exact Rlt_R0_R1. +Qed. + +(*********) +Lemma mul_factor_gt:(eps:R)(l,l':R)(Rgt eps R0)-> + (Rgt (Rmult eps (mul_factor l l')) R0). +Intros;Unfold Rgt;Rewrite <- (Rmult_Or eps);Apply Rlt_monotony. +Assumption. +Unfold mul_factor;Apply Rlt_Rinv; + Cut (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))). +Cut (Rlt R0 R1). +Exact (Rlt_le_trans ? ? ?). +Exact Rlt_R0_R1. +Replace (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))) + with (Rle (Rplus R1 R0) (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))). +Apply Rle_compatibility. +Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))). +Cut (Rle R0 (Rabsolu (Rplus l l'))). +Exact (Rle_trans ? ? ?). +Exact (Rabsolu_pos ?). +Exact (Rabsolu_triang ? ?). +Rewrite (proj1 ? ? (Rplus_ne R1));Trivial. +Qed. + +(*********) +Lemma mul_factor_gt_f:(eps:R)(l,l':R)(Rgt eps R0)-> + (Rgt (Rmin R1 (Rmult eps (mul_factor l l'))) R0). +Intros;Apply Rmin_Rgt_r;Split. +Exact Rlt_R0_R1. +Exact (mul_factor_gt eps l l' H). +Qed. + + +(*******************************) +(* Metric space *) +(*******************************) + +(*********) +Record Metric_Space:Type:= { + Base:Type; + dist:Base->Base->R; + dist_pos:(x,y:Base)(Rge (dist x y) R0); + dist_sym:(x,y:Base)(dist x y)==(dist y x); + dist_refl:(x,y:Base)((dist x y)==R0<->x==y); + dist_tri:(x,y,z:Base)(Rle (dist x y) + (Rplus (dist x z) (dist z y))) }. + +(*******************************) +(* Limit in Metric space *) +(*******************************) + +(*********) +Definition limit_in:= + [X:Metric_Space; X':Metric_Space; f:(Base X)->(Base X'); + D:(Base X)->Prop; x0:(Base X); l:(Base X')] + (eps:R)(Rgt eps R0)-> + (EXT alp:R | (Rgt alp R0)/\(x:(Base X))(D x)/\ + (Rlt (dist X x x0) alp)-> + (Rlt (dist X' (f x) l) eps)). + +(*******************************) +(* R is a metric space *) +(*******************************) + +(*********) +Definition R_met:Metric_Space:=(Build_Metric_Space R R_dist + R_dist_pos R_dist_sym R_dist_refl R_dist_tri). + +(*******************************) +(* Limit 1 arg *) +(*******************************) +(*********) +Definition Dgf:=[Df,Dg:R->Prop][f:R->R][x:R](Df x)/\(Dg (f x)). + +(*********) +Definition limit1_in:(R->R)->(R->Prop)->R->R->Prop:= + [f:R->R; D:R->Prop; l:R; x0:R](limit_in R_met R_met f D x0 l). + +(*********) +Lemma tech_limit:(f:R->R)(D:R->Prop)(l:R)(x0:R)(D x0)-> + (limit1_in f D l x0)->l==(f x0). +Intros f D l x0 H H0. +Case (Rabsolu_pos (Rminus (f x0) l)); Intros H1. +Absurd (Rlt (dist R_met (f x0) l) (dist R_met (f x0) l)). +Apply Rlt_antirefl. +Case (H0 (dist R_met (f x0) l)); Auto. +Intros alpha1 (H2, H3); Apply H3; Auto; Split; Auto. +Case (dist_refl R_met x0 x0); Intros Hr1 Hr2; Rewrite Hr2; Auto. +Case (dist_refl R_met (f x0) l); Intros Hr1 Hr2; Apply sym_eqT; Auto. +Qed. + +(*********) +Lemma tech_limit_contr:(f:R->R)(D:R->Prop)(l:R)(x0:R)(D x0)->~l==(f x0) + ->~(limit1_in f D l x0). +Intros;Generalize (tech_limit f D l x0);Tauto. +Qed. + +(*********) +Lemma lim_x:(D:R->Prop)(x0:R)(limit1_in [x:R]x D x0 x0). +Unfold limit1_in; Unfold limit_in; Simpl; Intros;Split with eps; + Split; Auto;Intros;Elim H0; Intros; Auto. +Qed. + +(*********) +Lemma limit_plus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) + (limit1_in f D l x0)->(limit1_in g D l' x0)-> + (limit1_in [x:R](Rplus (f x) (g x)) D (Rplus l l') x0). +Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros; + Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1)); + Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1)); + Simpl;Clear H H0; Intros; Elim H; Elim H0; Clear H H0; Intros; + Split with (Rmin x1 x); Split. +Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)). +Intros;Elim H4; Clear H4; Intros; + Cut (Rlt (Rplus (R_dist (f x2) l) (R_dist (g x2) l')) eps). + Cut (Rle (R_dist (Rplus (f x2) (g x2)) (Rplus l l')) + (Rplus (R_dist (f x2) l) (R_dist (g x2) l'))). +Exact (Rle_lt_trans ? ? ?). +Exact (R_dist_plus ? ? ? ?). +Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros. +Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6)); + Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5)); + Intros; + Replace eps + with (Rplus (Rmult eps (Rinv (Rplus R1 R1))) + (Rmult eps (Rinv (Rplus R1 R1)))). +Exact (Rplus_lt ? ? ? ? H7 H8). +Exact (eps2 eps). +Qed. + +(*********) +Lemma limit_Ropp:(f:R->R)(D:R->Prop)(l:R)(x0:R) + (limit1_in f D l x0)->(limit1_in [x:R](Ropp (f x)) D (Ropp l) x0). +Unfold limit1_in;Unfold limit_in;Simpl;Intros;Elim (H eps H0);Clear H; + Intros;Elim H;Clear H;Intros;Split with x;Split;Auto;Intros; + Generalize (H1 x1 H2);Clear H1;Intro;Unfold R_dist;Unfold Rminus; + Rewrite (Ropp_Ropp l);Rewrite (Rplus_sym (Ropp (f x1)) l); + Fold (Rminus l (f x1));Fold (R_dist l (f x1));Rewrite R_dist_sym; + Assumption. +Qed. + +(*********) +Lemma limit_minus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) + (limit1_in f D l x0)->(limit1_in g D l' x0)-> + (limit1_in [x:R](Rminus (f x) (g x)) D (Rminus l l') x0). +Intros;Unfold Rminus;Generalize (limit_Ropp g D l' x0 H0);Intro; + Exact (limit_plus f [x:R](Ropp (g x)) D l (Ropp l') x0 H H1). +Qed. + +(*********) +Lemma limit_free:(f:R->R)(D:R->Prop)(x:R)(x0:R) + (limit1_in [h:R](f x) D (f x) x0). +Unfold limit1_in;Unfold limit_in;Simpl;Intros;Split with eps;Split; + Auto;Intros;Elim (R_dist_refl (f x) (f x));Intros a b; + Rewrite (b (refl_eqT R (f x)));Unfold Rgt in H;Assumption. +Qed. + +(*********) +Lemma limit_mul:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R) + (limit1_in f D l x0)->(limit1_in g D l' x0)-> + (limit1_in [x:R](Rmult (f x) (g x)) D (Rmult l l') x0). +Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros; + Elim (H (Rmin R1 (Rmult eps (mul_factor l l'))) + (mul_factor_gt_f eps l l' H1)); + Elim (H0 (Rmult eps (mul_factor l l')) (mul_factor_gt eps l l' H1)); + Clear H H0; Simpl; Intros; Elim H; Elim H0; Clear H H0; Intros; + Split with (Rmin x1 x); Split. +Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)). +Intros; Elim H4; Clear H4; Intros;Unfold R_dist; + Replace (Rminus (Rmult (f x2) (g x2)) (Rmult l l')) with + (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus (f x2) l))). +Cut (Rlt (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu (Rmult l' + (Rminus (f x2) l)))) eps). +Cut (Rle (Rabsolu (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus + (f x2) l)))) (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu + (Rmult l' (Rminus (f x2) l))))). +Exact (Rle_lt_trans ? ? ?). +Exact (Rabsolu_triang ? ?). +Rewrite (Rabsolu_mult (f x2) (Rminus (g x2) l')); + Rewrite (Rabsolu_mult l' (Rminus (f x2) l)); + Cut (Rle (Rplus (Rmult (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l'))) + (Rmult (Rabsolu l') (Rmult eps (mul_factor l l')))) eps). +Cut (Rlt (Rplus (Rmult (Rabsolu (f x2)) (Rabsolu (Rminus (g x2) l'))) (Rmult + (Rabsolu l') (Rabsolu (Rminus (f x2) l)))) (Rplus (Rmult (Rplus R1 (Rabsolu + l)) (Rmult eps (mul_factor l l'))) (Rmult (Rabsolu l') (Rmult eps + (mul_factor l l'))))). +Exact (Rlt_le_trans ? ? ?). +Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros; + Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));Intro; + Generalize (Rmin_Rgt_l ? ? ? H7);Intro;Elim H8;Intros;Clear H0 H8; + Apply Rplus_lt_le_lt. +Apply Rmult_lt_0. +Apply Rle_sym1. +Exact (Rabsolu_pos (Rminus (g x2) l')). +Rewrite (Rplus_sym R1 (Rabsolu l));Unfold Rgt;Apply Rlt_r_plus_R1; + Exact (Rabsolu_pos l). +Unfold R_dist in H9; + Apply (Rlt_anti_compatibility (Ropp (Rabsolu l)) (Rabsolu (f x2)) + (Rplus R1 (Rabsolu l))). +Rewrite <- (Rplus_assoc (Ropp (Rabsolu l)) R1 (Rabsolu l)); + Rewrite (Rplus_sym (Ropp (Rabsolu l)) R1); + Rewrite (Rplus_assoc R1 (Ropp (Rabsolu l)) (Rabsolu l)); + Rewrite (Rplus_Ropp_l (Rabsolu l)); + Rewrite (proj1 ? ? (Rplus_ne R1)); + Rewrite (Rplus_sym (Ropp (Rabsolu l)) (Rabsolu (f x2))); + Generalize H9; +Cut (Rle (Rminus (Rabsolu (f x2)) (Rabsolu l)) (Rabsolu (Rminus (f x2) l))). +Exact (Rle_lt_trans ? ? ?). +Exact (Rabsolu_triang_inv ? ?). +Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));Trivial. +Apply Rle_monotony. +Exact (Rabsolu_pos l'). +Unfold Rle;Left;Assumption. +Rewrite (Rmult_sym (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l'))); + Rewrite (Rmult_sym (Rabsolu l') (Rmult eps (mul_factor l l'))); + Rewrite <- (Rmult_Rplus_distr + (Rmult eps (mul_factor l l')) + (Rplus R1 (Rabsolu l)) + (Rabsolu l')); + Rewrite (Rmult_assoc eps (mul_factor l l') (Rplus (Rplus R1 (Rabsolu l)) + (Rabsolu l'))); + Rewrite (Rplus_assoc R1 (Rabsolu l) (Rabsolu l'));Unfold mul_factor; + Rewrite (Rinv_l (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l'))) + (mul_factor_wd l l')); + Rewrite (proj1 ? ? (Rmult_ne eps));Apply eq_Rle;Trivial. +Ring. +Qed. + +(*********) +Definition adhDa:(R->Prop)->R->Prop:=[D:R->Prop][a:R] + (alp:R)(Rgt alp R0)->(EXT x:R | (D x)/\(Rlt (R_dist x a) alp)). + +(*********) +Lemma single_limit:(f:R->R)(D:R->Prop)(l:R)(l':R)(x0:R) + (adhDa D x0)->(limit1_in f D l x0)->(limit1_in f D l' x0)->l==l'. +Unfold limit1_in; Unfold limit_in; Intros. +Cut (eps:R)(Rgt eps R0)->(Rlt (dist R_met l l') + (Rmult (Rplus R1 R1) eps)). +Clear H0 H1;Unfold dist; Unfold R_met; Unfold R_dist; + Unfold Rabsolu;Case (case_Rabsolu (Rminus l l')); Intros. +Cut (eps:R)(Rgt eps R0)->(Rlt (Ropp (Rminus l l')) eps). +Intro;Generalize (prop_eps (Ropp (Rminus l l')) H1);Intro; + Generalize (Rlt_RoppO (Rminus l l') r); Intro;Unfold Rgt in H3; + Generalize (Rle_not (Ropp (Rminus l l')) R0 H3); Intro; + ElimType False; Auto. +Intros;Cut (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0). +Intro;Generalize (H0 (Rmult eps (Rinv (Rplus R1 R1))) H2); + Rewrite (Rmult_sym eps (Rinv (Rplus R1 R1))); + Rewrite <- (Rmult_assoc (Rplus R1 R1) (Rinv (Rplus R1 R1)) eps); + Rewrite (Rinv_r (Rplus R1 R1)). +Elim (Rmult_ne eps);Intros a b;Rewrite b;Clear a b;Trivial. +Apply (imp_not_Req (Rplus R1 R1) R0);Right;Generalize Rlt_R0_R1;Intro; + Unfold Rgt;Generalize (Rlt_compatibility R1 R0 R1 H3);Intro; + Elim (Rplus_ne R1);Intros a b;Rewrite a in H4;Clear a b; + Apply (Rlt_trans R0 R1 (Rplus R1 R1) H3 H4). +Unfold Rgt;Unfold Rgt in H1; + Rewrite (Rmult_sym eps(Rinv (Rplus R1 R1))); + Rewrite <-(Rmult_Or (Rinv (Rplus R1 R1))); + Apply (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps);Auto. +Apply (Rlt_Rinv (Rplus R1 R1));Cut (Rlt R1 (Rplus R1 R1)). +Intro;Apply (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H2). +Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Elim (Rplus_ne R1); + Intros a b;Rewrite a;Clear a b;Trivial. +(**) +Cut (eps:R)(Rgt eps R0)->(Rlt (Rminus l l') eps). +Intro;Generalize (prop_eps (Rminus l l') H1);Intro; + Elim (Rle_le_eq (Rminus l l') R0);Intros a b;Clear b; + Apply (Rminus_eq l l');Apply a;Split. +Assumption. +Apply (Rle_sym2 R0 (Rminus l l') r). +Intros;Cut (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0). +Intro;Generalize (H0 (Rmult eps (Rinv (Rplus R1 R1))) H2); + Rewrite (Rmult_sym eps (Rinv (Rplus R1 R1))); + Rewrite <- (Rmult_assoc (Rplus R1 R1) (Rinv (Rplus R1 R1)) eps); + Rewrite (Rinv_r (Rplus R1 R1)). +Elim (Rmult_ne eps);Intros a b;Rewrite b;Clear a b;Trivial. +Apply (imp_not_Req (Rplus R1 R1) R0);Right;Generalize Rlt_R0_R1;Intro; + Unfold Rgt;Generalize (Rlt_compatibility R1 R0 R1 H3);Intro; + Elim (Rplus_ne R1);Intros a b;Rewrite a in H4;Clear a b; + Apply (Rlt_trans R0 R1 (Rplus R1 R1) H3 H4). +Unfold Rgt;Unfold Rgt in H1; + Rewrite (Rmult_sym eps(Rinv (Rplus R1 R1))); + Rewrite <-(Rmult_Or (Rinv (Rplus R1 R1))); + Apply (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps);Auto. +Apply (Rlt_Rinv (Rplus R1 R1));Cut (Rlt R1 (Rplus R1 R1)). +Intro;Apply (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H2). +Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Elim (Rplus_ne R1); + Intros a b;Rewrite a;Clear a b;Trivial. +(**) +Intros;Unfold adhDa in H;Elim (H0 eps H2);Intros;Elim (H1 eps H2); + Intros;Clear H0 H1;Elim H3;Elim H4;Clear H3 H4;Intros; + Simpl;Simpl in H1 H4;Generalize (Rmin_Rgt x x1 R0);Intro;Elim H5; + Intros;Clear H5; + Elim (H (Rmin x x1) (H7 (conj (Rgt x R0) (Rgt x1 R0) H3 H0))); + Intros; Elim H5;Intros;Clear H5 H H6 H7; + Generalize (Rmin_Rgt x x1 (R_dist x2 x0));Intro;Elim H; + Intros;Clear H H6;Unfold Rgt in H5;Elim (H5 H9);Intros;Clear H5 H9; + Generalize (H1 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H8 H6)); + Generalize (H4 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H8 H)); + Clear H8 H H6 H1 H4 H0 H3;Intros; + Generalize (Rplus_lt (R_dist (f x2) l) eps (R_dist (f x2) l') eps + H H0); Unfold R_dist;Intros; + Rewrite (Rabsolu_minus_sym (f x2) l) in H1; + Rewrite (Rmult_sym (Rplus R1 R1) eps);Rewrite (Rmult_Rplus_distr eps R1 R1); + Elim (Rmult_ne eps);Intros a b;Rewrite a;Clear a b; + Generalize (R_dist_tri l l' (f x2));Unfold R_dist;Intros; + Apply (Rle_lt_trans (Rabsolu (Rminus l l')) + (Rplus (Rabsolu (Rminus l (f x2))) (Rabsolu (Rminus (f x2) l'))) + (Rplus eps eps) H3 H1). +Qed. + +(*********) +Lemma limit_comp:(f,g:R->R)(Df,Dg:R->Prop)(l,l':R)(x0:R) + (limit1_in f Df l x0)->(limit1_in g Dg l' l)-> + (limit1_in [x:R](g (f x)) (Dgf Df Dg f) l' x0). +Unfold limit1_in limit_in Dgf;Simpl. +Intros f g Df Dg l l' x0 Hf Hg eps eps_pos. +Elim (Hg eps eps_pos). +Intros alpg lg. +Elim (Hf alpg). +2: Tauto. +Intros alpf lf. +Exists alpf. +Intuition. +Qed. + +(*********) + +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. +Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym l). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Rewrite (Rmult_sym l). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r; Reflexivity. +DiscrR. +Exact H0. +Exact H0. +Exact H0. +Exact H0. +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; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro H18; Assumption | Discriminate]. +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. +Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym (Rabsolu l)). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r; Reflexivity. +DiscrR. +Apply Rabsolu_no_R0. +Assumption. +Unfold Rdiv. +Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym (Rabsolu (f x))). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Reflexivity. +Apply Rabsolu_no_R0; 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. +Rewrite (Rinv_Rmult ? ? H0 H16). +Unfold Rminus; Rewrite Rmult_Rplus_distrl. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l. +Rewrite Ropp_mul1. +Rewrite (Rmult_sym (f x)). +Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Reflexivity. +Assumption. +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; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro; Assumption | Discriminate]. +Pattern 3 (Rabsolu l); Rewrite double_var. +Ring. +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; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]. +Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H3; Generalize (lt_INR_0 (2) (neq_O_lt (2) H3)); Unfold INR; Intro; Assumption | Discriminate]]. +Qed. |