diff options
Diffstat (limited to 'theories7/Reals/SeqProp.v')
| -rw-r--r-- | theories7/Reals/SeqProp.v | 1089 |
1 files changed, 0 insertions, 1089 deletions
diff --git a/theories7/Reals/SeqProp.v b/theories7/Reals/SeqProp.v deleted file mode 100644 index b34fa339..00000000 --- a/theories7/Reals/SeqProp.v +++ /dev/null @@ -1,1089 +0,0 @@ -(************************************************************************) -(* 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: SeqProp.v,v 1.1.2.1 2004/07/16 19:31:36 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require Rseries. -Require Classical. -Require Max. -V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. -Open Local Scope R_scope. - -Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)). -Definition opp_seq [Un:nat->R] : nat->R := [n:nat]``-(Un n)``. -Definition has_ub [Un:nat->R] : Prop := (bound (EUn Un)). -Definition has_lb [Un:nat->R] : Prop := (bound (EUn (opp_seq Un))). - -(**********) -Lemma growing_cv : (Un:nat->R) (Un_growing Un) -> (has_ub Un) -> (sigTT R [l:R](Un_cv Un l)). -Unfold Un_growing Un_cv;Intros; - NewDestruct (complet (EUn Un) H0 (EUn_noempty Un)) as [x [H2 H3]]. - Exists x;Intros eps H1. - Unfold is_upper_bound in H2 H3. -Assert H5:(n:nat)(Rle (Un n) x). - Intro n; Apply (H2 (Un n) (Un_in_EUn Un n)). -Cut (Ex [N:nat] (Rlt (Rminus x eps) (Un N))). -Intro H6;NewDestruct H6 as [N H6];Exists N. -Intros n H7;Unfold R_dist;Apply (Rabsolu_def1 (Rminus (Un n) x) eps). -Unfold Rgt in H1. - Apply (Rle_lt_trans (Rminus (Un n) x) R0 eps - (Rle_minus (Un n) x (H5 n)) H1). -Fold Un_growing in H;Generalize (growing_prop Un n N H H7);Intro H8. - Generalize (Rlt_le_trans (Rminus x eps) (Un N) (Un n) H6 - (Rle_sym2 (Un N) (Un n) H8));Intro H9; - Generalize (Rlt_compatibility (Ropp x) (Rminus x eps) (Un n) H9); - Unfold Rminus;Rewrite <-(Rplus_assoc (Ropp x) x (Ropp eps)); - Rewrite (Rplus_sym (Ropp x) (Un n));Fold (Rminus (Un n) x); - Rewrite Rplus_Ropp_l;Rewrite (let (H1,H2)=(Rplus_ne (Ropp eps)) in H2); - Trivial. -Cut ~((N:nat)(Rle (Un N) (Rminus x eps))). -Intro H6;Apply (not_all_not_ex nat ([N:nat](Rlt (Rminus x eps) (Un N)))). - Intro H7; Apply H6; Intro N; Apply Rnot_lt_le; Apply H7. -Intro H7;Generalize (Un_bound_imp Un (Rminus x eps) H7);Intro H8; - Unfold is_upper_bound in H8;Generalize (H3 (Rminus x eps) H8); - Apply Rlt_le_not; Apply tech_Rgt_minus; Exact H1. -Qed. - -Lemma decreasing_growing : (Un:nat->R) (Un_decreasing Un) -> (Un_growing (opp_seq Un)). -Intro. -Unfold Un_growing opp_seq Un_decreasing. -Intros. -Apply Rle_Ropp1. -Apply H. -Qed. - -Lemma decreasing_cv : (Un:nat->R) (Un_decreasing Un) -> (has_lb Un) -> (sigTT R [l:R](Un_cv Un l)). -Intros. -Cut (sigTT R [l:R](Un_cv (opp_seq Un) l)) -> (sigTT R [l:R](Un_cv Un l)). -Intro. -Apply X. -Apply growing_cv. -Apply decreasing_growing; Assumption. -Exact H0. -Intro. -Elim X; Intros. -Apply existTT with ``-x``. -Unfold Un_cv in p. -Unfold R_dist in p. -Unfold opp_seq in p. -Unfold Un_cv. -Unfold R_dist. -Intros. -Elim (p eps H1); Intros. -Exists x0; Intros. -Assert H4 := (H2 n H3). -Rewrite <- Rabsolu_Ropp. -Replace ``-((Un n)- -x)`` with ``-(Un n)-x``; [Assumption | Ring]. -Qed. - -(***********) -Lemma maj_sup : (Un:nat->R) (has_ub Un) -> (sigTT R [l:R](is_lub (EUn Un) l)). -Intros. -Unfold has_ub in H. -Apply complet. -Assumption. -Exists (Un O). -Unfold EUn. -Exists O; Reflexivity. -Qed. - -(**********) -Lemma min_inf : (Un:nat->R) (has_lb Un) -> (sigTT R [l:R](is_lub (EUn (opp_seq Un)) l)). -Intros; Unfold has_lb in H. -Apply complet. -Assumption. -Exists ``-(Un O)``. -Exists O. -Reflexivity. -Qed. - -Definition majorant [Un:nat->R;pr:(has_ub Un)] : R := Cases (maj_sup Un pr) of (existTT a b) => a end. - -Definition minorant [Un:nat->R;pr:(has_lb Un)] : R := Cases (min_inf Un pr) of (existTT a b) => ``-a`` end. - -Lemma maj_ss : (Un:nat->R;k:nat) (has_ub Un) -> (has_ub [i:nat](Un (plus k i))). -Intros. -Unfold has_ub in H. -Unfold bound in H. -Elim H; Intros. -Unfold is_upper_bound in H0. -Unfold has_ub. -Exists x. -Unfold is_upper_bound. -Intros. -Apply H0. -Elim H1; Intros. -Exists (plus k x1); Assumption. -Qed. - -Lemma min_ss : (Un:nat->R;k:nat) (has_lb Un) -> (has_lb [i:nat](Un (plus k i))). -Intros. -Unfold has_lb in H. -Unfold bound in H. -Elim H; Intros. -Unfold is_upper_bound in H0. -Unfold has_lb. -Exists x. -Unfold is_upper_bound. -Intros. -Apply H0. -Elim H1; Intros. -Exists (plus k x1); Assumption. -Qed. - -Definition sequence_majorant [Un:nat->R;pr:(has_ub Un)] : nat -> R := [i:nat](majorant [k:nat](Un (plus i k)) (maj_ss Un i pr)). - -Definition sequence_minorant [Un:nat->R;pr:(has_lb Un)] : nat -> R := [i:nat](minorant [k:nat](Un (plus i k)) (min_ss Un i pr)). - -Lemma Wn_decreasing : (Un:nat->R;pr:(has_ub Un)) (Un_decreasing (sequence_majorant Un pr)). -Intros. -Unfold Un_decreasing. -Intro. -Unfold sequence_majorant. -Assert H := (maj_sup [k:nat](Un (plus (S n) k)) (maj_ss Un (S n) pr)). -Assert H0 := (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr)). -Elim H; Intros. -Elim H0; Intros. -Cut (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr)) == x; [Intro Maj1; Rewrite Maj1 | Idtac]. -Cut (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr)) == x0; [Intro Maj2; Rewrite Maj2 | Idtac]. -Unfold is_lub in p. -Unfold is_lub in p0. -Elim p; Intros. -Apply H2. -Elim p0; Intros. -Unfold is_upper_bound. -Intros. -Unfold is_upper_bound in H3. -Apply H3. -Elim H5; Intros. -Exists (plus (1) x2). -Replace (plus n (plus (S O) x2)) with (plus (S n) x2). -Assumption. -Replace (S n) with (plus (1) n); [Ring | Ring]. -Cut (is_lub (EUn [k:nat](Un (plus n k))) (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr))). -Intro. -Unfold is_lub in p0; Unfold is_lub in H1. -Elim p0; Intros; Elim H1; Intros. -Assert H6 := (H5 x0 H2). -Assert H7 := (H3 (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr)) H4). -Apply Rle_antisym; Assumption. -Unfold majorant. -Case (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr)). -Trivial. -Cut (is_lub (EUn [k:nat](Un (plus (S n) k))) (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr))). -Intro. -Unfold is_lub in p; Unfold is_lub in H1. -Elim p; Intros; Elim H1; Intros. -Assert H6 := (H5 x H2). -Assert H7 := (H3 (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr)) H4). -Apply Rle_antisym; Assumption. -Unfold majorant. -Case (maj_sup [k:nat](Un (plus (S n) k)) (maj_ss Un (S n) pr)). -Trivial. -Qed. - -Lemma Vn_growing : (Un:nat->R;pr:(has_lb Un)) (Un_growing (sequence_minorant Un pr)). -Intros. -Unfold Un_growing. -Intro. -Unfold sequence_minorant. -Assert H := (min_inf [k:nat](Un (plus (S n) k)) (min_ss Un (S n) pr)). -Assert H0 := (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr)). -Elim H; Intros. -Elim H0; Intros. -Cut (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr)) == ``-x``; [Intro Maj1; Rewrite Maj1 | Idtac]. -Cut (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr)) == ``-x0``; [Intro Maj2; Rewrite Maj2 | Idtac]. -Unfold is_lub in p. -Unfold is_lub in p0. -Elim p; Intros. -Apply Rle_Ropp1. -Apply H2. -Elim p0; Intros. -Unfold is_upper_bound. -Intros. -Unfold is_upper_bound in H3. -Apply H3. -Elim H5; Intros. -Exists (plus (1) x2). -Unfold opp_seq in H6. -Unfold opp_seq. -Replace (plus n (plus (S O) x2)) with (plus (S n) x2). -Assumption. -Replace (S n) with (plus (1) n); [Ring | Ring]. -Cut (is_lub (EUn (opp_seq [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr)))). -Intro. -Unfold is_lub in p0; Unfold is_lub in H1. -Elim p0; Intros; Elim H1; Intros. -Assert H6 := (H5 x0 H2). -Assert H7 := (H3 (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr))) H4). -Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr))). -Apply eq_Ropp; Apply Rle_antisym; Assumption. -Unfold minorant. -Case (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr)). -Intro; Rewrite Ropp_Ropp. -Trivial. -Cut (is_lub (EUn (opp_seq [k:nat](Un (plus (S n) k)))) (Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr)))). -Intro. -Unfold is_lub in p; Unfold is_lub in H1. -Elim p; Intros; Elim H1; Intros. -Assert H6 := (H5 x H2). -Assert H7 := (H3 (Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr))) H4). -Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr))). -Apply eq_Ropp; Apply Rle_antisym; Assumption. -Unfold minorant. -Case (min_inf [k:nat](Un (plus (S n) k)) (min_ss Un (S n) pr)). -Intro; Rewrite Ropp_Ropp. -Trivial. -Qed. - -(**********) -Lemma Vn_Un_Wn_order : (Un:nat->R;pr1:(has_ub Un);pr2:(has_lb Un)) (n:nat) ``((sequence_minorant Un pr2) n)<=(Un n)<=((sequence_majorant Un pr1) n)``. -Intros. -Split. -Unfold sequence_minorant. -Cut (sigTT R [l:R](is_lub (EUn (opp_seq [i:nat](Un (plus n i)))) l)). -Intro. -Elim X; Intros. -Replace (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2)) with ``-x``. -Unfold is_lub in p. -Elim p; Intros. -Unfold is_upper_bound in H. -Rewrite <- (Ropp_Ropp (Un n)). -Apply Rle_Ropp1. -Apply H. -Exists O. -Unfold opp_seq. -Replace (plus n O) with n; [Reflexivity | Ring]. -Cut (is_lub (EUn (opp_seq [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2)))). -Intro. -Unfold is_lub in p; Unfold is_lub in H. -Elim p; Intros; Elim H; Intros. -Assert H4 := (H3 x H0). -Assert H5 := (H1 (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2))) H2). -Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2))). -Apply eq_Ropp; Apply Rle_antisym; Assumption. -Unfold minorant. -Case (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr2)). -Intro; Rewrite Ropp_Ropp. -Trivial. -Apply min_inf. -Apply min_ss; Assumption. -Unfold sequence_majorant. -Cut (sigTT R [l:R](is_lub (EUn [i:nat](Un (plus n i))) l)). -Intro. -Elim X; Intros. -Replace (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1)) with ``x``. -Unfold is_lub in p. -Elim p; Intros. -Unfold is_upper_bound in H. -Apply H. -Exists O. -Replace (plus n O) with n; [Reflexivity | Ring]. -Cut (is_lub (EUn [k:nat](Un (plus n k))) (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1))). -Intro. -Unfold is_lub in p; Unfold is_lub in H. -Elim p; Intros; Elim H; Intros. -Assert H4 := (H3 x H0). -Assert H5 := (H1 (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1)) H2). -Apply Rle_antisym; Assumption. -Unfold majorant. -Case (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr1)). -Intro; Trivial. -Apply maj_sup. -Apply maj_ss; Assumption. -Qed. - -Lemma min_maj : (Un:nat->R;pr1:(has_ub Un);pr2:(has_lb Un)) (has_ub (sequence_minorant Un pr2)). -Intros. -Assert H := (Vn_Un_Wn_order Un pr1 pr2). -Unfold has_ub. -Unfold bound. -Unfold has_ub in pr1. -Unfold bound in pr1. -Elim pr1; Intros. -Exists x. -Unfold is_upper_bound. -Intros. -Unfold is_upper_bound in H0. -Elim H1; Intros. -Rewrite H2. -Apply Rle_trans with (Un x1). -Assert H3 := (H x1); Elim H3; Intros; Assumption. -Apply H0. -Exists x1; Reflexivity. -Qed. - -Lemma maj_min : (Un:nat->R;pr1:(has_ub Un);pr2:(has_lb Un)) (has_lb (sequence_majorant Un pr1)). -Intros. -Assert H := (Vn_Un_Wn_order Un pr1 pr2). -Unfold has_lb. -Unfold bound. -Unfold has_lb in pr2. -Unfold bound in pr2. -Elim pr2; Intros. -Exists x. -Unfold is_upper_bound. -Intros. -Unfold is_upper_bound in H0. -Elim H1; Intros. -Rewrite H2. -Apply Rle_trans with ((opp_seq Un) x1). -Assert H3 := (H x1); Elim H3; Intros. -Unfold opp_seq; Apply Rle_Ropp1. -Assumption. -Apply H0. -Exists x1; Reflexivity. -Qed. - -(**********) -Lemma cauchy_maj : (Un:nat->R) (Cauchy_crit Un) -> (has_ub Un). -Intros. -Unfold has_ub. -Apply cauchy_bound. -Assumption. -Qed. - -(**********) -Lemma cauchy_opp : (Un:nat->R) (Cauchy_crit Un) -> (Cauchy_crit (opp_seq Un)). -Intro. -Unfold Cauchy_crit. -Unfold R_dist. -Intros. -Elim (H eps H0); Intros. -Exists x; Intros. -Unfold opp_seq. -Rewrite <- Rabsolu_Ropp. -Replace ``-( -(Un n)- -(Un m))`` with ``(Un n)-(Un m)``; [Apply H1; Assumption | Ring]. -Qed. - -(**********) -Lemma cauchy_min : (Un:nat->R) (Cauchy_crit Un) -> (has_lb Un). -Intros. -Unfold has_lb. -Assert H0 := (cauchy_opp ? H). -Apply cauchy_bound. -Assumption. -Qed. - -(**********) -Lemma maj_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (sequence_majorant Un (cauchy_maj Un pr)) l)). -Intros. -Apply decreasing_cv. -Apply Wn_decreasing. -Apply maj_min. -Apply cauchy_min. -Assumption. -Qed. - -(**********) -Lemma min_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (sequence_minorant Un (cauchy_min Un pr)) l)). -Intros. -Apply growing_cv. -Apply Vn_growing. -Apply min_maj. -Apply cauchy_maj. -Assumption. -Qed. - -Lemma cond_eq : (x,y:R) ((eps:R)``0<eps``->``(Rabsolu (x-y))<eps``) -> x==y. -Intros. -Case (total_order_T x y); Intro. -Elim s; Intro. -Cut ``0<y-x``. -Intro. -Assert H1 := (H ``y-x`` H0). -Rewrite <- Rabsolu_Ropp in H1. -Cut ``-(x-y)==y-x``; [Intro; Rewrite H2 in H1 | Ring]. -Rewrite Rabsolu_right in H1. -Elim (Rlt_antirefl ? H1). -Left; Assumption. -Apply Rlt_anti_compatibility with x. -Rewrite Rplus_Or; Replace ``x+(y-x)`` with y; [Assumption | Ring]. -Assumption. -Cut ``0<x-y``. -Intro. -Assert H1 := (H ``x-y`` H0). -Rewrite Rabsolu_right in H1. -Elim (Rlt_antirefl ? H1). -Left; Assumption. -Apply Rlt_anti_compatibility with y. -Rewrite Rplus_Or; Replace ``y+(x-y)`` with x; [Assumption | Ring]. -Qed. - -Lemma not_Rlt : (r1,r2:R)~(``r1<r2``)->``r1>=r2``. -Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rge. -Tauto. -Qed. - -(**********) -Lemma approx_maj : (Un:nat->R;pr:(has_ub Un)) (eps:R) ``0<eps`` -> (EX k : nat | ``(Rabsolu ((majorant Un pr)-(Un k))) < eps``). -Intros. -Pose P := [k:nat]``(Rabsolu ((majorant Un pr)-(Un k))) < eps``. -Unfold P. -Cut (EX k:nat | (P k)) -> (EX k:nat | ``(Rabsolu ((majorant Un pr)-(Un k))) < eps``). -Intros. -Apply H0. -Apply not_all_not_ex. -Red; Intro. -2:Unfold P; Trivial. -Unfold P in H1. -Cut (n:nat)``(Rabsolu ((majorant Un pr)-(Un n))) >= eps``. -Intro. -Cut (is_lub (EUn Un) (majorant Un pr)). -Intro. -Unfold is_lub in H3. -Unfold is_upper_bound in H3. -Elim H3; Intros. -Cut (n:nat)``eps<=(majorant Un pr)-(Un n)``. -Intro. -Cut (n:nat)``(Un n)<=(majorant Un pr)-eps``. -Intro. -Cut ((x:R)(EUn Un x)->``x <= (majorant Un pr)-eps``). -Intro. -Assert H9 := (H5 ``(majorant Un pr)-eps`` H8). -Cut ``eps<=0``. -Intro. -Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H H10)). -Apply Rle_anti_compatibility with ``(majorant Un pr)-eps``. -Rewrite Rplus_Or. -Replace ``(majorant Un pr)-eps+eps`` with (majorant Un pr); [Assumption | Ring]. -Intros. -Unfold EUn in H8. -Elim H8; Intros. -Rewrite H9; Apply H7. -Intro. -Assert H7 := (H6 n). -Apply Rle_anti_compatibility with ``eps-(Un n)``. -Replace ``eps-(Un n)+(Un n)`` with ``eps``. -Replace ``eps-(Un n)+((majorant Un pr)-eps)`` with ``(majorant Un pr)-(Un n)``. -Assumption. -Ring. -Ring. -Intro. -Assert H6 := (H2 n). -Rewrite Rabsolu_right in H6. -Apply Rle_sym2. -Assumption. -Apply Rle_sym1. -Apply Rle_anti_compatibility with (Un n). -Rewrite Rplus_Or; Replace ``(Un n)+((majorant Un pr)-(Un n))`` with (majorant Un pr); [Apply H4 | Ring]. -Exists n; Reflexivity. -Unfold majorant. -Case (maj_sup Un pr). -Trivial. -Intro. -Assert H2 := (H1 n). -Apply not_Rlt; Assumption. -Qed. - -(**********) -Lemma approx_min : (Un:nat->R;pr:(has_lb Un)) (eps:R) ``0<eps`` -> (EX k :nat | ``(Rabsolu ((minorant Un pr)-(Un k))) < eps``). -Intros. -Pose P := [k:nat]``(Rabsolu ((minorant Un pr)-(Un k))) < eps``. -Unfold P. -Cut (EX k:nat | (P k)) -> (EX k:nat | ``(Rabsolu ((minorant Un pr)-(Un k))) < eps``). -Intros. -Apply H0. -Apply not_all_not_ex. -Red; Intro. -2:Unfold P; Trivial. -Unfold P in H1. -Cut (n:nat)``(Rabsolu ((minorant Un pr)-(Un n))) >= eps``. -Intro. -Cut (is_lub (EUn (opp_seq Un)) ``-(minorant Un pr)``). -Intro. -Unfold is_lub in H3. -Unfold is_upper_bound in H3. -Elim H3; Intros. -Cut (n:nat)``eps<=(Un n)-(minorant Un pr)``. -Intro. -Cut (n:nat)``((opp_seq Un) n)<=-(minorant Un pr)-eps``. -Intro. -Cut ((x:R)(EUn (opp_seq Un) x)->``x <= -(minorant Un pr)-eps``). -Intro. -Assert H9 := (H5 ``-(minorant Un pr)-eps`` H8). -Cut ``eps<=0``. -Intro. -Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H H10)). -Apply Rle_anti_compatibility with ``-(minorant Un pr)-eps``. -Rewrite Rplus_Or. -Replace ``-(minorant Un pr)-eps+eps`` with ``-(minorant Un pr)``; [Assumption | Ring]. -Intros. -Unfold EUn in H8. -Elim H8; Intros. -Rewrite H9; Apply H7. -Intro. -Assert H7 := (H6 n). -Unfold opp_seq. -Apply Rle_anti_compatibility with ``eps+(Un n)``. -Replace ``eps+(Un n)+ -(Un n)`` with ``eps``. -Replace ``eps+(Un n)+(-(minorant Un pr)-eps)`` with ``(Un n)-(minorant Un pr)``. -Assumption. -Ring. -Ring. -Intro. -Assert H6 := (H2 n). -Rewrite Rabsolu_left1 in H6. -Apply Rle_sym2. -Replace ``(Un n)-(minorant Un pr)`` with `` -((minorant Un pr)-(Un n))``; [Assumption | Ring]. -Apply Rle_anti_compatibility with ``-(minorant Un pr)``. -Rewrite Rplus_Or; Replace ``-(minorant Un pr)+((minorant Un pr)-(Un n))`` with ``-(Un n)``. -Apply H4. -Exists n; Reflexivity. -Ring. -Unfold minorant. -Case (min_inf Un pr). -Intro. -Rewrite Ropp_Ropp. -Trivial. -Intro. -Assert H2 := (H1 n). -Apply not_Rlt; Assumption. -Qed. - -(* Unicity of limit for convergent sequences *) -Lemma UL_sequence : (Un:nat->R;l1,l2:R) (Un_cv Un l1) -> (Un_cv Un l2) -> l1==l2. -Intros Un l1 l2; Unfold Un_cv; Unfold R_dist; Intros. -Apply cond_eq. -Intros; Cut ``0<eps/2``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. -Elim (H ``eps/2`` H2); Intros. -Elim (H0 ``eps/2`` H2); Intros. -Pose N := (max x x0). -Apply Rle_lt_trans with ``(Rabsolu (l1 -(Un N)))+(Rabsolu ((Un N)-l2))``. -Replace ``l1-l2`` with ``(l1-(Un N))+((Un N)-l2)``; [Apply Rabsolu_triang | Ring]. -Rewrite (double_var eps); Apply Rplus_lt. -Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H3; Unfold ge N; Apply le_max_l. -Apply H4; Unfold ge N; Apply le_max_r. -Qed. - -(**********) -Lemma CV_plus : (An,Bn:nat->R;l1,l2:R) (Un_cv An l1) -> (Un_cv Bn l2) -> (Un_cv [i:nat]``(An i)+(Bn i)`` ``l1+l2``). -Unfold Un_cv; Unfold R_dist; Intros. -Cut ``0<eps/2``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. -Elim (H ``eps/2`` H2); Intros. -Elim (H0 ``eps/2`` H2); Intros. -Pose N := (max x x0). -Exists N; Intros. -Replace ``(An n)+(Bn n)-(l1+l2)`` with ``((An n)-l1)+((Bn n)-l2)``; [Idtac | Ring]. -Apply Rle_lt_trans with ``(Rabsolu ((An n)-l1))+(Rabsolu ((Bn n)-l2))``. -Apply Rabsolu_triang. -Rewrite (double_var eps); Apply Rplus_lt. -Apply H3; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_l | Assumption]. -Apply H4; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_r | Assumption]. -Qed. - -(**********) -Lemma cv_cvabs : (Un:nat->R;l:R) (Un_cv Un l) -> (Un_cv [i:nat](Rabsolu (Un i)) (Rabsolu l)). -Unfold Un_cv; Unfold R_dist; Intros. -Elim (H eps H0); Intros. -Exists x; Intros. -Apply Rle_lt_trans with ``(Rabsolu ((Un n)-l))``. -Apply Rabsolu_triang_inv2. -Apply H1; Assumption. -Qed. - -(**********) -Lemma CV_Cauchy : (Un:nat->R) (sigTT R [l:R](Un_cv Un l)) -> (Cauchy_crit Un). -Intros; Elim X; Intros. -Unfold Cauchy_crit; Intros. -Unfold Un_cv in p; Unfold R_dist in p. -Cut ``0<eps/2``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. -Elim (p ``eps/2`` H0); Intros. -Exists x0; Intros. -Unfold R_dist; Apply Rle_lt_trans with ``(Rabsolu ((Un n)-x))+(Rabsolu (x-(Un m)))``. -Replace ``(Un n)-(Un m)`` with ``((Un n)-x)+(x-(Un m))``; [Apply Rabsolu_triang | Ring]. -Rewrite (double_var eps); Apply Rplus_lt. -Apply H1; Assumption. -Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H1; Assumption. -Qed. - -(**********) -Lemma maj_by_pos : (Un:nat->R) (sigTT R [l:R](Un_cv Un l)) -> (EXT l:R | ``0<l``/\((n:nat)``(Rabsolu (Un n))<=l``)). -Intros; Elim X; Intros. -Cut (sigTT R [l:R](Un_cv [k:nat](Rabsolu (Un k)) l)). -Intro. -Assert H := (CV_Cauchy [k:nat](Rabsolu (Un k)) X0). -Assert H0 := (cauchy_bound [k:nat](Rabsolu (Un k)) H). -Elim H0; Intros. -Exists ``x0+1``. -Cut ``0<=x0``. -Intro. -Split. -Apply ge0_plus_gt0_is_gt0; [Assumption | Apply Rlt_R0_R1]. -Intros. -Apply Rle_trans with x0. -Unfold is_upper_bound in H1. -Apply H1. -Exists n; Reflexivity. -Pattern 1 x0; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1. -Apply Rle_trans with (Rabsolu (Un O)). -Apply Rabsolu_pos. -Unfold is_upper_bound in H1. -Apply H1. -Exists O; Reflexivity. -Apply existTT with (Rabsolu x). -Apply cv_cvabs; Assumption. -Qed. - -(**********) -Lemma CV_mult : (An,Bn:nat->R;l1,l2:R) (Un_cv An l1) -> (Un_cv Bn l2) -> (Un_cv [i:nat]``(An i)*(Bn i)`` ``l1*l2``). -Intros. -Cut (sigTT R [l:R](Un_cv An l)). -Intro. -Assert H1 := (maj_by_pos An X). -Elim H1; Intros M H2. -Elim H2; Intros. -Unfold Un_cv; Unfold R_dist; Intros. -Cut ``0<eps/(2*M)``. -Intro. -Case (Req_EM l2 R0); Intro. -Unfold Un_cv in H0; Unfold R_dist in H0. -Elim (H0 ``eps/(2*M)`` H6); Intros. -Exists x; Intros. -Apply Rle_lt_trans with ``(Rabsolu ((An n)*(Bn n)-(An n)*l2))+(Rabsolu ((An n)*l2-l1*l2))``. -Replace ``(An n)*(Bn n)-l1*l2`` with ``((An n)*(Bn n)-(An n)*l2)+((An n)*l2-l1*l2)``; [Apply Rabsolu_triang | Ring]. -Replace ``(Rabsolu ((An n)*(Bn n)-(An n)*l2))`` with ``(Rabsolu (An n))*(Rabsolu ((Bn n)-l2))``. -Replace ``(Rabsolu ((An n)*l2-l1*l2))`` with R0. -Rewrite Rplus_Or. -Apply Rle_lt_trans with ``M*(Rabsolu ((Bn n)-l2))``. -Do 2 Rewrite <- (Rmult_sym ``(Rabsolu ((Bn n)-l2))``). -Apply Rle_monotony. -Apply Rabsolu_pos. -Apply H4. -Apply Rlt_monotony_contra with ``/M``. -Apply Rlt_Rinv; Apply H3. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite (Rmult_sym ``/M``). -Apply Rlt_trans with ``eps/(2*M)``. -Apply H8; Assumption. -Unfold Rdiv; Rewrite Rinv_Rmult. -Apply Rlt_monotony_contra with ``2``. -Sup0. -Replace ``2*(eps*(/2*/M))`` with ``(2*/2)*(eps*/M)``; [Idtac | Ring]. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l; Rewrite double. -Pattern 1 ``eps*/M``; Rewrite <- Rplus_Or. -Apply Rlt_compatibility; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Assumption]. -DiscrR. -DiscrR. -Red; Intro; Rewrite H10 in H3; Elim (Rlt_antirefl ? H3). -Red; Intro; Rewrite H10 in H3; Elim (Rlt_antirefl ? H3). -Rewrite H7; Do 2 Rewrite Rmult_Or; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Reflexivity. -Replace ``(An n)*(Bn n)-(An n)*l2`` with ``(An n)*((Bn n)-l2)``; [Idtac | Ring]. -Symmetry; Apply Rabsolu_mult. -Cut ``0<eps/(2*(Rabsolu l2))``. -Intro. -Unfold Un_cv in H; Unfold R_dist in H; Unfold Un_cv in H0; Unfold R_dist in H0. -Elim (H ``eps/(2*(Rabsolu l2))`` H8); Intros N1 H9. -Elim (H0 ``eps/(2*M)`` H6); Intros N2 H10. -Pose N := (max N1 N2). -Exists N; Intros. -Apply Rle_lt_trans with ``(Rabsolu ((An n)*(Bn n)-(An n)*l2))+(Rabsolu ((An n)*l2-l1*l2))``. -Replace ``(An n)*(Bn n)-l1*l2`` with ``((An n)*(Bn n)-(An n)*l2)+((An n)*l2-l1*l2)``; [Apply Rabsolu_triang | Ring]. -Replace ``(Rabsolu ((An n)*(Bn n)-(An n)*l2))`` with ``(Rabsolu (An n))*(Rabsolu ((Bn n)-l2))``. -Replace ``(Rabsolu ((An n)*l2-l1*l2))`` with ``(Rabsolu l2)*(Rabsolu ((An n)-l1))``. -Rewrite (double_var eps); Apply Rplus_lt. -Apply Rle_lt_trans with ``M*(Rabsolu ((Bn n)-l2))``. -Do 2 Rewrite <- (Rmult_sym ``(Rabsolu ((Bn n)-l2))``). -Apply Rle_monotony. -Apply Rabsolu_pos. -Apply H4. -Apply Rlt_monotony_contra with ``/M``. -Apply Rlt_Rinv; Apply H3. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Rewrite (Rmult_sym ``/M``). -Apply Rlt_le_trans with ``eps/(2*M)``. -Apply H10. -Unfold ge; Apply le_trans with N. -Unfold N; Apply le_max_r. -Assumption. -Unfold Rdiv; Rewrite Rinv_Rmult. -Right; Ring. -DiscrR. -Red; Intro; Rewrite H12 in H3; Elim (Rlt_antirefl ? H3). -Red; Intro; Rewrite H12 in H3; Elim (Rlt_antirefl ? H3). -Apply Rlt_monotony_contra with ``/(Rabsolu l2)``. -Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Apply Rlt_le_trans with ``eps/(2*(Rabsolu l2))``. -Apply H9. -Unfold ge; Apply le_trans with N. -Unfold N; Apply le_max_l. -Assumption. -Unfold Rdiv; Right; Rewrite Rinv_Rmult. -Ring. -DiscrR. -Apply Rabsolu_no_R0; Assumption. -Apply Rabsolu_no_R0; Assumption. -Replace ``(An n)*l2-l1*l2`` with ``l2*((An n)-l1)``; [Symmetry; Apply Rabsolu_mult | Ring]. -Replace ``(An n)*(Bn n)-(An n)*l2`` with ``(An n)*((Bn n)-l2)``; [Symmetry; Apply Rabsolu_mult | Ring]. -Unfold Rdiv; Apply Rmult_lt_pos. -Assumption. -Apply Rlt_Rinv; Apply Rmult_lt_pos; [Sup0 | Apply Rabsolu_pos_lt; Assumption]. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rmult_lt_pos; [Sup0 | Assumption]]. -Apply existTT with l1; Assumption. -Qed. - -Lemma tech9 : (Un:nat->R) (Un_growing Un) -> ((m,n:nat)(le m n)->``(Un m)<=(Un n)``). -Intros; Unfold Un_growing in H. -Induction n. -Induction m. -Right; Reflexivity. -Elim (le_Sn_O ? H0). -Cut (le m n)\/m=(S n). -Intro; Elim H1; Intro. -Apply Rle_trans with (Un n). -Apply Hrecn; Assumption. -Apply H. -Rewrite H2; Right; Reflexivity. -Inversion H0. -Right; Reflexivity. -Left; Assumption. -Qed. - -Lemma tech10 : (Un:nat->R;x:R) (Un_growing Un) -> (is_lub (EUn Un) x) -> (Un_cv Un x). -Intros; Cut (bound (EUn Un)). -Intro; Assert H2 := (Un_cv_crit ? H H1). -Elim H2; Intros. -Case (total_order_T x x0); Intro. -Elim s; Intro. -Cut (n:nat)``(Un n)<=x``. -Intro; Unfold Un_cv in H3; Cut ``0<x0-x``. -Intro; Elim (H3 ``x0-x`` H5); Intros. -Cut (ge x1 x1). -Intro; Assert H8 := (H6 x1 H7). -Unfold R_dist in H8; Rewrite Rabsolu_left1 in H8. -Rewrite Ropp_distr2 in H8; Unfold Rminus in H8. -Assert H9 := (Rlt_anti_compatibility ``x0`` ? ? H8). -Assert H10 := (Ropp_Rlt ? ? H9). -Assert H11 := (H4 x1). -Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H10 H11)). -Apply Rle_minus; Apply Rle_trans with x. -Apply H4. -Left; Assumption. -Unfold ge; Apply le_n. -Apply Rgt_minus; Assumption. -Intro; Unfold is_lub in H0; Unfold is_upper_bound in H0; Elim H0; Intros. -Apply H4; Unfold EUn; Exists n; Reflexivity. -Rewrite b; Assumption. -Cut ((n:nat)``(Un n)<=x0``). -Intro; Unfold is_lub in H0; Unfold is_upper_bound in H0; Elim H0; Intros. -Cut (y:R)(EUn Un y)->``y<=x0``. -Intro; Assert H8 := (H6 ? H7). -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H8 r)). -Unfold EUn; Intros; Elim H7; Intros. -Rewrite H8; Apply H4. -Intro; Case (total_order_Rle (Un n) x0); Intro. -Assumption. -Cut (n0:nat)(le n n0) -> ``x0<(Un n0)``. -Intro; Unfold Un_cv in H3; Cut ``0<(Un n)-x0``. -Intro; Elim (H3 ``(Un n)-x0`` H5); Intros. -Cut (ge (max n x1) x1). -Intro; Assert H8 := (H6 (max n x1) H7). -Unfold R_dist in H8. -Rewrite Rabsolu_right in H8. -Unfold Rminus in H8; Do 2 Rewrite <- (Rplus_sym ``-x0``) in H8. -Assert H9 := (Rlt_anti_compatibility ? ? ? H8). -Cut ``(Un n)<=(Un (max n x1))``. -Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H10 H9)). -Apply tech9; [Assumption | Apply le_max_l]. -Apply Rge_trans with ``(Un n)-x0``. -Unfold Rminus; Apply Rle_sym1; Do 2 Rewrite <- (Rplus_sym ``-x0``); Apply Rle_compatibility. -Apply tech9; [Assumption | Apply le_max_l]. -Left; Assumption. -Unfold ge; Apply le_max_r. -Apply Rlt_anti_compatibility with x0. -Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym x0); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H4; Apply le_n. -Intros; Apply Rlt_le_trans with (Un n). -Case (total_order_Rlt_Rle x0 (Un n)); Intro. -Assumption. -Elim n0; Assumption. -Apply tech9; Assumption. -Unfold bound; Exists x; Unfold is_lub in H0; Elim H0; Intros; Assumption. -Qed. - -Lemma tech13 : (An:nat->R;k:R) ``0<=k<1`` -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> (EXT k0 : R | ``k<k0<1`` /\ (EX N:nat | (n:nat) (le N n)->``(Rabsolu ((An (S n))/(An n)))<k0``)). -Intros; Exists ``k+(1-k)/2``. -Split. -Split. -Pattern 1 k; Rewrite <- Rplus_Or; Apply Rlt_compatibility. -Unfold Rdiv; Apply Rmult_lt_pos. -Apply Rlt_anti_compatibility with k; Rewrite Rplus_Or; Replace ``k+(1-k)`` with R1; [Elim H; Intros; Assumption | Ring]. -Apply Rlt_Rinv; Sup0. -Apply Rlt_monotony_contra with ``2``. -Sup0. -Unfold Rdiv; Rewrite Rmult_1r; Rewrite Rmult_Rplus_distr; Pattern 1 ``2``; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1r; Replace ``2*k+(1-k)`` with ``1+k``; [Idtac | Ring]. -Elim H; Intros. -Apply Rlt_compatibility; Assumption. -Unfold Un_cv in H0; Cut ``0<(1-k)/2``. -Intro; Elim (H0 ``(1-k)/2`` H1); Intros. -Exists x; Intros. -Assert H4 := (H2 n H3). -Unfold R_dist in H4; Rewrite <- Rabsolu_Rabsolu; Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``((Rabsolu ((An (S n))/(An n)))-k)+k``; [Idtac | Ring]; Apply Rle_lt_trans with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-k))+(Rabsolu k)``. -Apply Rabsolu_triang. -Rewrite (Rabsolu_right k). -Apply Rlt_anti_compatibility with ``-k``; Rewrite <- (Rplus_sym k); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Repeat Rewrite Rplus_Ol; Apply H4. -Apply Rle_sym1; Elim H; Intros; Assumption. -Unfold Rdiv; Apply Rmult_lt_pos. -Apply Rlt_anti_compatibility with k; Rewrite Rplus_Or; Elim H; Intros; Replace ``k+(1-k)`` with R1; [Assumption | Ring]. -Apply Rlt_Rinv; Sup0. -Qed. - -(**********) -Lemma growing_ineq : (Un:nat->R;l:R) (Un_growing Un) -> (Un_cv Un l) -> ((n:nat)``(Un n)<=l``). -Intros; Case (total_order_T (Un n) l); Intro. -Elim s; Intro. -Left; Assumption. -Right; Assumption. -Cut ``0<(Un n)-l``. -Intro; Unfold Un_cv in H0; Unfold R_dist in H0. -Elim (H0 ``(Un n)-l`` H1); Intros N1 H2. -Pose N := (max n N1). -Cut ``(Un n)-l<=(Un N)-l``. -Intro; Cut ``(Un N)-l<(Un n)-l``. -Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H3 H4)). -Apply Rle_lt_trans with ``(Rabsolu ((Un N)-l))``. -Apply Rle_Rabsolu. -Apply H2. -Unfold ge N; Apply le_max_r. -Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-l``); Apply Rle_compatibility. -Apply tech9. -Assumption. -Unfold N; Apply le_max_l. -Apply Rlt_anti_compatibility with l. -Rewrite Rplus_Or. -Replace ``l+((Un n)-l)`` with (Un n); [Assumption | Ring]. -Qed. - -(* Un->l => (-Un) -> (-l) *) -Lemma CV_opp : (An:nat->R;l:R) (Un_cv An l) -> (Un_cv (opp_seq An) ``-l``). -Intros An l. -Unfold Un_cv; Unfold R_dist; Intros. -Elim (H eps H0); Intros. -Exists x; Intros. -Unfold opp_seq; Replace ``-(An n)- (-l)`` with ``-((An n)-l)``; [Rewrite Rabsolu_Ropp | Ring]. -Apply H1; Assumption. -Qed. - -(**********) -Lemma decreasing_ineq : (Un:nat->R;l:R) (Un_decreasing Un) -> (Un_cv Un l) -> ((n:nat)``l<=(Un n)``). -Intros. -Assert H1 := (decreasing_growing ? H). -Assert H2 := (CV_opp ? ? H0). -Assert H3 := (growing_ineq ? ? H1 H2). -Apply Ropp_Rle. -Unfold opp_seq in H3; Apply H3. -Qed. - -(**********) -Lemma CV_minus : (An,Bn:nat->R;l1,l2:R) (Un_cv An l1) -> (Un_cv Bn l2) -> (Un_cv [i:nat]``(An i)-(Bn i)`` ``l1-l2``). -Intros. -Replace [i:nat]``(An i)-(Bn i)`` with [i:nat]``(An i)+((opp_seq Bn) i)``. -Unfold Rminus; Apply CV_plus. -Assumption. -Apply CV_opp; Assumption. -Unfold Rminus opp_seq; Reflexivity. -Qed. - -(* Un -> +oo *) -Definition cv_infty [Un:nat->R] : Prop := (M:R)(EXT N:nat | (n:nat) (le N n) -> ``M<(Un n)``). - -(* Un -> +oo => /Un -> O *) -Lemma cv_infty_cv_R0 : (Un:nat->R) ((n:nat)``(Un n)<>0``) -> (cv_infty Un) -> (Un_cv [n:nat]``/(Un n)`` R0). -Unfold cv_infty Un_cv; Unfold R_dist; Intros. -Elim (H0 ``/eps``); Intros N0 H2. -Exists N0; Intros. -Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite (Rabsolu_Rinv ? (H n)). -Apply Rlt_monotony_contra with (Rabsolu (Un n)). -Apply Rabsolu_pos_lt; Apply H. -Rewrite <- Rinv_r_sym. -Apply Rlt_monotony_contra with ``/eps``. -Apply Rlt_Rinv; Assumption. -Rewrite Rmult_1r; Rewrite (Rmult_sym ``/eps``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Apply Rlt_le_trans with (Un n). -Apply H2; Assumption. -Apply Rle_Rabsolu. -Red; Intro; Rewrite H4 in H1; Elim (Rlt_antirefl ? H1). -Apply Rabsolu_no_R0; Apply H. -Qed. - -(**********) -Lemma decreasing_prop : (Un:nat->R;m,n:nat) (Un_decreasing Un) -> (le m n) -> ``(Un n)<=(Un m)``. -Unfold Un_decreasing; Intros. -Induction n. -Induction m. -Right; Reflexivity. -Elim (le_Sn_O ? H0). -Cut (le m n)\/m=(S n). -Intro; Elim H1; Intro. -Apply Rle_trans with (Un n). -Apply H. -Apply Hrecn; Assumption. -Rewrite H2; Right; Reflexivity. -Inversion H0; [Right; Reflexivity | Left; Assumption]. -Qed. - -(* |x|^n/n! -> 0 *) -Lemma cv_speed_pow_fact : (x:R) (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` R0). -Intro; Cut (Un_cv [n:nat]``(pow (Rabsolu x) n)/(INR (fact n))`` R0) -> (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` ``0``). -Intro; Apply H. -Unfold Un_cv; Unfold R_dist; Intros; Case (Req_EM x R0); Intro. -Exists (S O); Intros. -Rewrite H1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_R0; Rewrite pow_ne_zero; [Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption | Red; Intro; Rewrite H3 in H2; Elim (le_Sn_n ? H2)]. -Assert H2 := (Rabsolu_pos_lt x H1); Pose M := (up (Rabsolu x)); Cut `0<=M`. -Intro; Elim (IZN M H3); Intros M_nat H4. -Pose Un := [n:nat]``(pow (Rabsolu x) (plus M_nat n))/(INR (fact (plus M_nat n)))``. -Cut (Un_cv Un R0); Unfold Un_cv; Unfold R_dist; Intros. -Elim (H5 eps H0); Intros N H6. -Exists (plus M_nat N); Intros; Cut (EX p:nat | (ge p N)/\n=(plus M_nat p)). -Intro; Elim H8; Intros p H9. -Elim H9; Intros; Rewrite H11; Unfold Un in H6; Apply H6; Assumption. -Exists (minus n M_nat). -Split. -Unfold ge; Apply simpl_le_plus_l with M_nat; Rewrite <- le_plus_minus. -Assumption. -Apply le_trans with (plus M_nat N). -Apply le_plus_l. -Assumption. -Apply le_plus_minus; Apply le_trans with (plus M_nat N); [Apply le_plus_l | Assumption]. -Pose Vn := [n:nat]``(Rabsolu x)*(Un O)/(INR (S n))``. -Cut (le (1) M_nat). -Intro; Cut (n:nat)``0<(Un n)``. -Intro; Cut (Un_decreasing Un). -Intro; Cut (n:nat)``(Un (S n))<=(Vn n)``. -Intro; Cut (Un_cv Vn R0). -Unfold Un_cv; Unfold R_dist; Intros. -Elim (H10 eps0 H5); Intros N1 H11. -Exists (S N1); Intros. -Cut (n:nat)``0<(Vn n)``. -Intro; Apply Rle_lt_trans with ``(Rabsolu ((Vn (pred n))-0))``. -Repeat Rewrite Rabsolu_right. -Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Replace n with (S (pred n)). -Apply H9. -Inversion H12; Simpl; Reflexivity. -Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H13. -Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H7. -Apply H11; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n; [Unfold ge in H12; Exact H12 | Inversion H12; Simpl; Reflexivity]. -Intro; Apply Rlt_le_trans with (Un (S n0)); [Apply H7 | Apply H9]. -Cut (cv_infty [n:nat](INR (S n))). -Intro; Cut (Un_cv [n:nat]``/(INR (S n))`` R0). -Unfold Un_cv R_dist; Intros; Unfold Vn. -Cut ``0<eps1/((Rabsolu x)*(Un O))``. -Intro; Elim (H11 ? H13); Intros N H14. -Exists N; Intros; Replace ``(Rabsolu x)*(Un O)/(INR (S n))-0`` with ``((Rabsolu x)*(Un O))*(/(INR (S n))-0)``; [Idtac | Unfold Rdiv; Ring]. -Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu ((Rabsolu x)*(Un O)))``. -Apply Rlt_Rinv; Apply Rabsolu_pos_lt. -Apply prod_neq_R0. -Apply Rabsolu_no_R0; Assumption. -Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16). -Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l. -Replace ``/(Rabsolu ((Rabsolu x)*(Un O)))*eps1`` with ``eps1/((Rabsolu x)*(Un O))``. -Apply H14; Assumption. -Unfold Rdiv; Rewrite (Rabsolu_right ``(Rabsolu x)*(Un O)``). -Apply Rmult_sym. -Apply Rle_sym1; Apply Rmult_le_pos. -Apply Rabsolu_pos. -Left; Apply H7. -Apply Rabsolu_no_R0. -Apply prod_neq_R0; [Apply Rabsolu_no_R0; Assumption | Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16)]. -Unfold Rdiv; Apply Rmult_lt_pos. -Assumption. -Apply Rlt_Rinv; Apply Rmult_lt_pos. -Apply Rabsolu_pos_lt; Assumption. -Apply H7. -Apply (cv_infty_cv_R0 [n:nat]``(INR (S n))``). -Intro; Apply not_O_INR; Discriminate. -Assumption. -Unfold cv_infty; Intro; Case (total_order_T M0 R0); Intro. -Elim s; Intro. -Exists O; Intros. -Apply Rlt_trans with R0; [Assumption | Apply lt_INR_0; Apply lt_O_Sn]. -Exists O; Intros; Rewrite b; Apply lt_INR_0; Apply lt_O_Sn. -Pose M0_z := (up M0). -Assert H10 := (archimed M0). -Cut `0<=M0_z`. -Intro; Elim (IZN ? H11); Intros M0_nat H12. -Exists M0_nat; Intros. -Apply Rlt_le_trans with (IZR M0_z). -Elim H10; Intros; Assumption. -Rewrite H12; Rewrite <- INR_IZR_INZ; Apply le_INR. -Apply le_trans with n; [Assumption | Apply le_n_Sn]. -Apply le_IZR; Left; Simpl; Unfold M0_z; Apply Rlt_trans with M0; [Assumption | Elim H10; Intros; Assumption]. -Intro; Apply Rle_trans with ``(Rabsolu x)*(Un n)*/(INR (S n))``. -Unfold Un; Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)). -Rewrite pow_add; Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring]. -Unfold Rdiv; Rewrite <- (Rmult_sym (Rabsolu x)); Repeat Rewrite Rmult_assoc; Repeat Apply Rle_monotony. -Apply Rabsolu_pos. -Left; Apply pow_lt; Assumption. -Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)). -Rewrite fact_simpl; Rewrite mult_sym; Rewrite mult_INR; Rewrite Rinv_Rmult. -Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H10 := (sym_eq ? ? ? H9); Elim (fact_neq_0 ? H10). -Left; Apply Rinv_lt. -Apply Rmult_lt_pos; Apply lt_INR_0; Apply lt_O_Sn. -Apply lt_INR; Apply lt_n_S. -Pattern 1 n; Replace n with (plus O n); [Idtac | Reflexivity]. -Apply lt_reg_r. -Apply lt_le_trans with (S O); [Apply lt_O_Sn | Assumption]. -Apply INR_fact_neq_0. -Apply not_O_INR; Discriminate. -Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity. -Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring. -Unfold Vn; Rewrite Rmult_assoc; Unfold Rdiv; Rewrite (Rmult_sym (Un O)); Rewrite (Rmult_sym (Un n)). -Repeat Apply Rle_monotony. -Apply Rabsolu_pos. -Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn. -Apply decreasing_prop; [Assumption | Apply le_O_n]. -Unfold Un_decreasing; Intro; Unfold Un. -Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)). -Rewrite pow_add; Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply pow_lt; Assumption. -Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring]. -Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)). -Apply Rle_monotony_contra with (INR (fact (S (plus M_nat n)))). -Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H9 := (sym_eq ? ? ? H8); Elim (fact_neq_0 ? H9). -Rewrite (Rmult_sym (Rabsolu x)); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l. -Rewrite fact_simpl; Rewrite mult_INR; Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Apply Rle_trans with (INR M_nat). -Left; Rewrite INR_IZR_INZ. -Rewrite <- H4; Assert H8 := (archimed (Rabsolu x)); Elim H8; Intros; Assumption. -Apply le_INR; Apply le_trans with (S M_nat); [Apply le_n_Sn | Apply le_n_S; Apply le_plus_l]. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity. -Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring. -Intro; Unfold Un; Unfold Rdiv; Apply Rmult_lt_pos. -Apply pow_lt; Assumption. -Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8). -Clear Un Vn; Apply INR_le; Simpl. -Induction M_nat. -Assert H6 := (archimed (Rabsolu x)); Fold M in H6; Elim H6; Intros. -Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7. -Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)). -Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n. -Apply le_IZR; Simpl; Left; Apply Rlt_trans with (Rabsolu x). -Assumption. -Elim (archimed (Rabsolu x)); Intros; Assumption. -Unfold Un_cv; Unfold R_dist; Intros; Elim (H eps H0); Intros. -Exists x0; Intros; Apply Rle_lt_trans with ``(Rabsolu ((pow (Rabsolu x) n)/(INR (fact n))-0))``. -Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Rewrite (Rabsolu_right ``(pow (Rabsolu x) n)/(INR (fact n))``). -Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``/(INR (fact n))``). -Rewrite Pow_Rabsolu; Right; Reflexivity. -Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4). -Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos. -Case (Req_EM x R0); Intro. -Rewrite H3; Rewrite Rabsolu_R0. -Induction n; [Simpl; Left; Apply Rlt_R0_R1 | Simpl; Rewrite Rmult_Ol; Right; Reflexivity]. -Left; Apply pow_lt; Apply Rabsolu_pos_lt; Assumption. -Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4). -Apply H1; Assumption. -Qed. |