From 0671d720e4f617b5fa4dae4432b893a84c664685 Mon Sep 17 00:00:00 2001 From: desmettr Date: Mon, 1 Jul 2002 14:00:53 +0000 Subject: Constructions des séries alternées et de PI git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2819 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/AltSeries.v | 463 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 463 insertions(+) create mode 100644 theories/Reals/AltSeries.v diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v new file mode 100644 index 0000000000..d8c25e1c3b --- /dev/null +++ b/theories/Reals/AltSeries.v @@ -0,0 +1,463 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* R] : nat->R := [i:nat]``(pow (-1) i)*(Un i)``. +Definition positivity_sui [Un:nat->R] : Prop := (n:nat)``0<=(Un n)``. + +(**********) +Lemma pow_1_even : (n:nat) ``(pow (-1) (mult (S (S O)) n))==1``. +Intro; Induction n. +Reflexivity. +Replace (mult (2) (S n)) with (plus (2) (mult (2) n)). +Rewrite pow_add; Rewrite Hrecn; Simpl; Ring. +Replace (S n) with (plus n (1)); [Ring | Ring]. +Qed. + +(**********) +Lemma pow_1_odd : (n:nat) ``(pow (-1) (S (mult (S (S O)) n)))==-1``. +Intro; Replace (S (mult (2) n)) with (plus (mult (2) n) (1)); [Idtac | Ring]. +Rewrite pow_add; Rewrite pow_1_even; Simpl; Ring. +Qed. + +(* Croissance des sommes partielles impaires *) +Lemma CV_ALT_step1 : (Un:nat->R) (Un_decreasing Un) -> (Un_growing [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N)))). +Intros; Unfold Un_growing; Intro. +Cut (mult (S (S O)) (S n)) = (S (S (mult (2) n))). +Intro; Rewrite H0. +Do 4 Rewrite tech5; Repeat Rewrite Rplus_assoc; Apply Rle_compatibility. +Pattern 1 (tg_alt Un (S (mult (S (S O)) n))); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Unfold tg_alt; Rewrite <- H0; Rewrite pow_1_odd; Rewrite pow_1_even; Rewrite Rmult_1l. +Apply Rle_anti_compatibility with ``(Un (S (mult (S (S O)) (S n))))``. +Rewrite Rplus_Or; Replace ``(Un (S (mult (S (S O)) (S n))))+((Un (mult (S (S O)) (S n)))+ -1*(Un (S (mult (S (S O)) (S n)))))`` with ``(Un (mult (S (S O)) (S n)))``; [Idtac | Ring]. +Apply H. +Cut (n:nat) (S n)=(plus n (1)); [Intro | Intro; Ring]. +Rewrite (H0 n); Rewrite (H0 (S (mult (2) n))); Rewrite (H0 (mult (2) n)); Ring. +Qed. + +(* Décroissance des sommes partielles paires *) +Lemma CV_ALT_step1_bis : (Un:nat->R) (Un_decreasing Un) -> (Un_decreasing [N:nat](sum_f_R0 (tg_alt Un) (mult (2) N))). +Intros; Unfold Un_decreasing; Intro. +Cut (mult (S (S O)) (S n)) = (S (S (mult (2) n))). +Intro; Rewrite H0; Do 2 Rewrite tech5; Repeat Rewrite Rplus_assoc. +Pattern 2 (sum_f_R0 (tg_alt Un) (mult (S (S O)) n)); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Unfold tg_alt; Rewrite <- H0; Rewrite pow_1_odd; Rewrite pow_1_even; Rewrite Rmult_1l. +Apply Rle_anti_compatibility with ``(Un (S (mult (S (S O)) n)))``. +Rewrite Rplus_Or; Replace ``(Un (S (mult (S (S O)) n)))+( -1*(Un (S (mult (S (S O)) n)))+(Un (mult (S (S O)) (S n))))`` with ``(Un (mult (S (S O)) (S n)))``; [Idtac | Ring]. +Rewrite H0; Apply H. +Cut (n:nat) (S n)=(plus n (1)); [Intro | Intro; Ring]. +Rewrite (H0 n); Rewrite (H0 (S (mult (2) n))); Rewrite (H0 (mult (2) n)); Ring. +Qed. + +(**********) +Lemma CV_ALT_step2 : (Un:nat->R;N:nat) (Un_decreasing Un) -> (positivity_sui Un) -> (Rle (sum_f_R0 [i:nat](tg_alt Un (S i)) (S (mult (2) N))) R0). +Intros; Induction N. +Simpl; Unfold tg_alt; Simpl; Rewrite Rmult_1r. +Replace ``-1* -1*(Un (S (S O)))`` with (Un (S (S O))); [Idtac | Ring]. +Apply Rle_anti_compatibility with ``(Un (S O))``; Rewrite Rplus_Or. +Replace ``(Un (S O))+ (-1*(Un (S O))+(Un (S (S O))))`` with (Un (S (S O))); [Apply H | Ring]. +Cut (S (mult (2) (S N))) = (S (S (S (mult (2) N)))). +Intro; Rewrite H1; Do 2 Rewrite tech5. +Apply Rle_trans with (sum_f_R0 [i:nat](tg_alt Un (S i)) (S (mult (S (S O)) N))). +Pattern 2 (sum_f_R0 [i:nat](tg_alt Un (S i)) (S (mult (S (S O)) N))); Rewrite <- Rplus_Or. +Rewrite Rplus_assoc; Apply Rle_compatibility. +Unfold tg_alt; Rewrite <- H1. +Rewrite pow_1_odd. +Cut (S (S (mult (2) (S N)))) = (mult (2) (S (S N))). +Intro; Rewrite H2; Rewrite pow_1_even; Rewrite Rmult_1l; Rewrite <- H2. +Apply Rle_anti_compatibility with ``(Un (S (mult (S (S O)) (S N))))``. +Rewrite Rplus_Or; Replace ``(Un (S (mult (S (S O)) (S N))))+( -1*(Un (S (mult (S (S O)) (S N))))+(Un (S (S (mult (S (S O)) (S N))))))`` with ``(Un (S (S (mult (S (S O)) (S N)))))``; [Idtac | Ring]. +Apply H. +Apply INR_eq; Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Apply HrecN. +Apply INR_eq; Repeat Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Qed. + +(* A more general inequality *) +Lemma CV_ALT_step3 : (Un:nat->R;N:nat) (Un_decreasing Un) -> (positivity_sui Un) -> (Rle (sum_f_R0 [i:nat](tg_alt Un (S i)) N) R0). +Intros; Induction N. +Simpl; Unfold tg_alt; Simpl; Rewrite Rmult_1r. +Apply Rle_anti_compatibility with (Un (S O)). +Rewrite Rplus_Or; Replace ``(Un (S O))+ -1*(Un (S O))`` with R0; [Apply H0 | Ring]. +Assert H1 := (even_odd_cor N). +Elim H1; Intros. +Elim H2; Intro. +Rewrite H3; Apply CV_ALT_step2; Assumption. +Rewrite H3; Rewrite tech5. +Apply Rle_trans with (sum_f_R0 [i:nat](tg_alt Un (S i)) (S (mult (S (S O)) x))). +Pattern 2 (sum_f_R0 [i:nat](tg_alt Un (S i)) (S (mult (S (S O)) x))); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Unfold tg_alt; Simpl. +Replace (plus x (plus x O)) with (mult (2) x); [Idtac | Ring]. +Rewrite pow_1_even. +Replace `` -1*( -1*( -1*1))*(Un (S (S (S (mult (S (S O)) x)))))`` with ``-(Un (S (S (S (mult (S (S O)) x)))))``; [Idtac | Ring]. +Apply Rle_anti_compatibility with (Un (S (S (S (mult (S (S O)) x))))). +Rewrite Rplus_Or; Rewrite Rplus_Ropp_r. +Apply H0. +Apply CV_ALT_step2; Assumption. +Qed. + +(**********) +Lemma CV_ALT_step4 : (Un:nat->R) (Un_decreasing Un) -> (positivity_sui Un) -> (majoree [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N)))). +Intros; Unfold majoree; Unfold bound. +Exists ``(Un O)``. +Unfold is_upper_bound; Intros; Elim H1; Intros. +Rewrite H2; Rewrite decomp_sum. +Replace (tg_alt Un O) with ``(Un O)``. +Pattern 2 ``(Un O)``; Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Apply CV_ALT_step3; Assumption. +Unfold tg_alt; Simpl; Ring. +Apply lt_O_Sn. +Qed. + +(**********) +Lemma pow_1_abs : (n:nat) ``(Rabsolu (pow (-1) n))==1``. +Intro; Induction n. +Simpl; Apply Rabsolu_R1. +Replace (S n) with (plus n (1)); [Rewrite pow_add | Ring]. +Rewrite Rabsolu_mult. +Rewrite Hrecn; Rewrite Rmult_1l; Simpl; Rewrite Rmult_1r; Rewrite Rabsolu_Ropp; Apply Rabsolu_R1. +Qed. + +(* 2m <= 2n => m<=n *) +Lemma le_double : (m,n:nat) (le (mult (2) m) (mult (2) n)) -> (le m n). +Intros; Apply INR_le. +Assert H1 := (le_INR ? ? H). +Do 2 Rewrite mult_INR in H1. +Apply Rle_monotony_contra with ``(INR (S (S O)))``. +Replace (INR (S (S O))) with ``2``; [Apply Rgt_2_0 | Reflexivity]. +Assumption. +Qed. + +(* Ceci donne quasiment le résultat sur la convergence des séries alternées *) +Lemma CV_ALT : (Un:nat->R) (Un_decreasing Un) -> (positivity_sui Un) -> (Un_cv Un R0) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 (tg_alt Un) N) l)). +Intros. +Assert H2 := (CV_ALT_step1 ? H). +Assert H3 := (CV_ALT_step4 ? H H0). +Assert X := (growing_cv ? H2 H3). +Elim X; Intros. +Apply existTT with x. +Unfold Un_cv; Unfold R_dist; Unfold Un_cv in H1; Unfold R_dist in H1; Unfold Un_cv in p; Unfold R_dist in p. +Intros; Cut ``0R;l:R) (Un_growing Un) -> (Un_cv Un l) -> ((n:nat)``(Un n)<=l``). +Intros; Case (total_order_T (Un n) l); Intro. +Elim s; Intro. +Left; Assumption. +Right; Assumption. +Cut ``0<(Un n)-l``. +Intro; Unfold Un_cv in H0; Unfold R_dist in H0. +Elim (H0 ``(Un n)-l`` H1); Intros N1 H2. +Pose N := (max n N1). +Cut ``(Un n)-l<=(Un N)-l``. +Intro; Cut ``(Un N)-l<(Un n)-l``. +Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H3 H4)). +Apply Rle_lt_trans with ``(Rabsolu ((Un N)-l))``. +Apply Rle_Rabsolu. +Apply H2. +Unfold ge N; Apply le_max_r. +Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-l``); Apply Rle_compatibility. +Apply tech9. +Assumption. +Unfold N; Apply le_max_l. +Apply Rlt_anti_compatibility with l. +Rewrite Rplus_Or. +Replace ``l+((Un n)-l)`` with (Un n); [Assumption | Ring]. +Qed. + +(* Un->l => (-Un) -> (-l) *) +Lemma CV_opp : (An:nat->R;l:R) (Un_cv An l) -> (Un_cv (opp_sui 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]. +Apply H1; Assumption. +Qed. + +(**********) +Lemma decreasing_ineq : (Un:nat->R;l:R) (Un_decreasing Un) -> (Un_cv Un l) -> ((n:nat)``l<=(Un n)``). +Intros. +Assert H1 := (decreasing_growing ? H). +Assert H2 := (CV_opp ? ? H0). +Assert H3 := (growing_ineq ? ? H1 H2). +Apply Ropp_Rle. +Unfold opp_sui in H3; Apply H3. +Qed. + +(************************************************) +(* Théorème de convergence des séries alternées *) +(* *) +(* Applications: PI, cos, sin... *) +(************************************************) +Theorem Series_Alternees : (Un:nat->R) (Un_decreasing Un) -> (Un_cv Un R0) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 (tg_alt Un) N) l)). +Intros; Apply CV_ALT. +Assumption. +Unfold positivity_sui; Apply decreasing_ineq; Assumption. +Assumption. +Qed. + +(* Encadrement de la limite par les sommes partielles *) +Theorem sommes_partielles_ineq : (Un:nat->R;l:R;N:nat) (Un_decreasing Un) -> (Un_cv Un R0) -> (Un_cv [N:nat](sum_f_R0 (tg_alt Un) N) l) -> ``(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) N)))<=l<=(sum_f_R0 (tg_alt Un) (mult (S (S O)) N))``. +Intros. +Cut (Un_cv [N:nat](sum_f_R0 (tg_alt Un) (mult (2) N)) l). +Cut (Un_cv [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N))) l). +Intros; Split. +Apply (growing_ineq [N:nat](sum_f_R0 (tg_alt Un) (S (mult (2) N)))). +Apply CV_ALT_step1; Assumption. +Assumption. +Apply (decreasing_ineq [N:nat](sum_f_R0 (tg_alt Un) (mult (2) N))). +Apply CV_ALT_step1_bis; Assumption. +Assumption. +Unfold Un_cv; Unfold R_dist; Unfold Un_cv in H1; Unfold R_dist in H1; Intros. +Elim (H1 eps H2); Intros. +Exists x; Intros. +Apply H3. +Unfold ge; Apply le_trans with (mult (2) n). +Apply le_trans with n. +Assumption. +Assert H5 := (mult_O_le n (2)). +Elim H5; Intro. +Cut ~(O)=(2); [Intro; Elim H7; Symmetry; Assumption | Discriminate]. +Assumption. +Apply le_n_Sn. +Unfold Un_cv; Unfold R_dist; Unfold Un_cv in H1; Unfold R_dist in H1; Intros. +Elim (H1 eps H2); Intros. +Exists x; Intros. +Apply H3. +Unfold ge; Apply le_trans with n. +Assumption. +Assert H5 := (mult_O_le n (2)). +Elim H5; Intro. +Cut ~(O)=(2); [Intro; Elim H7; Symmetry; Assumption | Discriminate]. +Assumption. +Qed. + +(************************************) +(* Application : construction de PI *) +(************************************) + +Definition PI_tg := [n:nat]``/(INR (plus (mult (S (S O)) n) (S O)))``. + +Lemma PI_tg_pos : (n:nat)``0<=(PI_tg n)``. +Intro; Unfold PI_tg; Left; Apply Rlt_Rinv; Apply lt_INR_0; Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Apply lt_O_Sn | Ring]. +Qed. + +Lemma PI_tg_decreasing : (Un_decreasing PI_tg). +Unfold PI_tg Un_decreasing; Intro. +Apply Rle_monotony_contra with ``(INR (plus (mult (S (S O)) n) (S O)))``. +Apply lt_INR_0. +Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Apply lt_O_Sn | Ring]. +Rewrite <- Rinv_r_sym. +Apply Rle_monotony_contra with ``(INR (plus (mult (S (S O)) (S n)) (S O)))``. +Apply lt_INR_0. +Replace (plus (mult (2) (S n)) (1)) with (S (mult (2) (S n))); [Apply lt_O_Sn | Ring]. +Rewrite (Rmult_sym ``(INR (plus (mult (S (S O)) (S n)) (S O)))``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Do 2 Rewrite Rmult_1r; Apply le_INR. +Replace (plus (mult (2) (S n)) (1)) with (S (S (plus (mult (2) n) (1)))). +Apply le_trans with (S (plus (mult (2) n) (1))); Apply le_n_Sn. +Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Apply not_O_INR; Discriminate. +Apply not_O_INR; Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Discriminate | Ring]. +Qed. + +Lemma PI_tg_cv : (Un_cv PI_tg R0). +Unfold Un_cv; Unfold R_dist; Intros. +Cut ``0<2*eps``; [Intro | Apply Rmult_lt_pos; [Apply Rgt_2_0 | Assumption]]. +Assert H1 := (archimed ``/(2*eps)``). +Cut (Zle `0` ``(up (/(2*eps)))``). +Intro; Assert H3 := (IZN ``(up (/(2*eps)))`` H2). +Elim H3; Intros N H4. +Cut (lt O N). +Intro; Exists N; Intros. +Cut (lt O n). +Intro; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_right. +Unfold PI_tg; Apply Rlt_trans with ``/(INR (mult (S (S O)) n))``. +Apply Rlt_monotony_contra with ``(INR (mult (S (S O)) n))``. +Apply lt_INR_0. +Replace (mult (2) n) with (plus n n); [Idtac | Ring]. +Apply lt_le_trans with n. +Assumption. +Apply le_plus_l. +Rewrite <- Rinv_r_sym. +Apply Rlt_monotony_contra with ``(INR (plus (mult (S (S O)) n) (S O)))``. +Apply lt_INR_0. +Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Apply lt_O_Sn | Ring]. +Rewrite (Rmult_sym ``(INR (plus (mult (S (S O)) n) (S O)))``). +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Do 2 Rewrite Rmult_1r; Apply lt_INR. +Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Apply lt_n_Sn | Ring]. +Apply not_O_INR; Replace (plus (mult (2) n) (1)) with (S (mult (2) n)); [Discriminate | Ring]. +Replace n with (S (pred n)). +Apply not_O_INR; Discriminate. +Symmetry; Apply S_pred with O. +Assumption. +Apply Rle_lt_trans with ``/(INR (mult (S (S O)) N))``. +Apply Rle_monotony_contra with ``(INR (mult (S (S O)) N))``. +Rewrite mult_INR; Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply lt_INR_0; Assumption]. +Rewrite <- Rinv_r_sym. +Apply Rle_monotony_contra with ``(INR (mult (S (S O)) n))``. +Rewrite mult_INR; Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply lt_INR_0; Assumption]. +Rewrite (Rmult_sym (INR (mult (S (S O)) n))); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Do 2 Rewrite Rmult_1r; Apply le_INR. +Apply mult_le; Assumption. +Replace n with (S (pred n)). +Apply not_O_INR; Discriminate. +Symmetry; Apply S_pred with O. +Assumption. +Replace N with (S (pred N)). +Apply not_O_INR; Discriminate. +Symmetry; Apply S_pred with O. +Assumption. +Rewrite mult_INR. +Rewrite Rinv_Rmult. +Replace (INR (S (S O))) with ``2``; [Idtac | Reflexivity]. +Apply Rlt_monotony_contra with ``2``. +Apply Rgt_2_0. +Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [Idtac | DiscrR]. +Rewrite Rmult_1l; Apply Rlt_monotony_contra with (INR N). +Apply lt_INR_0; Assumption. +Rewrite <- Rinv_r_sym. +Apply Rlt_monotony_contra with ``/(2*eps)``. +Apply Rlt_Rinv; Assumption. +Rewrite Rmult_1r; Replace ``/(2*eps)*((INR N)*(2*eps))`` with ``(INR N)*((2*eps)*/(2*eps))``; [Idtac | Ring]. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r; Replace (INR N) with (IZR (INZ N)). +Rewrite <- H4. +Elim H1; Intros; Assumption. +Symmetry; Apply INR_IZR_INZ. +Apply prod_neq_R0; [DiscrR | Red; Intro; Rewrite H8 in H; Elim (Rlt_antirefl ? H)]. +Apply not_O_INR. +Red; Intro; Rewrite H8 in H5; Elim (lt_n_n ? H5). +Replace (INR (S (S O))) with ``2``; [DiscrR | Reflexivity]. +Apply not_O_INR. +Red; Intro; Rewrite H8 in H5; Elim (lt_n_n ? H5). +Apply Rle_sym1; Apply PI_tg_pos. +Apply lt_le_trans with N; Assumption. +Elim H1; Intros H5 _. +Assert H6 := (lt_eq_lt_dec O N). +Elim H6; Intro. +Elim a; Intro. +Assumption. +Rewrite <- b in H4. +Rewrite H4 in H5. +Simpl in H5. +Cut ``0 a end)). + +(* We can get an approximation of PI with the following inequality *) +Lemma PI_ineq : (N:nat) ``(sum_f_R0 (tg_alt PI_tg) (S (mult (S (S O)) N)))<=PI/4<=(sum_f_R0 (tg_alt PI_tg) (mult (S (S O)) N))``. +Intro; Apply sommes_partielles_ineq. +Apply PI_tg_decreasing. +Apply PI_tg_cv. +Unfold PI; Case exist_PI; Intro. +Replace ``(4*x)/4`` with x. +Trivial. +Unfold Rdiv; Rewrite (Rmult_sym ``4``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym; [Rewrite Rmult_1r; Reflexivity | DiscrR]. +Qed. + +Lemma PI_RGT_0 : ``0