diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
commit | bcc5b59c086d1c06a1ec03ee0bff7647338bb258 (patch) | |
tree | 4f332b460941cdbb211806659b1fe76253f2fc67 /theories/Reals/Alembert.v | |
parent | 35cd1baf98895aa07d300d22c9e8148c91b43dac (diff) |
Réorganisation de la librairie des réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Alembert.v')
-rw-r--r-- | theories/Reals/Alembert.v | 456 |
1 files changed, 202 insertions, 254 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 0424b55f8..d3414317a 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -8,240 +8,12 @@ (*i $Id$ i*) - -Require Max. -Require Raxioms. -Require DiscrR. -Require Rbase. +Require RealsB. +Require Rfunctions. Require Rseries. -Require Rtrigo_fun. - -(*********************) -(* Lemmes techniques *) -(*********************) - -Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. -Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. -Qed. - -Lemma Rgt_2_0 : ``0<2``. -Sup0. -Qed. - -Lemma Rgt_3_0 : ``0<3``. -Sup0. -Qed. - -Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. -Intros; Induction N. -Simpl; Apply H; Apply le_n. -Simpl; Apply gt0_plus_gt0_is_gt0. -Apply HrecN; Intros; Apply H; Apply le_S; Assumption. -Apply H; Apply le_n. -Qed. - -(* Relation de Chasles *) -Lemma tech2 : (An:nat->R;m,n:nat) (lt m n) -> (sum_f_R0 An n) == (Rplus (sum_f_R0 An m) (sum_f_R0 [i:nat]``(An (plus (S m) i))`` (minus n (S m)))). -Intros; Induction n. -Elim (lt_n_O ? H). -Cut (lt m n)\/m=n. -Intro; Elim H0; Intro. -Replace (sum_f_R0 An (S n)) with ``(sum_f_R0 An n)+(An (S n))``; [Idtac | Reflexivity]. -Replace (minus (S n) (S m)) with (S (minus n (S m))). -Replace (sum_f_R0 [i:nat](An (plus (S m) i)) (S (minus n (S m)))) with (Rplus (sum_f_R0 [i:nat](An (plus (S m) i)) (minus n (S m))) (An (plus (S m) (S (minus n (S m)))))); [Idtac | Reflexivity]. -Replace (plus (S m) (S (minus n (S m)))) with (S n). -Rewrite (Hrecn H1). -Ring. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite minus_INR. -Rewrite S_INR; Ring. -Apply lt_le_S; Assumption. -Apply INR_eq; Rewrite S_INR; Repeat Rewrite minus_INR. -Repeat Rewrite S_INR; Ring. -Apply le_n_S; Apply lt_le_weak; Assumption. -Apply lt_le_S; Assumption. -Rewrite H1; Rewrite <- minus_n_n; Simpl. -Replace (plus n O) with n; [Reflexivity | Ring]. -Inversion H. -Right; Reflexivity. -Left; Apply lt_le_trans with (S m); [Apply lt_n_Sn | Assumption]. -Qed. - -(* Somme d'une suite géométrique *) -Lemma tech3 : (k:R;N:nat) ``k<>1`` -> (sum_f_R0 [i:nat](pow k i) N)==``(1-(pow k (S N)))/(1-k)``. -Intros; Cut ``1-k<>0``. -Intro; Induction N. -Simpl; Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rinv_r_sym. -Reflexivity. -Apply H0. -Replace (sum_f_R0 ([i:nat](pow k i)) (S N)) with (Rplus (sum_f_R0 [i:nat](pow k i) N) (pow k (S N))); [Idtac | Reflexivity]; Rewrite HrecN; Replace ``(1-(pow k (S N)))/(1-k)+(pow k (S N))`` with ``((1-(pow k (S N)))+(1-k)*(pow k (S N)))/(1-k)``. -Apply r_Rmult_mult with ``1-k``. -Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(1-k)``); Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [ Do 2 Rewrite Rmult_1l; Simpl; Ring | Apply H0]. -Apply H0. -Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Rewrite (Rmult_sym ``1-k``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Reflexivity. -Apply H0. -Apply Rminus_eq_contra; Red; Intro; Elim H; Symmetry; Assumption. -Qed. - -Lemma tech4 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> ``(An N)<=(An O)*(pow k N)``. -Intros; Induction N. -Simpl; Right; Ring. -Apply Rle_trans with ``k*(An N)``. -Left; Apply (H0 N). -Replace (S N) with (plus N (1)); [Idtac | Ring]. -Rewrite pow_add; Simpl; Rewrite Rmult_1r; Replace ``(An O)*((pow k N)*k)`` with ``k*((An O)*(pow k N))``; [Idtac | Ring]; Apply Rle_monotony. -Assumption. -Apply HrecN. -Qed. - -Lemma tech5 : (An:nat->R;N:nat) (sum_f_R0 An (S N))==``(sum_f_R0 An N)+(An (S N))``. -Intros; Reflexivity. -Qed. - -Lemma tech6 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> (Rle (sum_f_R0 An N) (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N))). -Intros; Induction N. -Simpl; Right; Ring. -Apply Rle_trans with (Rplus (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N)) (An (S N))). -Rewrite tech5; Do 2 Rewrite <- (Rplus_sym (An (S N))); Apply Rle_compatibility. -Apply HrecN. -Rewrite tech5 ; Rewrite Rmult_Rplus_distr; Apply Rle_compatibility. -Apply tech4; Assumption. -Qed. - -Lemma tech7 : (r1,r2:R) ``r1<>0`` -> ``r2<>0`` -> ``r1<>r2`` -> ``/r1<>/r2``. -Intros; Red; Intro. -Assert H3 := (Rmult_mult_r r1 ? ? H2). -Rewrite <- Rinv_r_sym in H3; [Idtac | Assumption]. -Assert H4 := (Rmult_mult_r r2 ? ? H3). -Rewrite Rmult_1r in H4; Rewrite <- Rmult_assoc in H4. -Rewrite Rinv_r_simpl_m in H4; [Idtac | Assumption]. -Elim H1; Symmetry; Assumption. -Qed. - -Lemma tech8 : (n,i:nat) (le n (plus (S n) i)). -Intros; Induction i. -Replace (plus (S n) O) with (S n); [Apply le_n_Sn | Ring]. -Replace (plus (S n) (S i)) with (S (plus (S n) i)). -Apply le_S; Assumption. -Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring. -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 tech11 : (An,Bn,Cn:nat->R;N:nat) ((i:nat) (An i)==``(Bn i)-(Cn i)``) -> (sum_f_R0 An N)==``(sum_f_R0 Bn N)-(sum_f_R0 Cn N)``. -Intros; Induction N. -Simpl; Apply H. -Do 3 Rewrite tech5; Rewrite HrecN; Rewrite (H (S N)); Ring. -Qed. - -Lemma tech12 : (An:nat->R;x:R;l:R) (Un_cv [N:nat](sum_f_R0 [i:nat]``(An i)*(pow x i)`` N) l) -> (Pser An x l). -Intros; Unfold Pser; Unfold infinit_sum; Unfold Un_cv in H; 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; Apply Rgt_2_0. -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -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; Apply Rgt_2_0. -Qed. - -Definition SigT := Specif.sigT. +Require SeqProp. +Require PartSum. +Require Max. (*************************************************) (* Différentes versions du critère de D'Alembert *) @@ -252,7 +24,7 @@ Intros An H H0. Cut (sigTT R [l:R](is_lub (EUn [N:nat](sum_f_R0 An N)) l)) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). Intro; Apply X. Apply complet. -Unfold Un_cv in H0; Unfold bound; Cut ``0</2``; [Intro | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Un_cv in H0; Unfold bound; Cut ``0</2``; [Intro | Apply Rlt_Rinv; Sup0]. Elim (H0 ``/2`` H1); Intros. Exists ``(sum_f_R0 An x)+2*(An (S x))``. Unfold is_upper_bound; Intros; Unfold EUn in H3; Elim H3; Intros. @@ -263,10 +35,10 @@ Replace (sum_f_R0 An x) with (Rplus (sum_f_R0 An x1) (sum_f_R0 [i:nat](An (plus Pattern 1 (sum_f_R0 An x1); Rewrite <- Rplus_Or; Rewrite Rplus_assoc; Apply Rle_compatibility. Left; Apply gt0_plus_gt0_is_gt0. Apply tech1; Intros; Apply H. -Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply H]. +Apply Rmult_lt_pos; [Sup0 | Apply H]. Symmetry; Apply tech2; Assumption. Rewrite b; Pattern 1 (sum_f_R0 An x); Rewrite <- Rplus_Or; Apply Rle_compatibility. -Left; Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply H]. +Left; Apply Rmult_lt_pos; [Sup0 | Apply H]. Replace (sum_f_R0 An x1) with (Rplus (sum_f_R0 An x) (sum_f_R0 [i:nat](An (plus (S x) i)) (minus x1 (S x)))). Apply Rle_compatibility. Cut (Rle (sum_f_R0 [i:nat](An (plus (S x) i)) (minus x1 (S x))) (Rmult (An (S x)) (sum_f_R0 [i:nat](pow ``/2`` i) (minus x1 (S x))))). @@ -278,11 +50,11 @@ Rewrite tech3. Replace ``1-/2`` with ``/2``. Unfold Rdiv; Rewrite Rinv_Rinv. Pattern 3 ``2``; Rewrite <- Rmult_1r; Rewrite <- (Rmult_sym ``2``); Apply Rle_monotony. -Left; Apply Rgt_2_0. +Left; Sup0. Left; Apply Rlt_anti_compatibility with ``(pow (/2) (S (minus x1 (S x))))``. Replace ``(pow (/2) (S (minus x1 (S x))))+(1-(pow (/2) (S (minus x1 (S x)))))`` with R1; [Idtac | Ring]. Rewrite <- (Rplus_sym ``1``); Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rlt_compatibility. -Apply pow_lt; Apply Rlt_Rinv; Apply Rgt_2_0. +Apply pow_lt; Apply Rlt_Rinv; Sup0. DiscrR. Apply r_Rmult_mult with ``2``. Rewrite Rminus_distr; Rewrite <- Rinv_r_sym. @@ -292,7 +64,7 @@ DiscrR. Pattern 3 R1; Replace R1 with ``/1``; [Apply tech7; DiscrR | Apply Rinv_R1]. Replace (An (S x)) with (An (plus (S x) O)). Apply (tech6 [i:nat](An (plus (S x) i)) ``/2``). -Left; Apply Rlt_Rinv; Apply Rgt_2_0. +Left; Apply Rlt_Rinv; Sup0. Intro; Cut (n:nat)(ge n x)->``(An (S n))</2*(An n)``. Intro; Replace (plus (S x) (S i)) with (S (plus (S x) i)). Apply H6; Unfold ge; Apply tech8. @@ -342,7 +114,7 @@ Rewrite Rminus_distr; Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. Ring. DiscrR. DiscrR. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. Cut (n:nat)``/2*(Rabsolu (An n))<=(Wn n)<=(3*/2)*(Rabsolu (An n))``. Intro; Cut (n:nat)``/(Wn n)<=2*/(Rabsolu (An n))``. Intro; Cut (n:nat)``(Wn (S n))/(Wn n)<=3*(Rabsolu (An (S n))/(An n))``. @@ -354,12 +126,12 @@ Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_ Apply Rle_lt_trans with ``3*(Rabsolu ((An (S n))/(An n)))``. Apply H6. Apply Rlt_monotony_contra with ``/3``. -Apply Rlt_Rinv; Apply Rgt_3_0. +Apply Rlt_Rinv; Sup0. Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H11; Exact H11. Left; Change ``0<(Wn (S n))/(Wn n)``; Unfold Rdiv; Apply Rmult_lt_pos. Apply H2. Apply Rlt_Rinv; Apply H2. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_3_0]. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. Intro; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite <- Rmult_assoc; Replace ``3`` with ``2*(3*/2)``; [Idtac | Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR]; Apply Rle_trans with ``(Wn (S n))*2*/(Rabsolu (An n))``. Rewrite Rmult_assoc; Apply Rle_monotony. Left; Apply H2. @@ -367,7 +139,7 @@ Apply H5. Rewrite Rabsolu_Rinv. Replace ``(Wn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Wn (S n))``; [Idtac | Ring]; Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring]; Apply Rle_monotony. Left; Apply Rmult_lt_pos. -Apply Rgt_2_0. +Sup0. Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H. Elim (H4 (S n)); Intros; Assumption. Apply H. @@ -378,7 +150,7 @@ Apply Rle_monotony_contra with (Rabsolu (An n)). Apply Rabsolu_pos_lt; Apply H. Rewrite Rmult_1r; Replace ``(Rabsolu (An n))*((Wn n)*(2*/(Rabsolu (An n))))`` with ``2*(Wn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring]; Rewrite <- Rinv_r_sym. Rewrite Rmult_1r; Apply Rle_monotony_contra with ``/2``. -Apply Rlt_Rinv; Apply Rgt_2_0. +Apply Rlt_Rinv; Sup0. Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1l; Elim (H4 n); Intros; Assumption. DiscrR. @@ -386,12 +158,12 @@ Apply Rabsolu_no_R0; Apply H. Red; Intro; Assert H6 := (H2 n); Rewrite H5 in H6; Elim (Rlt_antirefl ? H6). Intro; Split. Unfold Wn; Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rgt_2_0. +Left; Apply Rlt_Rinv; Sup0. Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Rewrite double; Unfold Rminus; Rewrite Rplus_assoc; Apply Rle_compatibility. Apply Rle_anti_compatibility with (An n). Rewrite Rplus_Or; Rewrite (Rplus_sym (An n)); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rle_Rabsolu. Unfold Wn; Unfold Rdiv; Repeat Rewrite <- (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rgt_2_0. +Left; Apply Rlt_Rinv; Sup0. Unfold Rminus; Rewrite double; Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring]; Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility. Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu. Cut (n:nat)``/2*(Rabsolu (An n))<=(Vn n)<=(3*/2)*(Rabsolu (An n))``. @@ -405,12 +177,12 @@ Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_ Apply Rle_lt_trans with ``3*(Rabsolu ((An (S n))/(An n)))``. Apply H5. Apply Rlt_monotony_contra with ``/3``. -Apply Rlt_Rinv; Apply Rgt_3_0. +Apply Rlt_Rinv; Sup0. Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H10; Exact H10. Left; Change ``0<(Vn (S n))/(Vn n)``; Unfold Rdiv; Apply Rmult_lt_pos. Apply H1. Apply Rlt_Rinv; Apply H1. -Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_3_0]. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. Intro; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite <- Rmult_assoc; Replace ``3`` with ``2*(3*/2)``; [Idtac | Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR]; Apply Rle_trans with ``(Vn (S n))*2*/(Rabsolu (An n))``. Rewrite Rmult_assoc; Apply Rle_monotony. Left; Apply H1. @@ -418,7 +190,7 @@ Apply H4. Rewrite Rabsolu_Rinv. Replace ``(Vn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Vn (S n))``; [Idtac | Ring]; Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring]; Apply Rle_monotony. Left; Apply Rmult_lt_pos. -Apply Rgt_2_0. +Sup0. Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H. Elim (H3 (S n)); Intros; Assumption. Apply H. @@ -429,7 +201,7 @@ Apply Rle_monotony_contra with (Rabsolu (An n)). Apply Rabsolu_pos_lt; Apply H. Rewrite Rmult_1r; Replace ``(Rabsolu (An n))*((Vn n)*(2*/(Rabsolu (An n))))`` with ``2*(Vn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring]; Rewrite <- Rinv_r_sym. Rewrite Rmult_1r; Apply Rle_monotony_contra with ``/2``. -Apply Rlt_Rinv; Apply Rgt_2_0. +Apply Rlt_Rinv; Sup0. Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1l; Elim (H3 n); Intros; Assumption. DiscrR. @@ -437,19 +209,19 @@ Apply Rabsolu_no_R0; Apply H. Red; Intro; Assert H5 := (H1 n); Rewrite H4 in H5; Elim (Rlt_antirefl ? H5). Intro; Split. Unfold Vn; Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rgt_2_0. +Left; Apply Rlt_Rinv; Sup0. Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Rewrite double; Rewrite Rplus_assoc; Apply Rle_compatibility. Apply Rle_anti_compatibility with ``-(An n)``; Rewrite Rplus_Or; Rewrite <- (Rplus_sym (An n)); Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu. Unfold Vn; Unfold Rdiv; Repeat Rewrite <- (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply Rlt_Rinv; Apply Rgt_2_0. +Left; Apply Rlt_Rinv; Sup0. Unfold Rminus; Rewrite double; Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring]; Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility; Apply Rle_Rabsolu. Intro; Unfold Wn; Unfold Rdiv; Rewrite <- (Rmult_Or ``/2``); Rewrite <- (Rmult_sym ``/2``); Apply Rlt_monotony. -Apply Rlt_Rinv; Apply Rgt_2_0. +Apply Rlt_Rinv; Sup0. Apply Rlt_anti_compatibility with (An n); Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym (An n)); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rle_lt_trans with (Rabsolu (An n)). Apply Rle_Rabsolu. Rewrite double; Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rabsolu_pos_lt; Apply H. Intro; Unfold Vn; Unfold Rdiv; Rewrite <- (Rmult_Or ``/2``); Rewrite <- (Rmult_sym ``/2``); Apply Rlt_monotony. -Apply Rlt_Rinv; Apply Rgt_2_0. +Apply Rlt_Rinv; Sup0. Apply Rlt_anti_compatibility with ``-(An n)``; Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym ``-(An n)``); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply Rle_lt_trans with (Rabsolu (An n)). Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu. Rewrite double; Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rabsolu_pos_lt; Apply H. @@ -598,3 +370,179 @@ Exists (sum_f_R0 An O); Unfold EUn; Exists O; Reflexivity. Intro; Elim X; Intros. Apply Specif.existT with x; Apply tech10; [Unfold Un_growing; Intro; Rewrite tech5; Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply H | Apply p]. Qed. + +Lemma Alembert_strong_general : (An:nat->R;k:R) ``0<=k<1`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). +Intros. +Cut (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). +Intro Hyp0; Apply Hyp0. +Apply cv_cauchy_2. +Apply cauchy_abs. +Apply cv_cauchy_1. +Cut (SigT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat](Rabsolu (An i)) N) l)) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat](Rabsolu (An i)) N) l)). +Intro Hyp; Apply Hyp. +Apply (Alembert_strong_positive [i:nat](Rabsolu (An i)) k). +Assumption. +Intro; Apply Rabsolu_pos_lt; Apply H0. +Unfold Un_cv. +Unfold Un_cv in H1. +Unfold Rdiv. +Intros. +Elim (H1 eps H2); Intros. +Exists x; Intros. +Rewrite <- Rabsolu_Rinv. +Rewrite <- Rabsolu_mult. +Rewrite Rabsolu_Rabsolu. +Unfold Rdiv in H3; Apply H3; Assumption. +Apply H0. +Intro. +Elim X; Intros. +Apply existTT with x. +Assumption. +Intro. +Elim X; Intros. +Apply Specif.existT with x. +Assumption. +Qed. + +(* Convergence de la SE dans le disque D(O,1/k) *) +(* le cas k=0 est decrit par le theoreme "Alembert" *) +Lemma Alembert_strong : (An:nat->R;x,k:R) ``0<k`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> ``(Rabsolu x)</k`` -> (SigT R [l:R](Pser An x l)). +Intros. +Cut (SigT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat]``(An i)*(pow x i)`` N) l)). +Intro. +Elim X; Intros. +Apply Specif.existT with x0. +Apply tech12; Assumption. +Case (total_order_T x R0); Intro. +Elim s; Intro. +EApply Alembert_strong_general with ``k*(Rabsolu x)``. +Split. +Unfold Rdiv; Apply Rmult_le_pos. +Left; Assumption. +Left; Apply Rabsolu_pos_lt. +Red; Intro; Rewrite H3 in a; Elim (Rlt_antirefl ? a). +Apply Rlt_monotony_contra with ``/k``. +Apply Rlt_Rinv; Assumption. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite Rmult_1r; Assumption. +Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). +Intro; Apply prod_neq_R0. +Apply H0. +Apply pow_nonzero. +Red; Intro; Rewrite H3 in a; Elim (Rlt_antirefl ? a). +Unfold Un_cv; Unfold Un_cv in H1. +Intros. +Cut ``0<eps/(Rabsolu x)``. +Intro. +Elim (H1 ``eps/(Rabsolu x)`` H4); Intros. +Exists x0. +Intros. +Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``. +Unfold R_dist. +Rewrite Rabsolu_mult. +Replace ``(Rabsolu ((An (S n))/(An n)))*(Rabsolu x)-k*(Rabsolu x)`` with ``(Rabsolu x)*((Rabsolu ((An (S n))/(An n)))-k)``; [Idtac | Ring]. +Rewrite Rabsolu_mult. +Rewrite Rabsolu_Rabsolu. +Apply Rlt_monotony_contra with ``/(Rabsolu x)``. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt. +Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a). +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite <- (Rmult_sym eps). +Unfold R_dist in H5. +Unfold Rdiv; Unfold Rdiv in H5; Apply H5; Assumption. +Apply Rabsolu_no_R0. +Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a). +Unfold Rdiv; Replace (S n) with (plus n (1)); [Idtac | Ring]. +Rewrite pow_add. +Simpl. +Rewrite Rmult_1r. +Rewrite Rinv_Rmult. +Replace ``(An (plus n (S O)))*((pow x n)*x)*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*/(An n)*x*((pow x n)*/(pow x n))``; [Idtac | Ring]. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r; Reflexivity. +Apply pow_nonzero. +Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a). +Apply H0. +Apply pow_nonzero. +Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a). +Unfold Rdiv; Apply Rmult_lt_pos. +Assumption. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt. +Red; Intro H7; Rewrite H7 in a; Elim (Rlt_antirefl ? a). +Apply Specif.existT with (An O). +Unfold Un_cv. +Intros. +Exists O. +Intros. +Unfold R_dist. +Replace (sum_f_R0 [i:nat]``(An i)*(pow x i)`` n) with (An O). +Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Induction n. +Simpl; Ring. +Rewrite tech5. +Rewrite <- Hrecn. +Rewrite b; Simpl; Ring. +Unfold ge; Apply le_O_n. +EApply Alembert_strong_general with ``k*(Rabsolu x)``. +Split. +Unfold Rdiv; Apply Rmult_le_pos. +Left; Assumption. +Left; Apply Rabsolu_pos_lt. +Red; Intro; Rewrite H3 in r; Elim (Rlt_antirefl ? r). +Apply Rlt_monotony_contra with ``/k``. +Apply Rlt_Rinv; Assumption. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite Rmult_1r; Assumption. +Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). +Intro; Apply prod_neq_R0. +Apply H0. +Apply pow_nonzero. +Red; Intro; Rewrite H3 in r; Elim (Rlt_antirefl ? r). +Unfold Un_cv; Unfold Un_cv in H1. +Intros. +Cut ``0<eps/(Rabsolu x)``. +Intro. +Elim (H1 ``eps/(Rabsolu x)`` H4); Intros. +Exists x0. +Intros. +Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``. +Unfold R_dist. +Rewrite Rabsolu_mult. +Replace ``(Rabsolu ((An (S n))/(An n)))*(Rabsolu x)-k*(Rabsolu x)`` with ``(Rabsolu x)*((Rabsolu ((An (S n))/(An n)))-k)``; [Idtac | Ring]. +Rewrite Rabsolu_mult. +Rewrite Rabsolu_Rabsolu. +Apply Rlt_monotony_contra with ``/(Rabsolu x)``. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt. +Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r). +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite <- (Rmult_sym eps). +Unfold R_dist in H5. +Unfold Rdiv; Unfold Rdiv in H5; Apply H5; Assumption. +Apply Rabsolu_no_R0. +Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r). +Unfold Rdiv; Replace (S n) with (plus n (1)); [Idtac | Ring]. +Rewrite pow_add. +Simpl. +Rewrite Rmult_1r. +Rewrite Rinv_Rmult. +Replace ``(An (plus n (S O)))*((pow x n)*x)*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*/(An n)*x*((pow x n)*/(pow x n))``; [Idtac | Ring]. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r; Reflexivity. +Apply pow_nonzero. +Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r). +Apply H0. +Apply pow_nonzero. +Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r). +Unfold Rdiv; Apply Rmult_lt_pos. +Assumption. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt. +Red; Intro H7; Rewrite H7 in r; Elim (Rlt_antirefl ? r). +Qed.
\ No newline at end of file |