diff options
Diffstat (limited to 'theories7/Reals/SeqProp.v')
| -rw-r--r-- | theories7/Reals/SeqProp.v | 1089 |
1 files changed, 1089 insertions, 0 deletions
diff --git a/theories7/Reals/SeqProp.v b/theories7/Reals/SeqProp.v new file mode 100644 index 00000000..b34fa339 --- /dev/null +++ b/theories7/Reals/SeqProp.v @@ -0,0 +1,1089 @@ +(************************************************************************) +(* 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. |