diff options
| -rw-r--r-- | theories/Reals/AltSeries.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Cos_plus.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Exp_prop.v | 6 | ||||
| -rw-r--r-- | theories/Reals/Rcomplete.v | 6 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 14 | ||||
| -rw-r--r-- | theories/Reals/Rsqrt_def.v | 12 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_reg.v | 6 | ||||
| -rw-r--r-- | theories/Reals/SeqProp.v | 167 | ||||
| -rw-r--r-- | theories/Reals/SeqSeries.v | 6 |
9 files changed, 106 insertions, 117 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index c5e1e0ba5..d9477c50d 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -97,8 +97,8 @@ Apply CV_ALT_step2; Assumption. Qed. (**********) -Lemma CV_ALT_step4 : (Un:nat->R) (Un_decreasing Un) -> (positivity_seq Un) -> (majoree [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N)))). -Intros; Unfold majoree; Unfold bound. +Lemma CV_ALT_step4 : (Un:nat->R) (Un_decreasing Un) -> (positivity_seq Un) -> (has_ub [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N)))). +Intros; Unfold has_ub; Unfold bound. Exists ``(Un O)``. Unfold is_upper_bound; Intros; Elim H1; Intros. Rewrite H2; Rewrite decomp_sum. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 15f68c1bb..9a4e04283 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -924,7 +924,7 @@ Intros. Cut (Un_cv (C1 x y) ``(cos x)*(cos y)-(sin x)*(sin y)``). Cut (Un_cv (C1 x y) ``(cos (x+y))``). Intros. -Apply UL_suite with (C1 x y); Assumption. +Apply UL_sequence with (C1 x y); Assumption. Apply C1_cvg. Unfold Un_cv; Unfold R_dist. Intros. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 750c0571f..61df2b49f 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -618,7 +618,7 @@ Lemma exp_plus : (x,y:R) ``(exp (x+y))==(exp x)*(exp y)``. Intros; Assert H0 := (E1_cvg x). Assert H := (E1_cvg y). Assert H1 := (E1_cvg ``x+y``). -EApply UL_suite. +EApply UL_sequence. Apply H1. Assert H2 := (CV_mult ? ? ? ? H0 H). Assert H3 := (CV_minus ? ? ? ? H2 (Reste_E_cv x y)). @@ -701,7 +701,7 @@ Apply (not_sym ? ? H6). Rewrite minus_R0; Apply H7. Unfold SFL. Case (cv ``0``); Intros. -EApply UL_suite. +EApply UL_sequence. Apply u. Unfold Un_cv SP. Intros; Exists (1); Intros. @@ -721,7 +721,7 @@ Apply lt_le_trans with (1); [Apply lt_n_Sn | Apply H9]. Unfold SFL exp. Unfold projT1. Case (cv h); Case (exist_exp h); Intros. -EApply UL_suite. +EApply UL_sequence. Apply u. Unfold Un_cv; Intros. Unfold exp_in in e. diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 8a653d1aa..0fff7c42a 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -24,8 +24,8 @@ Require Max. Theorem R_complete : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)). Intros. -Pose Vn := (suite_minorant Un (cauchy_min Un H)). -Pose Wn := (suite_majorant Un (cauchy_maj Un H)). +Pose Vn := (sequence_minorant Un (cauchy_min Un H)). +Pose Wn := (sequence_majorant Un (cauchy_maj Un H)). Assert H0 := (maj_cv Un H). Fold Wn in H0. Assert H1 := (min_cv Un H). @@ -126,7 +126,7 @@ Replace ``-(x-(Wn N))`` with ``(Wn N)-x``; [Apply H4 | Ring]. Unfold ge N. Apply le_trans with (max N1 N2); Apply le_max_l. Unfold Wn Vn. -Unfold suite_majorant suite_minorant. +Unfold sequence_majorant sequence_minorant. Assert H7 := (approx_maj [k:nat](Un (plus N k)) (maj_ss Un N (cauchy_maj Un H))). Assert H8 := (approx_min [k:nat](Un (plus N k)) (min_ss Un N (cauchy_min Un H))). Cut (Wn N)==(majorant ([k:nat](Un (plus N k))) (maj_ss Un N (cauchy_maj Un H))). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 116cc2e6f..aa43801a9 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -186,7 +186,7 @@ Definition RiemannInt [f:R->R;a,b:R;pr:(Riemann_integrable f a b)] : R := Cases (RiemannInt_exists pr 5!RinvN RinvN_cv) of (existTT a' b') => a' end. Lemma RiemannInt_P5 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable f a b)) (RiemannInt pr1)==(RiemannInt pr2). -Intros; Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; EApply UL_suite; [Apply u0 | Apply RiemannInt_P4 with pr2 RinvN; Apply RinvN_cv Orelse Assumption]. +Intros; Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; EApply UL_sequence; [Apply u0 | Apply RiemannInt_P4 with pr2 RinvN; Apply RinvN_cv Orelse Assumption]. Qed. (**************************************) @@ -395,7 +395,7 @@ Intros; Case (total_order_T a b); Intro; [Elim s; Intro; [Apply RiemannInt_P6; A Qed. Lemma RiemannInt_P8 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable f b a)) ``(RiemannInt pr1)==-(RiemannInt pr2)``. -Intros; EApply UL_suite. +Intros; EApply UL_sequence. Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; Apply u. Unfold RiemannInt; Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; Cut (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a b pr1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Cut (EXT psi2:nat->(StepFun b a) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f b a pr2 n) t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). @@ -595,8 +595,8 @@ Qed. Lemma RiemannInt_P12 : (f,g:R->R;a,b,l:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable g a b);pr3:(Riemann_integrable [x:R]``(f x)+l*(g x)`` a b)) ``a<=b`` -> ``(RiemannInt pr3)==(RiemannInt pr1)+l*(RiemannInt pr2)``. Intros; Case (Req_EM l R0); Intro. -Pattern 2 l; Rewrite H0; Rewrite Rmult_Ol; Rewrite Rplus_Or; Unfold RiemannInt; Case (RiemannInt_exists pr3 5!RinvN RinvN_cv); Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; EApply UL_suite; [Apply u0 | Pose psi1 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Pose psi2 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr3 n)); Apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; [Apply RinvN_cv | Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)) | Intro; Assert H1 : ((t:R) ``(Rmin a b) <= t``/\``t <= (Rmax a b)`` -> (Rle (Rabsolu (Rminus ``(f t)+l*(g t)`` (phi_sequence RinvN pr3 n t))) (psi2 n t))) /\ ``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``; [Apply (projT2 ? ? (phi_sequence_prop RinvN pr3 n)) | Elim H1; Intros; Split; Try Assumption; Intros; Replace (f t) with ``(f t)+l*(g t)``; [Apply H2; Assumption | Rewrite H0; Ring]] | Assumption]]. -EApply UL_suite. +Pattern 2 l; Rewrite H0; Rewrite Rmult_Ol; Rewrite Rplus_Or; Unfold RiemannInt; Case (RiemannInt_exists pr3 5!RinvN RinvN_cv); Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; EApply UL_sequence; [Apply u0 | Pose psi1 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Pose psi2 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr3 n)); Apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; [Apply RinvN_cv | Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)) | Intro; Assert H1 : ((t:R) ``(Rmin a b) <= t``/\``t <= (Rmax a b)`` -> (Rle (Rabsolu (Rminus ``(f t)+l*(g t)`` (phi_sequence RinvN pr3 n t))) (psi2 n t))) /\ ``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``; [Apply (projT2 ? ? (phi_sequence_prop RinvN pr3 n)) | Elim H1; Intros; Split; Try Assumption; Intros; Replace (f t) with ``(f t)+l*(g t)``; [Apply H2; Assumption | Rewrite H0; Ring]] | Assumption]]. +EApply UL_sequence. Unfold RiemannInt; Case (RiemannInt_exists pr3 5!RinvN RinvN_cv); Intros; Apply u. Unfold Un_cv; Intros; Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Unfold Un_cv; Intros; Assert H2 : ``0<eps/5``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. @@ -670,7 +670,7 @@ Unfold Riemann_integrable; Intros; Split with (mkStepFun (StepFun_P4 a b c)); Sp Qed. Lemma RiemannInt_P15 : (a,b,c:R;pr:(Riemann_integrable (fct_cte c) a b)) ``(RiemannInt pr)==c*(b-a)``. -Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!(fct_cte c) 2!a 3!b pr 5!RinvN RinvN_cv); Intros; EApply UL_suite. +Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!(fct_cte c) 2!a 3!b pr 5!RinvN RinvN_cv); Intros; EApply UL_sequence. Apply u. Pose phi1 := [N:nat](phi_sequence RinvN 2!(fct_cte c) 3!a 4!b pr N); Change (Un_cv [N:nat](RiemannInt_SF (phi1 N)) ``c*(b-a)``); Pose f := (fct_cte c); Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a b pr n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr n)). @@ -726,7 +726,7 @@ Elim H0; Clear H0; Intros psi3 H0; Elim H1; Clear H1; Intros psi2 H1; Apply Riem Qed. Lemma RiemannInt_P18 : (f,g:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable g a b)) ``a<=b`` -> ((x:R)``a<x<b``->``(f x)==(g x)``) -> ``(RiemannInt pr1)==(RiemannInt pr2)``. -Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!g 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; EApply UL_suite. +Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!g 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; EApply UL_sequence. Apply u0. Pose phi1 := [N:nat](phi_sequence RinvN 2!f 3!a 4!b pr1 N); Change (Un_cv [N:nat](RiemannInt_SF (phi1 N)) x); Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)). @@ -1109,7 +1109,7 @@ Apply RiemannInt_P1; Apply RiemannInt_P21 with b; Auto with real Orelse Apply Ri Qed. Lemma RiemannInt_P25 : (f:R->R;a,b,c:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable f b c);pr3:(Riemann_integrable f a c)) ``a<=b``->``b<=c``->``(RiemannInt pr1)+(RiemannInt pr2)==(RiemannInt pr3)``. -Intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!f 2!b 3!c pr2 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!f 2!a 3!c pr3 5!RinvN RinvN_cv); Intros; Symmetry; EApply UL_suite. +Intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!f 2!b 3!c pr2 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!f 2!a 3!c pr3 5!RinvN RinvN_cv); Intros; Symmetry; EApply UL_sequence. Apply u. Unfold Un_cv; Intros; Assert H0 : ``0<eps/3``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index ed939426f..8c63c9eb5 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -111,11 +111,11 @@ Assumption. Apply le_O_n. Qed. -Lemma dicho_lb_maj : (x,y:R;P:R->bool) ``x<=y`` -> (majoree (dicho_lb x y P)). +Lemma dicho_lb_maj : (x,y:R;P:R->bool) ``x<=y`` -> (has_ub (dicho_lb x y P)). Intros. Cut (n:nat)``(dicho_lb x y P n)<=y``. Intro. -Unfold majoree. +Unfold has_ub. Unfold bound. Exists y. Unfold is_upper_bound. @@ -145,18 +145,18 @@ Assumption. Assumption. Qed. -Lemma dicho_up_min : (x,y:R;P:R->bool) ``x<=y`` -> (minoree (dicho_up x y P)). +Lemma dicho_up_min : (x,y:R;P:R->bool) ``x<=y`` -> (has_lb (dicho_up x y P)). Intros. Cut (n:nat)``x<=(dicho_up x y P n)``. Intro. -Unfold minoree. +Unfold has_lb. Unfold bound. Exists ``-x``. Unfold is_upper_bound. Intros. Elim H1; Intros. Rewrite H2. -Unfold opp_sui. +Unfold opp_seq. Apply Rle_Ropp1. Apply H0. Apply dicho_up_min_x; Assumption. @@ -287,7 +287,7 @@ Intros. Assert H2 := (CV_minus ? ? ? ? H0 H1). Cut (Un_cv [i:nat]``(dicho_lb x y P i)-(dicho_up x y P i)`` R0). Intro. -Assert H4 := (UL_suite ? ? ? H2 H3). +Assert H4 := (UL_sequence ? ? ? H2 H3). Symmetry; Apply Rminus_eq_right; Assumption. Unfold Un_cv; Unfold R_dist. Intros. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 7694cf0a2..ac5c9ed20 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -114,7 +114,7 @@ Apply H4. Intros; Rewrite (H0 x); Rewrite (H0 x1); Apply H5; Apply H6. Intro; Unfold cos SFL. Case (cv x); Case (exist_cos (Rsqr x)); Intros. -Symmetry; EApply UL_suite. +Symmetry; EApply UL_sequence. Apply u. Unfold cos_in in c; Unfold infinit_sum in c; Unfold Un_cv; Intros. Elim (c ? H0); Intros N0 H1. @@ -259,7 +259,7 @@ Unfold SFL sin. Case (cv h); Intros. Case (exist_sin (Rsqr h)); Intros. Unfold Rdiv; Rewrite (Rinv_r_simpl_m h x0 H6). -EApply UL_suite. +EApply UL_sequence. Apply u. Unfold sin_in in s; Unfold sin_n infinit_sum in s; Unfold SP fn Un_cv; Intros. Elim (s ? H10); Intros N0 H11. @@ -270,7 +270,7 @@ Apply H11; Assumption. Apply sum_eq; Intros; Apply Rmult_mult_r; Unfold Rsqr; Rewrite pow_sqr; Reflexivity. Unfold SFL sin. Case (cv R0); Intros. -EApply UL_suite. +EApply UL_sequence. Apply u. Unfold SP fn; Unfold Un_cv; Intros; Exists (S O); Intros. Unfold R_dist; Replace (sum_f_R0 [k:nat]``(pow ( -1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))*(pow 0 (mult (S (S O)) k))`` n) with R1. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 6c9f709e5..6f489f37f 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -15,13 +15,12 @@ Require Classical. Require Max. Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)). -Definition opp_sui [Un:nat->R] : nat->R := [n:nat]``-(Un n)``. -Definition majoree [Un:nat->R] : Prop := (bound (EUn Un)). -Definition minoree [Un:nat->R] : Prop := (bound (EUn (opp_sui Un))). +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))). -(* Toute suite croissante et majoree converge *) -(* Preuve inspiree de celle presente dans Rseries *) -Lemma growing_cv : (Un:nat->R) (Un_growing Un) -> (majoree Un) -> (sigTT R [l:R](Un_cv Un l)). +(**********) +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; Generalize (complet (EUn Un) H0 (EUn_noempty Un));Intro H1. Elim H1;Clear H1;Intros;Split with x;Intros. @@ -60,19 +59,17 @@ Right;Auto. Apply (H2 (Un n) (Un_in_EUn Un n)). Qed. -(* Pour toute suite decroissante, la suite "opposee" est croissante *) -Lemma decreasing_growing : (Un:nat->R) (Un_decreasing Un) -> (Un_growing (opp_sui Un)). +Lemma decreasing_growing : (Un:nat->R) (Un_decreasing Un) -> (Un_growing (opp_seq Un)). Intro. -Unfold Un_growing opp_sui Un_decreasing. +Unfold Un_growing opp_seq Un_decreasing. Intros. Apply Rle_Ropp1. Apply H. Qed. -(* Toute suite decroissante et minoree converge *) -Lemma decreasing_cv : (Un:nat->R) (Un_decreasing Un) -> (minoree Un) -> (sigTT R [l:R](Un_cv Un l)). +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_sui Un) l)) -> (sigTT R [l:R](Un_cv Un l)). +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. @@ -83,7 +80,7 @@ Elim X; Intros. Apply existTT with ``-x``. Unfold Un_cv in p. Unfold R_dist in p. -Unfold opp_sui in p. +Unfold opp_seq in p. Unfold Un_cv. Unfold R_dist. Intros. @@ -95,9 +92,9 @@ Replace ``-((Un n)- -x)`` with ``-(Un n)-x``; [Assumption | Ring]. Qed. (***********) -Lemma maj_sup : (Un:nat->R) (majoree Un) -> (sigTT R [l:R](is_lub (EUn Un) l)). +Lemma maj_sup : (Un:nat->R) (has_ub Un) -> (sigTT R [l:R](is_lub (EUn Un) l)). Intros. -Unfold majoree in H. +Unfold has_ub in H. Apply complet. Assumption. Exists (Un O). @@ -106,8 +103,8 @@ Exists O; Reflexivity. Qed. (**********) -Lemma min_inf : (Un:nat->R) (minoree Un) -> (sigTT R [l:R](is_lub (EUn (opp_sui Un)) l)). -Intros; Unfold minoree in H. +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)``. @@ -115,18 +112,17 @@ Exists O. Reflexivity. Qed. -Definition majorant [Un:nat->R;pr:(majoree Un)] : R := Cases (maj_sup Un pr) of (existTT a b) => a end. +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:(minoree Un)] : R := Cases (min_inf 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. -(* Conservation de la propriete de majoration par extraction *) -Lemma maj_ss : (Un:nat->R;k:nat) (majoree Un) -> (majoree [i:nat](Un (plus k i))). +Lemma maj_ss : (Un:nat->R;k:nat) (has_ub Un) -> (has_ub [i:nat](Un (plus k i))). Intros. -Unfold majoree in H. +Unfold has_ub in H. Unfold bound in H. Elim H; Intros. Unfold is_upper_bound in H0. -Unfold majoree. +Unfold has_ub. Exists x. Unfold is_upper_bound. Intros. @@ -135,14 +131,13 @@ Elim H1; Intros. Exists (plus k x1); Assumption. Qed. -(* Conservation de la propriete de minoration par extraction *) -Lemma min_ss : (Un:nat->R;k:nat) (minoree Un) -> (minoree [i:nat](Un (plus k i))). +Lemma min_ss : (Un:nat->R;k:nat) (has_lb Un) -> (has_lb [i:nat](Un (plus k i))). Intros. -Unfold minoree in H. +Unfold has_lb in H. Unfold bound in H. Elim H; Intros. Unfold is_upper_bound in H0. -Unfold minoree. +Unfold has_lb. Exists x. Unfold is_upper_bound. Intros. @@ -151,16 +146,15 @@ Elim H1; Intros. Exists (plus k x1); Assumption. Qed. -Definition suite_majorant [Un:nat->R;pr:(majoree Un)] : nat -> R := [i:nat](majorant [k:nat](Un (plus i k)) (maj_ss Un i pr)). +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 suite_minorant [Un:nat->R;pr:(minoree Un)] : nat -> R := [i:nat](minorant [k:nat](Un (plus i k)) (min_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)). -(* La suite des majorants est decroissante *) -Lemma Wn_decreasing : (Un:nat->R;pr:(majoree Un)) (Un_decreasing (suite_majorant Un pr)). +Lemma Wn_decreasing : (Un:nat->R;pr:(has_ub Un)) (Un_decreasing (sequence_majorant Un pr)). Intros. Unfold Un_decreasing. Intro. -Unfold suite_majorant. +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. @@ -203,12 +197,11 @@ Case (maj_sup [k:nat](Un (plus (S n) k)) (maj_ss Un (S n) pr)). Trivial. Qed. -(* La suite des minorants est croissante *) -Lemma Vn_growing : (Un:nat->R;pr:(minoree Un)) (Un_growing (suite_minorant Un pr)). +Lemma Vn_growing : (Un:nat->R;pr:(has_lb Un)) (Un_growing (sequence_minorant Un pr)). Intros. Unfold Un_growing. Intro. -Unfold suite_minorant. +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. @@ -227,12 +220,12 @@ Unfold is_upper_bound in H3. Apply H3. Elim H5; Intros. Exists (plus (1) x2). -Unfold opp_sui in H6. -Unfold opp_sui. +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_sui [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr)))). +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. @@ -244,7 +237,7 @@ 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_sui [k:nat](Un (plus (S n) k)))) (Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr)))). +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. @@ -258,12 +251,12 @@ Intro; Rewrite Ropp_Ropp. Trivial. Qed. -(* Encadrement Vn,Un,Wn *) -Lemma Vn_Un_Wn_order : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (n:nat) ``((suite_minorant Un pr2) n)<=(Un n)<=((suite_majorant Un pr1) n)``. +(**********) +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 suite_minorant. -Cut (sigTT R [l:R](is_lub (EUn (opp_sui [i:nat](Un (plus n i)))) l)). +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``. @@ -274,9 +267,9 @@ Rewrite <- (Ropp_Ropp (Un n)). Apply Rle_Ropp1. Apply H. Exists O. -Unfold opp_sui. +Unfold opp_seq. Replace (plus n O) with n; [Reflexivity | Ring]. -Cut (is_lub (EUn (opp_sui [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2)))). +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. @@ -290,7 +283,7 @@ Intro; Rewrite Ropp_Ropp. Trivial. Apply min_inf. Apply min_ss; Assumption. -Unfold suite_majorant. +Unfold sequence_majorant. Cut (sigTT R [l:R](is_lub (EUn [i:nat](Un (plus n i))) l)). Intro. Elim X; Intros. @@ -315,13 +308,12 @@ Apply maj_sup. Apply maj_ss; Assumption. Qed. -(* La suite des minorants est majoree *) -Lemma min_maj : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (majoree (suite_minorant Un pr2)). +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 majoree. +Unfold has_ub. Unfold bound. -Unfold majoree in pr1. +Unfold has_ub in pr1. Unfold bound in pr1. Elim pr1; Intros. Exists x. @@ -336,13 +328,12 @@ Apply H0. Exists x1; Reflexivity. Qed. -(* La suite des majorants est minoree *) -Lemma maj_min : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (minoree (suite_majorant Un pr1)). +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 minoree. +Unfold has_lb. Unfold bound. -Unfold minoree in pr2. +Unfold has_lb in pr2. Unfold bound in pr2. Elim pr2; Intros. Exists x. @@ -351,46 +342,46 @@ Intros. Unfold is_upper_bound in H0. Elim H1; Intros. Rewrite H2. -Apply Rle_trans with ((opp_sui Un) x1). +Apply Rle_trans with ((opp_seq Un) x1). Assert H3 := (H x1); Elim H3; Intros. -Unfold opp_sui; Apply Rle_Ropp1. +Unfold opp_seq; Apply Rle_Ropp1. Assumption. Apply H0. Exists x1; Reflexivity. Qed. -(* Toute suite de Cauchy est majoree *) -Lemma cauchy_maj : (Un:nat->R) (Cauchy_crit Un) -> (majoree Un). +(**********) +Lemma cauchy_maj : (Un:nat->R) (Cauchy_crit Un) -> (has_ub Un). Intros. -Unfold majoree. +Unfold has_ub. Apply cauchy_bound. Assumption. Qed. (**********) -Lemma cauchy_opp : (Un:nat->R) (Cauchy_crit Un) -> (Cauchy_crit (opp_sui Un)). +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_sui. +Unfold opp_seq. Rewrite <- Rabsolu_Ropp. Replace ``-( -(Un n)- -(Un m))`` with ``(Un n)-(Un m)``; [Apply H1; Assumption | Ring]. Qed. -(* Toute suite de Cauchy est minoree *) -Lemma cauchy_min : (Un:nat->R) (Cauchy_crit Un) -> (minoree Un). +(**********) +Lemma cauchy_min : (Un:nat->R) (Cauchy_crit Un) -> (has_lb Un). Intros. -Unfold minoree. +Unfold has_lb. Assert H0 := (cauchy_opp ? H). Apply cauchy_bound. Assumption. Qed. -(* La suite des majorants converge *) -Lemma maj_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (suite_majorant Un (cauchy_maj Un pr)) l)). +(**********) +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. @@ -399,8 +390,8 @@ Apply cauchy_min. Assumption. Qed. -(* La suite des minorants converge *) -Lemma min_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (suite_minorant Un (cauchy_min Un pr)) l)). +(**********) +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. @@ -409,7 +400,6 @@ 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. @@ -435,14 +425,13 @@ 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. -(* On peut approcher la borne sup de toute suite majoree *) -Lemma approx_maj : (Un:nat->R;pr:(majoree Un)) (eps:R) ``0<eps`` -> (EX k : nat | ``(Rabsolu ((majorant Un pr)-(Un k))) < eps``). +(**********) +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. @@ -502,8 +491,8 @@ Assert H2 := (H1 n). Apply not_Rlt; Assumption. Qed. -(* On peut approcher la borne inf de toute suite minoree *) -Lemma approx_min : (Un:nat->R;pr:(minoree Un)) (eps:R) ``0<eps`` -> (EX k :nat | ``(Rabsolu ((minorant Un pr)-(Un k))) < eps``). +(**********) +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. @@ -516,16 +505,16 @@ Red; Intro. Unfold P in H1. Cut (n:nat)``(Rabsolu ((minorant Un pr)-(Un n))) >= eps``. Intro. -Cut (is_lub (EUn (opp_sui Un)) ``-(minorant Un pr)``). +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_sui Un) n)<=-(minorant Un pr)-eps``. +Cut (n:nat)``((opp_seq Un) n)<=-(minorant Un pr)-eps``. Intro. -Cut ((x:R)(EUn (opp_sui Un) x)->``x <= -(minorant Un pr)-eps``). +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``. @@ -540,7 +529,7 @@ Elim H8; Intros. Rewrite H9; Apply H7. Intro. Assert H7 := (H6 n). -Unfold opp_sui. +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)``. @@ -567,8 +556,8 @@ Assert H2 := (H1 n). Apply not_Rlt; Assumption. Qed. -(* Unicité de la limite pour les suites convergentes *) -Lemma UL_suite : (Un:nat->R;l1,l2:R) (Un_cv Un l1) -> (Un_cv Un l2) -> l1==l2. +(* 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]]. @@ -582,7 +571,7 @@ Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H3; Unfold ge N; Apply le_ma Apply H4; Unfold ge N; Apply le_max_r. Qed. -(* La limite de la somme de deux suites convergentes est la somme des limites *) +(**********) 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]]. @@ -598,7 +587,7 @@ Apply H3; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_l | Assumpti Apply H4; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_r | Assumption]. Qed. -(* Lien convergence / convergence absolue *) +(**********) 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. @@ -608,7 +597,7 @@ Apply Rabsolu_triang_inv2. Apply H1; Assumption. Qed. -(* Toute suite convergente est de Cauchy *) +(**********) 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. @@ -651,7 +640,7 @@ Apply existTT with (Rabsolu x). Apply cv_cvabs; Assumption. Qed. -(* La limite du produit de deux suites convergentes est le produit des limites *) +(**********) 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)). @@ -882,12 +871,12 @@ 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_sui An) ``-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_sui; Replace ``-(An n)- (-l)`` with ``-((An n)-l)``; [Rewrite Rabsolu_Ropp | Ring]. +Unfold opp_seq; Replace ``-(An n)- (-l)`` with ``-((An n)-l)``; [Rewrite Rabsolu_Ropp | Ring]. Apply H1; Assumption. Qed. @@ -898,17 +887,17 @@ Assert H1 := (decreasing_growing ? H). Assert H2 := (CV_opp ? ? H0). Assert H3 := (growing_ineq ? ? H1 H2). Apply Ropp_Rle. -Unfold opp_sui in H3; Apply H3. +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_sui Bn) i)``. +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_sui; Reflexivity. +Unfold Rminus opp_seq; Reflexivity. Qed. (* Un -> +oo *) diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 421d6576e..bd818a0ba 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -34,7 +34,7 @@ Apply sum_cv_maj with [l:nat](An (plus (S N) l)) [l:nat][x:R](fn (plus (S N) l) Unfold SP; Apply H2. Apply H3. Intros; Apply H1. -Symmetry; EApply UL_suite. +Symmetry; EApply UL_sequence. Apply H3. Unfold Un_cv in H0; Unfold Un_cv; Intros; Elim (H0 eps H5); Intros N0 H6. Unfold R_dist in H6; Exists N0; Intros. @@ -64,7 +64,7 @@ Apply sum_eq; Intros. Reflexivity. Apply le_lt_n_Sm; Apply le_plus_l. Apply le_O_n. -Symmetry; EApply UL_suite. +Symmetry; EApply UL_sequence. Apply H2. Unfold Un_cv in H; Unfold Un_cv; Intros. Elim (H eps H4); Intros N0 H5. @@ -162,7 +162,7 @@ Apply le_plus_l. Apply le_O_n. Qed. -(* Théorème de comparaison de convergence pour les séries *) +(* Comparaison of convergence for series *) Lemma Rseries_CV_comp : (An,Bn:nat->R) ((n:nat)``0<=(An n)<=(Bn n)``) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 Bn N) l)) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). Intros; Apply cv_cauchy_2. Assert H0 := (cv_cauchy_1 ? X). |