diff options
Diffstat (limited to 'theories/Reals')
-rw-r--r-- | theories/Reals/Alembert.v | 1035 | ||||
-rw-r--r-- | theories/Reals/Ranalysis1.v | 2 | ||||
-rw-r--r-- | theories/Reals/Raxioms.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rbase.v | 4 | ||||
-rw-r--r-- | theories/Reals/Rseries.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rtrigo.v | 24 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 59 |
7 files changed, 1081 insertions, 47 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v new file mode 100644 index 000000000..f1ed4cc69 --- /dev/null +++ b/theories/Reals/Alembert.v @@ -0,0 +1,1035 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + + +Require Max. +Require Raxioms. +Require DiscrR. +Require Rbase. +Require Rseries. +Require Rtrigo_fun. + +Axiom fct_eq : (A:Type)(f1,f2:A->R) ((x:A)(f1 x)==(f2 x)) -> f1 == f2. + +Definition SigT := Specif.sigT. + +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``. +Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro H; Assumption | Discriminate]. +Qed. + +Lemma Rgt_3_0 : ``0<3``. +Cut ~(O=(3)); [Intro H0; Generalize (lt_INR_0 (3) (neq_O_lt (3) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H; Assumption | Discriminate]. +Qed. + +(*********************) +(* Lemmes techniques *) +(*********************) + +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. +Replace (sum_f_R0 An (S N)) with ``(sum_f_R0 An N)+(An (S N))``. +Apply gt0_plus_gt0_is_gt0. +Apply HrecN; Intros; Apply H. +Apply le_S; Assumption. +Apply H. +Apply le_n. +Reflexivity. +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. +Replace (minus (S n) (S n)) with O. +Simpl. +Replace (plus n O) with n; [Idtac | Ring]. +Reflexivity. +Apply minus_n_n. +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. +Induction N. +Simpl. +Field. +Replace ``1+ -k`` with ``1-k``; [Idtac | Ring]. +Apply Rminus_eq_contra. +Apply not_sym. +Assumption. +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)``; [Idtac | Field; Replace ``1+ -k`` with ``1-k``; [Idtac | Ring]; Apply Rminus_eq_contra; Apply not_sym; Assumption]. +Replace ``(1-(pow k (S N))+(1-k)*(pow k (S N)))`` with ``1-k*(pow k (S N))``; [Idtac | Ring]. +Replace (S (S N)) with (plus (1) (S N)). +Rewrite pow_add. +Simpl. +Rewrite Rmult_1r. +Reflexivity. +Ring. +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))). +Replace ``(sum_f_R0 An (S N))`` with ``(sum_f_R0 An N)+(An (S N))``. +Do 2 Rewrite <- (Rplus_sym (An (S N))). +Apply Rle_compatibility. +Apply HrecN. +Symmetry; Apply tech5. +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. +Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring]. +Rewrite H. +Rewrite (H n). +Rewrite (H i). +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. +Replace (sum_f_R0 An (S N)) with ``(sum_f_R0 An N)+(An (S N))``; [Idtac | Reflexivity]. +Replace (sum_f_R0 Bn (S N)) with ``(sum_f_R0 Bn N)+(Bn (S N))``; [Idtac | Reflexivity]. +Replace (sum_f_R0 Cn (S N)) with ``(sum_f_R0 Cn N)+(Cn (S N))``; [Idtac | Reflexivity]. +Rewrite HrecN. +Unfold Rminus. +Repeat Rewrite Rplus_assoc. +Apply Rplus_plus_r. +Rewrite Ropp_distr1. +Rewrite <- Rplus_assoc. +Rewrite <- (Rplus_sym ``-(sum_f_R0 Cn N)``). +Rewrite Rplus_assoc. +Apply Rplus_plus_r. +Unfold Rminus in H. +Apply H. +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. + + +(*************************************************) +(* Différentes versions du critère de D'Alembert *) +(*************************************************) + +Lemma Alembert_positive : (An:nat->R) ((n:nat)``0<(An n)``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) R0) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). +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. +2:Exists (sum_f_R0 An O). +2:Unfold EUn. +2:Exists O. +2:Reflexivity. +Unfold Un_cv in H0. +Unfold bound. +Cut ``0</2``; [Intro | Apply Rlt_Rinv; Apply Rgt_2_0]. +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. +Rewrite H4. +Assert H5 := (lt_eq_lt_dec x1 x). +Elim H5; Intros. +Elim a; Intro. +Replace (sum_f_R0 An x) with (Rplus (sum_f_R0 An x1) (sum_f_R0 [i:nat](An (plus (S x1) i)) (minus x (S x1)))). +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. +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. +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. +2:Symmetry. +2:Apply tech2. +2:Assumption. +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))))). +Intro. +Apply Rle_trans with (Rmult (An (S x)) (sum_f_R0 [i:nat](pow ``/2`` i) (minus x1 (S x)))). +Assumption. +Rewrite <- (Rmult_sym (An (S x))). +Apply Rle_monotony. +Left; Apply H. +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; 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. +DiscrR. +Field. +DiscrR. +Pattern 3 R1; Replace R1 with ``/1``. +2:Apply Rinv_R1. +Apply tech7; DiscrR. +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. +2:Replace (plus (S x) O) with (S x); [Reflexivity | Ring]. +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. +Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring]. +Rewrite H7. +Rewrite (H7 x). +Rewrite (H7 i). +Ring. +Intros. +Unfold R_dist in H2. +Apply Rlt_monotony_contra with ``/(An n)``. +Apply Rlt_Rinv; Apply H. +Do 2 Rewrite (Rmult_sym ``/(An n)``). +Rewrite Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r. +Replace ``(An (S n))*/(An n)`` with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-0))``. +Apply H2; Assumption. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or. +Rewrite Rabsolu_Rabsolu. +Rewrite Rabsolu_right. +Unfold Rdiv; Reflexivity. +Left; Unfold Rdiv; Change ``0<(An (S n))*/(An n)``; Apply Rmult_lt_pos. +Apply H. +Apply Rlt_Rinv; Apply H. +Red; Intro. +Assert H8 := (H n). +Rewrite H7 in H8; Elim (Rlt_antirefl ? H8). +Intro. +Elim X; Intros. +Apply Specif.existT with x. +Apply tech10. +2:Assumption. +Unfold Un_growing. +Intro. +Rewrite tech5. +Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Left; Apply H. +Qed. + +Lemma Alembert_general:(An:nat->R) ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) R0) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). +Intros. +Pose Vn := [i:nat]``(2*(Rabsolu (An i))+(An i))/2``. +Pose Wn := [i:nat]``(2*(Rabsolu (An i))-(An i))/2``. +Cut (n:nat)``0<(Vn n)``. +Intro. +Cut (n:nat)``0<(Wn n)``. +Intro. +Cut (Un_cv [n:nat](Rabsolu ``(Vn (S n))/(Vn n)``) ``0``). +Intro. +Cut (Un_cv [n:nat](Rabsolu ``(Wn (S n))/(Wn n)``) ``0``). +Intro. +Assert H5 := (Alembert_positive Vn H1 H3). +Assert H6 := (Alembert_positive Wn H2 H4). +Elim H5; Intros. +Elim H6; Intros. +Apply Specif.existT with ``x-x0``. +Unfold Un_cv. +Unfold Un_cv in p. +Unfold Un_cv in p0. +Intros. +Cut ``0<eps/2``. +Intro. +Elim (p ``eps/2`` H8); Clear p; Intros. +Elim (p0 ``eps/2`` H8); Clear p0; Intros. +Pose N := (max x1 x2). +Exists N. +Intros. +Replace (sum_f_R0 An n) with (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)). +Unfold R_dist. +Replace (Rminus (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)) (Rminus x x0)) with (Rplus (Rminus (sum_f_R0 Vn n) x) (Ropp (Rminus (sum_f_R0 Wn n) x0))); [Idtac | Ring]. +Apply Rle_lt_trans with (Rplus (Rabsolu (Rminus (sum_f_R0 Vn n) x)) (Rabsolu (Ropp (Rminus (sum_f_R0 Wn n) x0)))). +Apply Rabsolu_triang. +Rewrite Rabsolu_Ropp. +Apply Rlt_le_trans with ``eps/2+eps/2``. +Apply Rplus_lt. +Unfold R_dist in H9. +Apply H9. +Unfold ge; Apply le_trans with N. +Unfold N; Apply le_max_l. +Assumption. +Unfold R_dist in H10. +Apply H10. +Unfold ge; Apply le_trans with N. +Unfold N; Apply le_max_r. +Assumption. +Right; Symmetry; Apply double_var. +Symmetry; Apply tech11. +Intro. +Unfold Vn Wn. +Field. +DiscrR. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0]. +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))``. +Intro. +Unfold Un_cv. +Intros. +Unfold Un_cv in H0. +Cut ``0<eps/3``. +Intro. +Elim (H0 ``eps/3`` H8); Intros. +Exists x. +Intros. +Assert H11 := (H9 n H10). +Unfold R_dist. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu. +Unfold R_dist in H11; Unfold Rminus in H11; Rewrite Ropp_O in H11; Rewrite Rplus_Or in H11; Rewrite Rabsolu_Rabsolu in H11. +Rewrite Rabsolu_right. +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. +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]. +Intro. +Unfold Rdiv. +Rewrite Rabsolu_mult. +Rewrite <- Rmult_assoc. +Replace ``3`` with ``2*(3*/2)``; [Idtac | Field; DiscrR]. +Apply Rle_trans with ``(Wn (S n))*2*/(Rabsolu (An n))``. +Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply H2. +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. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H. +Elim (H4 (S n)); Intros; Assumption. +Apply H. +Intro. +Apply Rle_monotony_contra with (Wn n). +Apply H2. +Rewrite <- Rinv_r_sym. +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. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l; Elim (H4 n); Intros; Assumption. +DiscrR. +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. +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. +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))``. +Intro. +Cut (n:nat)``/(Vn n)<=2*/(Rabsolu (An n))``. +Intro. +Cut (n:nat)``(Vn (S n))/(Vn n)<=3*(Rabsolu (An (S n))/(An n))``. +Intro. +Unfold Un_cv. +Intros. +Unfold Un_cv in H1. +Cut ``0<eps/3``. +Intro. +Elim (H0 ``eps/3`` H7); Intros. +Exists x. +Intros. +Assert H10 := (H8 n H9). +Unfold R_dist. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu. +Unfold R_dist in H10; Unfold Rminus in H10; Rewrite Ropp_O in H10; Rewrite Rplus_Or in H10; Rewrite Rabsolu_Rabsolu in H10. +Rewrite Rabsolu_right. +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. +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]. +Intro. +Unfold Rdiv. +Rewrite Rabsolu_mult. +Rewrite <- Rmult_assoc. +Replace ``3`` with ``2*(3*/2)``; [Idtac | Field; DiscrR]. +Apply Rle_trans with ``(Vn (S n))*2*/(Rabsolu (An n))``. +Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply H1. +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. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H. +Elim (H3 (S n)); Intros; Assumption. +Apply H. +Intro. +Apply Rle_monotony_contra with (Vn n). +Apply H1. +Rewrite <- Rinv_r_sym. +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. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l; Elim (H3 n); Intros; Assumption. +DiscrR. +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. +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. +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_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_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. +Qed. + +Lemma Alembert_step1 : (An:nat->R;x:R) ``x<>0`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) ``0``) -> (SigT R [l:R](Pser An x l)). +Intros. +Pose Bn := [i:nat]``(An i)*(pow x i)``. +Cut (n:nat)``(Bn n)<>0``. +Intro. +Cut (Un_cv [n:nat](Rabsolu ``(Bn (S n))/(Bn n)``) ``0``). +Intro. +Assert H4 := (Alembert_general Bn H2 H3). +Elim H4; Intros. +Apply Specif.existT with x0. +Unfold Bn in p. +Apply tech12. +Assumption. +Unfold Un_cv. +Intros. +Unfold Un_cv in H1. +Cut ``0<eps/(Rabsolu x)``. +Intro. +Elim (H1 ``eps/(Rabsolu x)`` H4); Intros. +Exists x0. +Intros. +Unfold R_dist. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu. +Unfold Bn. +Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``. +Rewrite Rabsolu_mult. +Apply Rlt_monotony_contra with ``/(Rabsolu x)``. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. +Rewrite <- (Rmult_sym (Rabsolu x)). +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite <- (Rmult_sym eps). +Unfold Rdiv in H5. +Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``(R_dist (Rabsolu ((An (S n))*/(An n))) 0)``. +Apply H5; Assumption. +Unfold R_dist. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu. +Unfold Rdiv; Reflexivity. +Apply Rabsolu_no_R0; Assumption. +Replace (S n) with (plus n (1)); [Idtac | Ring]. +Rewrite pow_add. +Unfold Rdiv. +Rewrite Rinv_Rmult. +Replace ``(An (plus n (S O)))*((pow x n)*(pow x (S O)))*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*(pow x (S O))*/(An n)*((pow x n)*/(pow x n))``; [Idtac | Ring]. +Rewrite <- Rinv_r_sym. +Simpl. +Ring. +Apply pow_nonzero; Assumption. +Apply H0. +Apply pow_nonzero; Assumption. +Unfold Rdiv; Apply Rmult_lt_pos. +Assumption. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. +Intro. +Unfold Bn. +Apply prod_neq_R0. +Apply H0. +Apply pow_nonzero; Assumption. +Qed. + +Lemma Alembert_step2 : (An:nat->R;x:R) ``x==0`` -> (SigT R [l:R](Pser An x l)). +Intros. +Apply Specif.existT with (An O). +Unfold Pser. +Unfold infinit_sum. +Intros. +Exists O. +Intros. +Replace (sum_f_R0 [n0:nat]``(An n0)*(pow x n0)`` n) with (An O). +Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Induction n. +Simpl. +Ring. +Rewrite tech5. +Rewrite Hrecn. +Rewrite H. +Simpl. +Ring. +Unfold ge; Apply le_O_n. +Qed. + +(* Un critère utile de convergence des séries entières *) +Theorem Alembert : (An:nat->R;x:R) ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) ``0``) -> (SigT R [l:R](Pser An x l)). +Intros. +Case (total_order_T x R0); Intro. +Elim s; Intro. +Cut ``x<>0``. +Intro. +Apply Alembert_step1; Assumption. +Red; Intro; Rewrite H1 in a; Elim (Rlt_antirefl ? a). +Apply Alembert_step2; Assumption. +Cut ``x<>0``. +Intro. +Apply Alembert_step1; Assumption. +Red; Intro; Rewrite H1 in r; Elim (Rlt_antirefl ? r). +Qed. + +(* Le "vrai" critère de D'Alembert pour les séries à TG positif *) +Lemma Alembert_strong_positive : (An:nat->R;k:R) ``0<=k<1`` -> ((n:nat)``0<(An n)``) -> (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 An k Hyp 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. +2:Exists (sum_f_R0 An O). +2:Unfold EUn. +2:Exists O. +2:Reflexivity. +Assert H1 := (tech13 ? ? Hyp H0). +Elim H1; Intros. +Elim H2; Intros. +Elim H4; Intros. +Unfold bound. +Exists ``(sum_f_R0 An x0)+/(1-x)*(An (S x0))``. +Unfold is_upper_bound. +Intros. +Unfold EUn in H6. +Elim H6; Intros. +Rewrite H7. +Assert H8 := (lt_eq_lt_dec x2 x0). +Elim H8; Intros. +Elim a; Intro. +Replace (sum_f_R0 An x0) with (Rplus (sum_f_R0 An x2) (sum_f_R0 [i:nat](An (plus (S x2) i)) (minus x0 (S x2)))). +Pattern 1 (sum_f_R0 An x2); 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 Rlt_Rinv. +Apply Rlt_anti_compatibility with x. +Rewrite Rplus_Or. +Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring]. +Apply H. +Symmetry; Apply tech2; Assumption. +Rewrite b. +Pattern 1 (sum_f_R0 An x0); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Left; Apply Rmult_lt_pos. +Apply Rlt_Rinv. +Apply Rlt_anti_compatibility with x. +Rewrite Rplus_Or. +Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring]. +Apply H. +Replace (sum_f_R0 An x2) with (Rplus (sum_f_R0 An x0) (sum_f_R0 [i:nat](An (plus (S x0) i)) (minus x2 (S x0)))). +Apply Rle_compatibility. +2:Symmetry. +2:Apply tech2. +2:Assumption. +Cut (Rle (sum_f_R0 [i:nat](An (plus (S x0) i)) (minus x2 (S x0))) (Rmult (An (S x0)) (sum_f_R0 [i:nat](pow x i) (minus x2 (S x0))))). +Intro. +Apply Rle_trans with (Rmult (An (S x0)) (sum_f_R0 [i:nat](pow x i) (minus x2 (S x0)))). +Assumption. +Rewrite <- (Rmult_sym (An (S x0))). +Apply Rle_monotony. +Left; Apply H. +Rewrite tech3. +Unfold Rdiv. +Apply Rle_monotony_contra with ``1-x``. +Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or. +Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring]. +Do 2 Rewrite (Rmult_sym ``1-x``). +Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Apply Rle_anti_compatibility with ``(pow x (S (minus x2 (S x0))))``. +Replace ``(pow x (S (minus x2 (S x0))))+(1-(pow x (S (minus x2 (S x0)))))`` with R1; [Idtac | Ring]. +Rewrite <- (Rplus_sym R1). +Pattern 1 R1; Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Left; Apply pow_lt. +Apply Rle_lt_trans with k. +Elim Hyp; Intros; Assumption. +Elim H3; Intros; Assumption. +Apply Rminus_eq_contra. +Red; Intro. +Elim H3; Intros. +Rewrite H10 in H12; Elim (Rlt_antirefl ? H12). +Red; Intro. +Elim H3; Intros. +Rewrite H10 in H12; Elim (Rlt_antirefl ? H12). +Replace (An (S x0)) with (An (plus (S x0) O)). +Apply (tech6 [i:nat](An (plus (S x0) i)) x). +Left; Apply Rle_lt_trans with k. +Elim Hyp; Intros; Assumption. +Elim H3; Intros; Assumption. +2:Replace (plus (S x0) O) with (S x0); [Reflexivity | Ring]. +Intro. +Cut (n:nat)(ge n x0)->``(An (S n))<x*(An n)``. +Intro. +Replace (plus (S x0) (S i)) with (S (plus (S x0) i)). +Apply H9. +Unfold ge. +Apply tech8. +Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring]. +Rewrite H10. +Rewrite (H10 x0). +Rewrite (H10 i). +Ring. +Intros. +Apply Rlt_monotony_contra with ``/(An n)``. +Apply Rlt_Rinv; Apply H. +Do 2 Rewrite (Rmult_sym ``/(An n)``). +Rewrite Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r. +Replace ``(An (S n))*/(An n)`` with ``(Rabsolu ((An (S n))/(An n)))``. +Apply H5; Assumption. +Rewrite Rabsolu_right. +Unfold Rdiv; Reflexivity. +Left; Unfold Rdiv; Change ``0<(An (S n))*/(An n)``; Apply Rmult_lt_pos. +Apply H. +Apply Rlt_Rinv; Apply H. +Red; Intro. +Assert H11 := (H n). +Rewrite H10 in H11; Elim (Rlt_antirefl ? H11). +Intro. +Elim X; Intros. +Apply Specif.existT with x. +Apply tech10. +2:Assumption. +Unfold Un_growing. +Intro. +Rewrite tech5. +Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Left; Apply H. +Qed. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index a7246218e..490940e73 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -15,7 +15,6 @@ Require Rlimit. Require Rderiv. Require DiscrR. Require Rtrigo. -Require Specif. (****************************************************) (** Basic operations on functions *) @@ -175,7 +174,6 @@ Definition derivable_pt_lim [f:R->R;x,l:R] : Prop := ((eps:R) ``0<eps``->(EXT de Definition derivable_pt_abs [f:R->R;x:R] : R -> Prop := [l:R](derivable_pt_lim f x l). -Definition SigT := Specif.sigT. Definition derivable_pt [f:R->R;x:R] := (SigT R (derivable_pt_abs f x)). Definition derivable [f:R->R] := (x:R)(derivable_pt f x). diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 1c7674f4e..e273b5bfd 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -147,5 +147,5 @@ Definition is_lub:=[E:R->Prop][m:R] (**********) Axiom complet:(E:R->Prop)(bound E)-> (ExT [x:R] (E x))-> - (ExT [m:R](is_lub E m)). + (sigTT R [m:R](is_lub E m)). diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 069ebe3cd..f92b5c2a6 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1577,3 +1577,7 @@ Lemma add_auto : (p,q:nat) ``(INR2 (S p))+(INR2 q)==(INR2 p)+(INR2 (S q))``. Intros; Repeat Rewrite <- INR_eq_INR2; Repeat Rewrite S_INR; Ring. Qed. +(**********) +Lemma complet_weak : (E:R->Prop) (bound E) -> (ExT [x:R] (E x)) -> (ExT [m:R] (is_lub E m)). +Intros; Elim (complet E H H0); Intros; Split with x; Assumption. +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 68e77d528..9af9bdd54 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -88,7 +88,7 @@ Qed. (*********) Lemma Un_cv_crit:Un_growing->(bound EUn)->(ExT [l:R] (Un_cv l)). Unfold Un_growing Un_cv;Intros; - Generalize (complet EUn H0 EUn_noempty);Intro; + Generalize (complet_weak EUn H0 EUn_noempty);Intro; Elim H1;Clear H1;Intros;Split with x;Intros; Unfold is_lub in H1;Unfold bound in H0;Unfold is_upper_bound in H0 H1; Elim H0;Clear H0;Intros;Elim H1;Clear H1;Intros; diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 06222a5d3..c1ada0451 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -15,6 +15,7 @@ Require Rbase. Require R_sqr. Require Rfunctions. Require Rsigma. +Require Rlimit. Require Export Rtrigo_def. Lemma PI_neq0 : ~``PI==0``. @@ -74,19 +75,10 @@ Lemma pythagorean : (x,y,z:R) ``(Rsqr x)+(Rsqr y)==(Rsqr z)`` -> ``0<=x`` -> ``0 Intros x y z H1 H2 H3 H4; Generalize (arc_sin_cos x y z H2 H3 H4); Intro H5; Elim H5; [ Intros x0 H6; Elim H6; Intros H7 H8; Exists x0; Rewrite H7; Rewrite H8; Replace ``z*(cos x0)*(cos x0)+z*(sin x0)*(sin x0)`` with ``z*((Rsqr (sin x0))+(Rsqr (cos x0)))``; [ Rewrite sin2_cos2; Ring | Unfold Rsqr; Ring] | Assumption]. Qed. -Lemma double : (x:R) ``2*x==x+x``. -Intro; Ring. -Qed. - Lemma aze : ``2<>0``. DiscrR. Qed. -Lemma double_var : (x:R) ``x == x/2 + x/2``. -Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m. -Apply aze. -Qed. - Lemma sin_2a : (x:R) ``(sin (2*x))==2*(sin x)*(cos x)``. Intro x; Rewrite double; Rewrite sin_plus. Rewrite <- (Rmult_sym (sin x)); Symmetry; Rewrite Rmult_assoc; Apply double. @@ -313,10 +305,6 @@ Lemma PI2_RGT_0 : ``0<PI/2``. Cut ~(O=(2)); [Intro H; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``2``) PI_RGT_0 (Rlt_Rinv ``2`` H1)); Intro H2; Assumption | Discriminate]. Qed. -Lemma Rgt_2_0 : ``0<2``. -Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro H; Assumption | Discriminate]. -Qed. - Lemma cos_eq_0_2PI_0 : (x:R) ``R0<=x`` -> ``x<=2*PI`` -> ``(cos x)==0`` -> ``x==(PI/2)``\/``x==3*(PI/2)``. Intros; Case (total_order x ``3*(PI/2)``); Intro. Rewrite cos_sin in H1. @@ -508,10 +496,6 @@ Lemma PI6_RLT_PI2 : ``PI/6<PI/2``. Cut ~(O=(4)); [ Intro H; Cut ~(O=(1)); [Intro H0; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rlt_compatibility ``2`` ``0`` ``4`` H1); Rewrite Rplus_sym; Rewrite Rplus_Ol; Replace ``2+4`` with ``6``; [Intro H2; Generalize (lt_INR_0 (1) (neq_O_lt (1) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H3; Generalize (Rlt_compatibility ``1`` ``0`` ``1`` H3); Rewrite Rplus_sym; Rewrite Rplus_Ol; Clear H3; Intro H3; Generalize (Rlt_Rinv_R1 ``2`` ``6`` (Rlt_le ``1`` ``2`` H3) H2); Intro H4; Generalize (Rlt_monotony PI (Rinv ``6``) (Rinv ``2``) PI_RGT_0 H4); Intro H5; Assumption | Ring] | Discriminate] | Discriminate ]. Qed. -Lemma Rgt_3_0 : ``0<3``. -Cut ~(O=(3)); [Intro H0; Generalize (lt_INR_0 (3) (neq_O_lt (3) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H; Assumption | Discriminate]. -Qed. - Lemma sqrt2_neq_0 : ~``(sqrt 2)==0``. Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``2`` H1 H2); Intro H; Absurd ``2==0``; [ DiscrR | Assumption]. Qed. @@ -524,10 +508,6 @@ Lemma sqrt3_2_neq_0 : ~``2*(sqrt 3)==0``. Apply prod_neq_R0; [DiscrR | Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``3`` H1 H2); Intro H; Absurd ``3==0``; [ DiscrR | Assumption]]. Qed. -Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. -Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. -Qed. - Lemma Rlt_sqrt2_0 : ``0<(sqrt 2)``. Generalize (foo ``2`` (Rlt_le ``0`` ``2`` Rgt_2_0)); Intro H1; Elim H1; Intro H2; [Assumption | Absurd ``0 == (sqrt 2)``; [Apply not_sym; Apply sqrt2_neq_0 | Assumption]]. Qed. @@ -1512,4 +1492,4 @@ Simpl; Discriminate. Simpl; Discriminate. Simpl; Discriminate. Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` a ``0`` H H2)). -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 8580f6893..8fc69e038 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -1,31 +1,36 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Require Max. Require Raxioms. Require DiscrR. Require Rbase. Require Rseries. Require Rtrigo_fun. -Require Specif. - -Section Pserie. - -Variable An:nat->R. - -Definition SigT := Specif.sigT. - -Axiom Alembert:(x,k:R) (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> ``(Rabsolu k) <1 `` -> (SigT R [l:R] (Pser An x l)). - -End Pserie. +Require Export Alembert. (*****************************) (* Definition of exponential *) (*****************************) Definition exp_in:R->R->Prop := [x,l:R](infinit_sum [i:nat]``/(INR (fact i))*(pow x i)`` l). +Lemma exp_cof_no_R0 : (n:nat) ``/(INR (fact n))<>0``. +Intro. +Apply Rinv_neq_R0. +Apply INR_fact_neq_0. +Qed. + Lemma exist_exp : (x:R)(SigT R [l:R](exp_in x l)). -Intro; Generalize (Alembert [n:nat](Rinv (INR (fact n))) x ``0`` Alembert_exp). -Intros; Cut ``(Rabsolu 0)<1``. -Intros; Exact (X H). -Rewrite Rabsolu_R0; Apply Rlt_R0_R1. +Intro; Generalize (Alembert [n:nat](Rinv (INR (fact n))) x exp_cof_no_R0 Alembert_exp). +Unfold Pser exp_in. +Trivial. Defined. Definition exp : R -> R := [x:R](projT1 ? ? (exist_exp x)). @@ -35,9 +40,6 @@ Intros; Apply pow_ne_zero. Red; Intro; Rewrite H0 in H; Elim (lt_n_n ? H). Qed. -(* Axiome d'extensionnalité *) -Axiom fct_eq : (A:Type)(f1,f2:A->R) ((x:A)(f1 x)==(f2 x)) -> f1 == f2. - (* Unicité de la limite d'une série convergente *) Lemma unicite_sum : (An:nat->R;l1,l2:R) (infinit_sum An l1) -> (infinit_sum An l2) -> l1 == l2. Unfold infinit_sum; Intros. @@ -236,12 +238,20 @@ Apply INR_eq. Repeat Rewrite S_INR; Rewrite plus_INR; Repeat Rewrite mult_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Replace (INR O) with R0; [Ring | Reflexivity]. Qed. +Lemma cosn_no_R0 : (n:nat)``(cos_n n)<>0``. +Intro; Unfold cos_n; Unfold Rdiv; Apply prod_neq_R0. +Apply pow_nonzero; DiscrR. +Apply Rinv_neq_R0. +Apply INR_fact_neq_0. +Qed. + (**********) Definition cos_in:R->R->Prop := [x,l:R](infinit_sum [i:nat]``(cos_n i)*(pow x i)`` l). (**********) Lemma exist_cos : (x:R)(SigT R [l:R](cos_in x l)). -Intro; Generalize (Alembert cos_n x R0 Alembert_cos); Unfold Pser cos_in; Rewrite Rabsolu_R0; Intros; Apply (X Rlt_R0_R1). +Intro; Generalize (Alembert cos_n x cosn_no_R0 Alembert_cos). +Unfold Pser cos_in; Trivial. Qed. (* Définition du cosinus *) @@ -327,12 +337,19 @@ Apply lt_O_Sn. Apply INR_eq; Repeat Rewrite S_INR; Rewrite plus_INR; Repeat Rewrite mult_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Replace (INR O) with R0; [Ring | Reflexivity]. Qed. +Lemma sin_no_R0 : (n:nat)``(sin_n n)<>0``. +Intro; Unfold sin_n; Unfold Rdiv; Apply prod_neq_R0. +Apply pow_nonzero; DiscrR. +Apply Rinv_neq_R0; Apply INR_fact_neq_0. +Qed. + (**********) Definition sin_in:R->R->Prop := [x,l:R](infinit_sum [i:nat]``(sin_n i)*(pow x i)`` l). (**********) Lemma exist_sin : (x:R)(SigT R [l:R](sin_in x l)). -Intro; Generalize (Alembert sin_n x R0 Alembert_sin); Rewrite Rabsolu_R0; Intros; Apply (X Rlt_R0_R1). +Intro; Generalize (Alembert sin_n x sin_no_R0 Alembert_sin). +Unfold Pser sin_n; Trivial. Qed. (***********************) @@ -411,4 +428,4 @@ Qed. Lemma sin_PI2 : ``(sin (PI/2))==1``. Assert H := (projT2 ? ? PI_ax); Elim H; Intros; Elim H1; Intros; Unfold PI; Exact H2. -Qed.
\ No newline at end of file +Qed. |