diff options
| author | desmettr | 2002-07-12 12:12:05 +0000 |
|---|---|---|
| committer | desmettr | 2002-07-12 12:12:05 +0000 |
| commit | 529130ea378d7da8097ac9729536dc426767e4e9 (patch) | |
| tree | fb04bc388877e58004b41740e3485382835c2d7b | |
| parent | 8ea702c49cc0d6941dd3652ea8a5511fe3c31224 (diff) | |
Preuve de cos_plus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/Cos_plus.v | 1128 | ||||
| -rw-r--r-- | theories/Reals/Cos_rel.v | 382 |
2 files changed, 1510 insertions, 0 deletions
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v new file mode 100644 index 0000000000..6e3e82ff16 --- /dev/null +++ b/theories/Reals/Cos_plus.v @@ -0,0 +1,1128 @@ +(***********************************************************************) +(* 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 Rbase. +Require DiscrR. +Require Rseries. +Require Binome. +Require Rtrigo_def. +Require Rtrigo_alt. +Require Export Rprod. +Require Export Cv_prop. +Require Export Cos_rel. + +Lemma pow_mult : (x:R;n1,n2:nat) (pow x (mult n1 n2))==(pow (pow x n1) n2). +Intros; Induction n2. +Simpl; Replace (mult n1 O) with O; [Reflexivity | Ring]. +Replace (mult n1 (S n2)) with (plus (mult n1 n2) n1). +Replace (S n2) with (plus n2 (1)); [Idtac | Ring]. +Do 2 Rewrite pow_add. +Rewrite Hrecn2. +Simpl. +Ring. +Apply INR_eq; Rewrite plus_INR; Do 2 Rewrite mult_INR; Rewrite S_INR; Ring. +Qed. + +Definition Majxy [x,y:R] : nat->R := [n:nat](Rdiv (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (4) (S n))) (INR (fact n))). + +Lemma Majxy_cv_R0 : (x,y:R) (Un_cv (Majxy x y) R0). +Intros. +Pose C := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))). +Pose C0 := (pow C (4)). +Cut ``0<C``. +Intro. +Cut ``0<C0``. +Intro. +Assert H1 := (cv_speed_pow_fact C0). +Unfold Un_cv in H1; Unfold R_dist in H1. +Unfold Un_cv; Unfold R_dist; Intros. +Cut ``0<eps/C0``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Assumption]]. +Elim (H1 ``eps/C0`` H3); Intros N0 H4. +Exists N0; Intros. +Replace (Majxy x y n) with ``(pow C0 (S n))/(INR (fact n))``. +Simpl. +Apply Rlt_monotony_contra with ``(Rabsolu (/C0))``. +Apply Rabsolu_pos_lt. +Apply Rinv_neq_R0. +Red; Intro; Rewrite H6 in H0; Elim (Rlt_antirefl ? H0). +Rewrite <- Rabsolu_mult. +Unfold Rminus; Rewrite Rmult_Rplus_distr. +Rewrite Ropp_O; Rewrite Rmult_Or. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite (Rabsolu_right ``/C0``). +Rewrite <- (Rmult_sym eps). +Replace ``(pow C0 n)*/(INR (fact n))+0`` with ``(pow C0 n)*/(INR (fact n))-0``; [Idtac | Ring]. +Unfold Rdiv in H4; Apply H4; Assumption. +Apply Rle_sym1; Left; Apply Rlt_Rinv; Assumption. +Red; Intro; Rewrite H6 in H0; Elim (Rlt_antirefl ? H0). +Unfold Majxy. +Unfold C0. +Rewrite pow_mult. +Unfold C; Reflexivity. +Unfold C0; Apply pow_lt; Assumption. +Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C. +Apply RmaxLess1. +Qed. + +Lemma sum_Rle : (An,Bn:nat->R;N:nat) ((n:nat)(le n N)->``(An n)<=(Bn n)``) -> ``(sum_f_R0 An N)<=(sum_f_R0 Bn N)``. +Intros. +Induction N. +Simpl; Apply H. +Apply le_n. +Do 2 Rewrite tech5. +Apply Rle_trans with ``(sum_f_R0 An N)+(Bn (S N))``. +Apply Rle_compatibility. +Apply H. +Apply le_n. +Do 2 Rewrite <- (Rplus_sym ``(Bn (S N))``). +Apply Rle_compatibility. +Apply HrecN. +Intros; Apply H. +Apply le_trans with N; [Assumption | Apply le_n_Sn]. +Qed. + +Lemma sum_Rabsolu : (An:nat->R;N:nat) (Rle (Rabsolu (sum_f_R0 An N)) (sum_f_R0 [l:nat](Rabsolu (An l)) N)). +Intros. +Induction N. +Simpl. +Right; Reflexivity. +Do 2 Rewrite tech5. +Apply Rle_trans with ``(Rabsolu (sum_f_R0 An N))+(Rabsolu (An (S N)))``. +Apply Rabsolu_triang. +Do 2 Rewrite <- (Rplus_sym (Rabsolu (An (S N)))). +Apply Rle_compatibility. +Apply HrecN. +Qed. + +Lemma fact_growing : (m,n:nat) (le m n) -> (le (fact m) (fact n)). +Intros. +Cut (Un_growing [n:nat](INR (fact n))). +Intro. +Apply INR_le. +Apply Rle_sym2. +Apply (growing_prop [l:nat](INR (fact l))). +Exact H0. +Unfold ge; Exact H. +Unfold Un_growing. +Intros. +Simpl. +Rewrite plus_INR. +Pattern 1 (INR (fact n0)); Rewrite <- Rplus_Or. +Apply Rle_compatibility. +Apply pos_INR. +Qed. + +Lemma pow_incr : (x,y:R;n:nat) ``0<=x<=y`` -> ``(pow x n)<=(pow y n)``. +Intros. +Induction n. +Right; Reflexivity. +Simpl. +Elim H; Intros. +Apply Rle_trans with ``y*(pow x n)``. +Do 2 Rewrite <- (Rmult_sym (pow x n)). +Apply Rle_monotony. +Apply pow_le; Assumption. +Assumption. +Apply Rle_monotony. +Apply Rle_trans with x; Assumption. +Apply Hrecn. +Qed. + +Lemma pow_R1_Rle : (x:R;k:nat) ``1<=x`` -> ``1<=(pow x k)``. +Intros. +Induction k. +Right; Reflexivity. +Simpl. +Apply Rle_trans with ``x*1``. +Rewrite Rmult_1r; Assumption. +Apply Rle_monotony. +Left; Apply Rlt_le_trans with R1; [Apply Rlt_R0_R1 | Assumption]. +Exact Hreck. +Qed. + +Lemma Rle_pow : (x:R;m,n:nat) ``1<=x`` -> (le m n) -> ``(pow x m)<=(pow x n)``. +Intros. +Replace n with (plus (minus n m) m). +Rewrite pow_add. +Rewrite Rmult_sym. +Pattern 1 (pow x m); Rewrite <- Rmult_1r. +Apply Rle_monotony. +Apply pow_le; Left; Apply Rlt_le_trans with R1; [Apply Rlt_R0_R1 | Assumption]. +Apply pow_R1_Rle; Assumption. +Rewrite plus_sym. +Symmetry; Apply le_plus_minus; Assumption. +Qed. + +Lemma sum_cte : (x:R;N:nat) (sum_f_R0 [_:nat]x N) == ``x*(INR (S N))``. +Intros. +Induction N. +Simpl; Ring. +Rewrite tech5. +Rewrite HrecN; Repeat Rewrite S_INR; Ring. +Qed. + +Lemma reste1_maj : (x,y:R;N:nat) (lt O N) -> ``(Rabsolu (Reste1 x y N))<=(Majxy x y (pred N))``. +Intros. +Pose C := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))). +Unfold Reste1. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (Rabsolu (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (mult (S (S O)) (S (plus l k)))))* + (pow x (mult (S (S O)) (S (plus l k))))* + (pow ( -1) (minus N l))/ + (INR (fact (mult (S (S O)) (minus N l))))* + (pow y (mult (S (S O)) (minus N l)))`` (pred (minus N k)))) + (pred N)). +Apply (sum_Rabsolu [k:nat] + (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (mult (S (S O)) (S (plus l k)))))* + (pow x (mult (S (S O)) (S (plus l k))))* + (pow ( -1) (minus N l))/ + (INR (fact (mult (S (S O)) (minus N l))))* + (pow y (mult (S (S O)) (minus N l)))`` (pred (minus N k))) (pred N)). +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + (Rabsolu (``(pow ( -1) (S (plus l k)))/ + (INR (fact (mult (S (S O)) (S (plus l k)))))* + (pow x (mult (S (S O)) (S (plus l k))))* + (pow ( -1) (minus N l))/ + (INR (fact (mult (S (S O)) (minus N l))))* + (pow y (mult (S (S O)) (minus N l)))``)) (pred (minus N k))) + (pred N)). +Apply sum_Rle. +Intros. +Apply (sum_Rabsolu [l:nat] + ``(pow ( -1) (S (plus l n)))/ + (INR (fact (mult (S (S O)) (S (plus l n)))))* + (pow x (mult (S (S O)) (S (plus l n))))* + (pow ( -1) (minus N l))/ + (INR (fact (mult (S (S O)) (minus N l))))* + (pow y (mult (S (S O)) (minus N l)))`` (pred (minus N n))). +Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(INR (mult (fact (mult (S (S O)) (S (plus l k)))) (fact (mult (S (S O)) (minus N l)))))*(pow C (mult (S (S O)) (S (plus N k))))`` (pred (minus N k))) (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Unfold Rdiv; Repeat Rewrite Rabsolu_mult. +Do 2 Rewrite pow_1_abs. +Do 2 Rewrite Rmult_1l. +Rewrite (Rabsolu_right ``/(INR (fact (mult (S (S O)) (S (plus n0 n)))))``). +Rewrite (Rabsolu_right ``/(INR (fact (mult (S (S O)) (minus N n0))))``). +Rewrite mult_INR. +Rewrite Rinv_Rmult. +Repeat Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Rewrite <- Rmult_assoc. +Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (minus N n0))))``). +Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Do 2 Rewrite <- Pow_Rabsolu. +Apply Rle_trans with ``(pow (Rabsolu x) (mult (S (S O)) (S (plus n0 n))))*(pow C (mult (S (S O)) (minus N n0)))``. +Apply Rle_monotony. +Apply pow_le; Apply Rabsolu_pos. +Apply pow_incr. +Split. +Apply Rabsolu_pos. +Unfold C. +Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)); Apply RmaxLess2. +Apply Rle_trans with ``(pow C (mult (S (S O)) (S (plus n0 n))))*(pow C (mult (S (S O)) (minus N n0)))``. +Do 2 Rewrite <- (Rmult_sym ``(pow C (mult (S (S O)) (minus N n0)))``). +Apply Rle_monotony. +Apply pow_le. +Apply Rle_trans with R1. +Left; Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Apply pow_incr. +Split. +Apply Rabsolu_pos. +Unfold C; Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). +Apply RmaxLess1. +Apply RmaxLess2. +Right. +Replace (mult (2) (S (plus N n))) with (plus (mult (2) (minus N n0)) (mult (2) (S (plus n0 n)))). +Rewrite pow_add. +Apply Rmult_sym. +Apply INR_eq; Rewrite plus_INR; Do 3 Rewrite mult_INR. +Rewrite minus_INR. +Repeat Rewrite S_INR; Do 2 Rewrite plus_INR; Ring. +Apply le_trans with (pred (minus N n)). +Exact H1. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``/(INR + (mult (fact (mult (S (S O)) (S (plus l k)))) + (fact (mult (S (S O)) (minus N l)))))* + (pow C (mult (S (S (S (S O)))) N))`` (pred (minus N k))) + (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Apply Rle_monotony. +Left; Apply Rlt_Rinv. +Rewrite mult_INR; Apply Rmult_lt_pos; Apply INR_fact_lt_0. +Apply Rle_pow. +Unfold C; Apply RmaxLess1. +Replace (mult (4) N) with (mult (2) (mult (2) N)); [Idtac | Ring]. +Apply mult_le. +Replace (mult (2) N) with (S (plus N (pred N))). +Apply le_n_S. +Apply le_reg_l; Assumption. +Rewrite pred_of_minus. +Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Rewrite minus_INR. +Repeat Rewrite S_INR; Ring. +Apply lt_le_S; Assumption. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``(pow C (mult (S (S (S (S O)))) N))*(Rsqr (/(INR (fact (S (plus N k))))))`` (pred (minus N k))) + (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) N))``). +Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Replace ``/(INR + (mult (fact (mult (S (S O)) (S (plus n0 n)))) + (fact (mult (S (S O)) (minus N n0)))))`` with ``(Binome.C (mult (S (S O)) (S (plus N n))) (mult (S (S O)) (S (plus n0 n))))/(INR (fact (mult (S (S O)) (S (plus N n)))))``. +Apply Rle_trans with ``(Binome.C (mult (S (S O)) (S (plus N n))) (S (plus N n)))/(INR (fact (mult (S (S O)) (S (plus N n)))))``. +Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (S (plus N n)))))``). +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply C_maj. +Apply mult_le. +Apply le_n_S. +Apply le_reg_r. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Right. +Unfold Rdiv; Rewrite Rmult_sym. +Unfold Binome.C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Replace (minus (mult (2) (S (plus N n))) (S (plus N n))) with (S (plus N n)). +Rewrite Rinv_Rmult. +Unfold Rsqr; Reflexivity. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply INR_eq; Rewrite S_INR; Rewrite minus_INR. +Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_2n. +Apply INR_fact_neq_0. +Unfold Rdiv; Rewrite Rmult_sym. +Unfold Binome.C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Replace (minus (mult (2) (S (plus N n))) (mult (2) (S (plus n0 n)))) with (mult (2) (minus N n0)). +Rewrite mult_INR. +Reflexivity. +Apply INR_eq; Rewrite minus_INR. +Do 3 Rewrite mult_INR; Repeat Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite minus_INR. +Ring. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply mult_le. +Apply le_n_S. +Apply le_reg_r. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply INR_fact_neq_0. +Apply Rle_trans with (sum_f_R0 [k:nat]``(INR N)/(INR (fact (S N)))*(pow C (mult (S (S (S (S O)))) N))`` (pred N)). +Apply sum_Rle; Intros. +Rewrite <- (scal_sum [_:nat]``(pow C (mult (S (S (S (S O)))) N))`` (pred (minus N n)) ``(Rsqr (/(INR (fact (S (plus N n))))))``). +Rewrite sum_cte. +Rewrite <- Rmult_assoc. +Do 2 Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) N))``). +Rewrite Rmult_assoc. +Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Apply Rle_trans with ``(Rsqr (/(INR (fact (S (plus N n))))))*(INR N)``. +Apply Rle_monotony. +Apply pos_Rsqr. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_INR. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Rewrite Rmult_sym; Unfold Rdiv; Apply Rle_monotony. +Apply pos_INR. +Apply Rle_trans with ``/(INR (fact (S (plus N n))))``. +Pattern 2 ``/(INR (fact (S (plus N n))))``; Rewrite <- Rmult_1r. +Unfold Rsqr. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply Rle_monotony_contra with ``(INR (fact (S (plus N n))))``. +Apply INR_fact_lt_0. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r. +Replace R1 with (INR (S O)). +Apply le_INR. +Apply lt_le_S. +Apply INR_lt; Apply INR_fact_lt_0. +Reflexivity. +Apply INR_fact_neq_0. +Apply Rle_monotony_contra with ``(INR (fact (S (plus N n))))``. +Apply INR_fact_lt_0. +Rewrite <- Rinv_r_sym. +Apply Rle_monotony_contra with ``(INR (fact (S N)))``. +Apply INR_fact_lt_0. +Rewrite Rmult_1r. +Rewrite (Rmult_sym (INR (fact (S N)))). +Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Apply le_INR. +Apply fact_growing. +Apply le_n_S. +Apply le_plus_l. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Rewrite sum_cte. +Apply Rle_trans with ``(pow C (mult (S (S (S (S O)))) N))/(INR (fact (pred N)))``. +Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) N))``). +Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Cut (S (pred N)) = N. +Intro; Rewrite H0. +Pattern 2 N; Rewrite <- H0. +Do 2 Rewrite fact_simpl. +Rewrite H0. +Repeat Rewrite mult_INR. +Repeat Rewrite Rinv_Rmult. +Rewrite (Rmult_sym ``/(INR (S N))``). +Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l. +Pattern 2 ``/(INR (fact (pred N)))``; Rewrite <- Rmult_1r. +Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply Rle_monotony_contra with (INR (S N)). +Apply lt_INR_0; Apply lt_O_Sn. +Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r; Rewrite Rmult_1l. +Apply le_INR; Apply le_n_Sn. +Apply not_O_INR; Discriminate. +Apply not_O_INR. +Red; Intro; Rewrite H1 in H; Elim (lt_n_n ? H). +Apply not_O_INR. +Red; Intro; Rewrite H1 in H; Elim (lt_n_n ? H). +Apply INR_fact_neq_0. +Apply not_O_INR; Discriminate. +Apply prod_neq_R0. +Apply not_O_INR. +Red; Intro; Rewrite H1 in H; Elim (lt_n_n ? H). +Apply INR_fact_neq_0. +Symmetry; Apply S_pred with O; Assumption. +Right. +Unfold Majxy. +Unfold C. +Replace (S (pred N)) with N. +Reflexivity. +Apply S_pred with O; Assumption. +Qed. + +Lemma reste2_maj : (x,y:R;N:nat) (lt O N) -> ``(Rabsolu (Reste2 x y N))<=(Majxy x y N)``. +Intros. +Pose C := (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))). +Unfold Reste2. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (Rabsolu (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (plus (mult (S (S O)) (S (plus l k))) (S O))))* + (pow x (plus (mult (S (S O)) (S (plus l k))) (S O)))* + (pow ( -1) (minus N l))/ + (INR (fact (plus (mult (S (S O)) (minus N l)) (S O))))* + (pow y (plus (mult (S (S O)) (minus N l)) (S O)))`` (pred (minus N k)))) + (pred N)). +Apply (sum_Rabsolu [k:nat] + (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (plus (mult (S (S O)) (S (plus l k))) (S O))))* + (pow x (plus (mult (S (S O)) (S (plus l k))) (S O)))* + (pow ( -1) (minus N l))/ + (INR (fact (plus (mult (S (S O)) (minus N l)) (S O))))* + (pow y (plus (mult (S (S O)) (minus N l)) (S O)))`` (pred (minus N k))) (pred N)). +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + (Rabsolu (``(pow ( -1) (S (plus l k)))/ + (INR (fact (plus (mult (S (S O)) (S (plus l k))) (S O))))* + (pow x (plus (mult (S (S O)) (S (plus l k))) (S O)))* + (pow ( -1) (minus N l))/ + (INR (fact (plus (mult (S (S O)) (minus N l)) (S O))))* + (pow y (plus (mult (S (S O)) (minus N l)) (S O)))``)) (pred (minus N k))) + (pred N)). +Apply sum_Rle. +Intros. +Apply (sum_Rabsolu [l:nat] + ``(pow ( -1) (S (plus l n)))/ + (INR (fact (plus (mult (S (S O)) (S (plus l n))) (S O))))* + (pow x (plus (mult (S (S O)) (S (plus l n))) (S O)))* + (pow ( -1) (minus N l))/ + (INR (fact (plus (mult (S (S O)) (minus N l)) (S O))))* + (pow y (plus (mult (S (S O)) (minus N l)) (S O)))`` (pred (minus N n))). +Apply Rle_trans with (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``/(INR (mult (fact (plus (mult (S (S O)) (S (plus l k))) (S O))) (fact (plus (mult (S (S O)) (minus N l)) (S O)))))*(pow C (mult (S (S O)) (S (S (plus N k)))))`` (pred (minus N k))) (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Unfold Rdiv; Repeat Rewrite Rabsolu_mult. +Do 2 Rewrite pow_1_abs. +Do 2 Rewrite Rmult_1l. +Rewrite (Rabsolu_right ``/(INR (fact (plus (mult (S (S O)) (S (plus n0 n))) (S O))))``). +Rewrite (Rabsolu_right ``/(INR (fact (plus (mult (S (S O)) (minus N n0)) (S O))))``). +Rewrite mult_INR. +Rewrite Rinv_Rmult. +Repeat Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Rewrite <- Rmult_assoc. +Rewrite <- (Rmult_sym ``/(INR (fact (plus (mult (S (S O)) (minus N n0)) (S O))))``). +Rewrite Rmult_assoc. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Do 2 Rewrite <- Pow_Rabsolu. +Apply Rle_trans with ``(pow (Rabsolu x) (plus (mult (S (S O)) (S (plus n0 n))) (S O)))*(pow C (plus (mult (S (S O)) (minus N n0)) (S O)))``. +Apply Rle_monotony. +Apply pow_le; Apply Rabsolu_pos. +Apply pow_incr. +Split. +Apply Rabsolu_pos. +Unfold C. +Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)); Apply RmaxLess2. +Apply Rle_trans with ``(pow C (plus (mult (S (S O)) (S (plus n0 n))) (S O)))*(pow C (plus (mult (S (S O)) (minus N n0)) (S O)))``. +Do 2 Rewrite <- (Rmult_sym ``(pow C (plus (mult (S (S O)) (minus N n0)) (S O)))``). +Apply Rle_monotony. +Apply pow_le. +Apply Rle_trans with R1. +Left; Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Apply pow_incr. +Split. +Apply Rabsolu_pos. +Unfold C; Apply Rle_trans with (Rmax (Rabsolu x) (Rabsolu y)). +Apply RmaxLess1. +Apply RmaxLess2. +Right. +Replace (mult (2) (S (S (plus N n)))) with (plus (plus (mult (2) (minus N n0)) (S O)) (plus (mult (2) (S (plus n0 n))) (S O))). +Repeat Rewrite pow_add. +Ring. +Apply INR_eq; Repeat Rewrite plus_INR; Do 3 Rewrite mult_INR. +Rewrite minus_INR. +Repeat Rewrite S_INR; Do 2 Rewrite plus_INR; Ring. +Apply le_trans with (pred (minus N n)). +Exact H1. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply Rle_sym1; Left; Apply Rlt_Rinv. +Apply INR_fact_lt_0. +Apply Rle_sym1; Left; Apply Rlt_Rinv. +Apply INR_fact_lt_0. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``/(INR + (mult (fact (plus (mult (S (S O)) (S (plus l k))) (S O))) + (fact (plus (mult (S (S O)) (minus N l)) (S O)))))* + (pow C (mult (S (S (S (S O)))) (S N)))`` (pred (minus N k))) + (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Apply Rle_monotony. +Left; Apply Rlt_Rinv. +Rewrite mult_INR; Apply Rmult_lt_pos; Apply INR_fact_lt_0. +Apply Rle_pow. +Unfold C; Apply RmaxLess1. +Replace (mult (4) (S N)) with (mult (2) (mult (2) (S N))); [Idtac | Ring]. +Apply mult_le. +Replace (mult (2) (S N)) with (S (S (plus N N))). +Repeat Apply le_n_S. +Apply le_reg_l. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply INR_eq; Do 2Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR. +Repeat Rewrite S_INR; Ring. +Apply Rle_trans with (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``(pow C (mult (S (S (S (S O)))) (S N)))*(Rsqr (/(INR (fact (S (S (plus N k)))))))`` (pred (minus N k))) + (pred N)). +Apply sum_Rle; Intros. +Apply sum_Rle; Intros. +Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) (S N)))``). +Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Replace ``/(INR + (mult (fact (plus (mult (S (S O)) (S (plus n0 n))) (S O))) + (fact (plus (mult (S (S O)) (minus N n0)) (S O)))))`` with ``(Binome.C (mult (S (S O)) (S (S (plus N n)))) (plus (mult (S (S O)) (S (plus n0 n))) (S O)))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``. +Apply Rle_trans with ``(Binome.C (mult (S (S O)) (S (S (plus N n)))) (S (S (plus N n))))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``. +Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``). +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply C_maj. +Apply le_trans with (mult (2) (S (S (plus n0 n)))). +Replace (mult (2) (S (S (plus n0 n)))) with (S (plus (mult (2) (S (plus n0 n))) (1))). +Apply le_n_Sn. +Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring. +Apply mult_le. +Repeat Apply le_n_S. +Apply le_reg_r. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Right. +Unfold Rdiv; Rewrite Rmult_sym. +Unfold Binome.C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Replace (minus (mult (2) (S (S (plus N n)))) (S (S (plus N n)))) with (S (S (plus N n))). +Rewrite Rinv_Rmult. +Unfold Rsqr; Reflexivity. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply INR_eq; Do 2 Rewrite S_INR; Rewrite minus_INR. +Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring. +Apply le_n_2n. +Apply INR_fact_neq_0. +Unfold Rdiv; Rewrite Rmult_sym. +Unfold Binome.C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Replace (minus (mult (2) (S (S (plus N n)))) (plus (mult (2) (S (plus n0 n))) (S O))) with (plus (mult (2) (minus N n0)) (S O)). +Rewrite mult_INR. +Reflexivity. +Apply INR_eq; Rewrite minus_INR. +Do 2 Rewrite plus_INR; Do 3 Rewrite mult_INR; Repeat Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite minus_INR. +Ring. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_trans with (mult (2) (S (S (plus n0 n)))). +Replace (mult (2) (S (S (plus n0 n)))) with (S (plus (mult (2) (S (plus n0 n))) (1))). +Apply le_n_Sn. +Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring. +Apply mult_le. +Repeat Apply le_n_S. +Apply le_reg_r. +Apply le_trans with (pred (minus N n)). +Assumption. +Apply le_S_n. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_trans with N. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply le_n_Sn. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply INR_fact_neq_0. +Apply Rle_trans with (sum_f_R0 [k:nat]``(INR N)/(INR (fact (S (S N))))*(pow C (mult (S (S (S (S O)))) (S N)))`` (pred N)). +Apply sum_Rle; Intros. +Rewrite <- (scal_sum [_:nat]``(pow C (mult (S (S (S (S O)))) (S N)))`` (pred (minus N n)) ``(Rsqr (/(INR (fact (S (S (plus N n)))))))``). +Rewrite sum_cte. +Rewrite <- Rmult_assoc. +Do 2 Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) (S N)))``). +Rewrite Rmult_assoc. +Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Apply Rle_trans with ``(Rsqr (/(INR (fact (S (S (plus N n)))))))*(INR N)``. +Apply Rle_monotony. +Apply pos_Rsqr. +Replace (S (pred (minus N n))) with (minus N n). +Apply le_INR. +Apply simpl_le_plus_l with n. +Rewrite <- le_plus_minus. +Apply le_plus_r. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Apply S_pred with O. +Apply simpl_lt_plus_l with n. +Rewrite <- le_plus_minus. +Replace (plus n O) with n; [Idtac | Ring]. +Apply le_lt_trans with (pred N). +Assumption. +Apply lt_pred_n_n; Assumption. +Apply le_trans with (pred N). +Assumption. +Apply le_pred_n. +Rewrite Rmult_sym; Unfold Rdiv; Apply Rle_monotony. +Apply pos_INR. +Apply Rle_trans with ``/(INR (fact (S (S (plus N n)))))``. +Pattern 2 ``/(INR (fact (S (S (plus N n)))))``; Rewrite <- Rmult_1r. +Unfold Rsqr. +Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply Rle_monotony_contra with ``(INR (fact (S (S (plus N n)))))``. +Apply INR_fact_lt_0. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1r. +Replace R1 with (INR (S O)). +Apply le_INR. +Apply lt_le_S. +Apply INR_lt; Apply INR_fact_lt_0. +Reflexivity. +Apply INR_fact_neq_0. +Apply Rle_monotony_contra with ``(INR (fact (S (S (plus N n)))))``. +Apply INR_fact_lt_0. +Rewrite <- Rinv_r_sym. +Apply Rle_monotony_contra with ``(INR (fact (S (S N))))``. +Apply INR_fact_lt_0. +Rewrite Rmult_1r. +Rewrite (Rmult_sym (INR (fact (S (S N))))). +Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Apply le_INR. +Apply fact_growing. +Repeat Apply le_n_S. +Apply le_plus_l. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Rewrite sum_cte. +Apply Rle_trans with ``(pow C (mult (S (S (S (S O)))) (S N)))/(INR (fact N))``. +Rewrite <- (Rmult_sym ``(pow C (mult (S (S (S (S O)))) (S N)))``). +Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony. +Apply pow_le. +Left; Apply Rlt_le_trans with R1. +Apply Rlt_R0_R1. +Unfold C; Apply RmaxLess1. +Cut (S (pred N)) = N. +Intro; Rewrite H0. +Do 2 Rewrite fact_simpl. +Repeat Rewrite mult_INR. +Repeat Rewrite Rinv_Rmult. +Apply Rle_trans with ``(INR (S (S N)))*(/(INR (S (S N)))*(/(INR (S N))*/(INR (fact N))))* + (INR N)``. +Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym (INR N)). +Rewrite (Rmult_sym (INR (S (S N)))). +Apply Rle_monotony. +Repeat Apply Rmult_le_pos. +Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn. +Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn. +Left; Apply Rlt_Rinv. +Apply INR_fact_lt_0. +Apply pos_INR. +Apply le_INR. +Apply le_trans with (S N); Apply le_n_Sn. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_r_sym. +Rewrite Rmult_1l. +Apply Rle_trans with ``/(INR (S N))*/(INR (fact N))*(INR (S N))``. +Repeat Rewrite Rmult_assoc. +Repeat Apply Rle_monotony. +Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Apply le_INR; Apply le_n_Sn. +Rewrite (Rmult_sym ``/(INR (S N))``). +Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r; Right; Reflexivity. +Apply not_O_INR; Discriminate. +Apply not_O_INR; Discriminate. +Apply not_O_INR; Discriminate. +Apply INR_fact_neq_0. +Apply not_O_INR; Discriminate. +Apply prod_neq_R0; [Apply not_O_INR; Discriminate | Apply INR_fact_neq_0]. +Symmetry; Apply S_pred with O; Assumption. +Right. +Unfold Majxy. +Unfold C. +Reflexivity. +Qed. + +Lemma reste1_cv_R0 : (x,y:R) (Un_cv (Reste1 x y) R0). +Intros. +Assert H := (Majxy_cv_R0 x y). +Unfold Un_cv in H; Unfold R_dist in H. +Unfold Un_cv; Unfold R_dist; Intros. +Elim (H eps H0); Intros N0 H1. +Exists (S N0); Intros. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or. +Apply Rle_lt_trans with (Rabsolu (Majxy x y (pred n))). +Rewrite (Rabsolu_right (Majxy x y (pred n))). +Apply reste1_maj. +Apply lt_le_trans with (S N0). +Apply lt_O_Sn. +Assumption. +Apply Rle_sym1. +Unfold Majxy. +Unfold Rdiv; Apply Rmult_le_pos. +Apply pow_le. +Apply Rle_trans with R1. +Left; Apply Rlt_R0_R1. +Apply RmaxLess1. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Replace (Majxy x y (pred n)) with ``(Majxy x y (pred n))-0``; [Idtac | Ring]. +Apply H1. +Unfold ge; Apply le_S_n. +Replace (S (pred n)) with n. +Assumption. +Apply S_pred with O. +Apply lt_le_trans with (S N0); [Apply lt_O_Sn | Assumption]. +Qed. + +Lemma reste2_cv_R0 : (x,y:R) (Un_cv (Reste2 x y) R0). +Intros. +Assert H := (Majxy_cv_R0 x y). +Unfold Un_cv in H; Unfold R_dist in H. +Unfold Un_cv; Unfold R_dist; Intros. +Elim (H eps H0); Intros N0 H1. +Exists (S N0); Intros. +Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or. +Apply Rle_lt_trans with (Rabsolu (Majxy x y n)). +Rewrite (Rabsolu_right (Majxy x y n)). +Apply reste2_maj. +Apply lt_le_trans with (S N0). +Apply lt_O_Sn. +Assumption. +Apply Rle_sym1. +Unfold Majxy. +Unfold Rdiv; Apply Rmult_le_pos. +Apply pow_le. +Apply Rle_trans with R1. +Left; Apply Rlt_R0_R1. +Apply RmaxLess1. +Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. +Replace (Majxy x y n) with ``(Majxy x y n)-0``; [Idtac | Ring]. +Apply H1. +Unfold ge; Apply le_trans with (S N0). +Apply le_n_Sn. +Exact H2. +Qed. + +Lemma reste_cv_R0 : (x,y:R) (Un_cv (Reste x y) R0). +Intros. +Unfold Reste. +Pose An := [n:nat](Reste2 x y n). +Pose Bn := [n:nat](Reste1 x y (S n)). +Cut (Un_cv [n:nat]``(An n)-(Bn n)`` ``0-0``) -> (Un_cv [N:nat]``(Reste2 x y N)-(Reste1 x y (S N))`` ``0``). +Intro. +Apply H. +Apply CV_minus. +Unfold An. +Replace [n:nat](Reste2 x y n) with (Reste2 x y). +Apply reste2_cv_R0. +Reflexivity. +Unfold Bn. +Assert H0 := (reste1_cv_R0 x y). +Unfold Un_cv in H0; Unfold R_dist in H0. +Unfold Un_cv; Unfold R_dist; Intros. +Elim (H0 eps H1); Intros N0 H2. +Exists N0; Intros. +Apply H2. +Unfold ge; Apply le_trans with (S N0). +Apply le_n_Sn. +Apply le_n_S; Assumption. +Unfold An Bn. +Intro. +Replace R0 with ``0-0``; [Idtac | Ring]. +Exact H. +Qed. + +Theorem cos_plus : (x,y:R) ``(cos (x+y))==(cos x)*(cos y)-(sin x)*(sin y)``. +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 C1_cvg. +Unfold Un_cv; Unfold R_dist. +Intros. +Assert H0 := (A1_cvg x). +Assert H1 := (A1_cvg y). +Assert H2 := (B1_cvg x). +Assert H3 := (B1_cvg y). +Assert H4 := (CV_mult ? ? ? ? H0 H1). +Assert H5 := (CV_mult ? ? ? ? H2 H3). +Assert H6 := (reste_cv_R0 x y). +Unfold Un_cv in H4; Unfold Un_cv in H5; Unfold Un_cv in H6. +Unfold R_dist in H4; Unfold R_dist in H5; Unfold R_dist in H6. +Cut ``0<eps/3``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. +Elim (H4 ``eps/3`` H7); Intros N1 H8. +Elim (H5 ``eps/3`` H7); Intros N2 H9. +Elim (H6 ``eps/3`` H7); Intros N3 H10. +Pose N := (S (S (max (max N1 N2) N3))). +Exists N. +Intros. +Cut n = (S (pred n)). +Intro; Rewrite H12. +Rewrite <- cos_plus_form. +Rewrite <- H12. +Apply Rle_lt_trans with ``(Rabsolu ((A1 x n)*(A1 y n)-(cos x)*(cos y)))+(Rabsolu ((sin x)*(sin y)-(B1 x (pred n))*(B1 y (pred n))+(Reste x y (pred n))))``. +Replace ``(A1 x n)*(A1 y n)-(B1 x (pred n))*(B1 y (pred n))+ + (Reste x y (pred n))-((cos x)*(cos y)-(sin x)*(sin y))`` with ``((A1 x n)*(A1 y n)-(cos x)*(cos y))+((sin x)*(sin y)-(B1 x (pred n))*(B1 y (pred n))+(Reste x y (pred n)))``; [Apply Rabsolu_triang | Ring]. +Replace ``eps`` with ``eps/3+(eps/3+eps/3)``. +Apply Rplus_lt. +Apply H8. +Unfold ge; Apply le_trans with N. +Unfold N. +Apply le_trans with (max N1 N2). +Apply le_max_l. +Apply le_trans with (max (max N1 N2) N3). +Apply le_max_l. +Apply le_trans with (S (max (max N1 N2) N3)); Apply le_n_Sn. +Assumption. +Apply Rle_lt_trans with ``(Rabsolu ((sin x)*(sin y)-(B1 x (pred n))*(B1 y (pred n))))+(Rabsolu (Reste x y (pred n)))``. +Apply Rabsolu_triang. +Apply Rplus_lt. +Rewrite <- Rabsolu_Ropp. +Rewrite Ropp_distr2. +Apply H9. +Unfold ge; Apply le_trans with (max N1 N2). +Apply le_max_r. +Apply le_S_n. +Rewrite <- H12. +Apply le_trans with N. +Unfold N. +Apply le_n_S. +Apply le_trans with (max (max N1 N2) N3). +Apply le_max_l. +Apply le_n_Sn. +Assumption. +Replace (Reste x y (pred n)) with ``(Reste x y (pred n))-0``. +Apply H10. +Unfold ge. +Apply le_S_n. +Rewrite <- H12. +Apply le_trans with N. +Unfold N. +Apply le_n_S. +Apply le_trans with (max (max N1 N2) N3). +Apply le_max_r. +Apply le_n_Sn. +Assumption. +Ring. +Pattern 4 eps; Replace eps with ``3*eps/3``. +Ring. +Unfold Rdiv. +Rewrite <- Rmult_assoc. +Apply Rinv_r_simpl_m. +DiscrR. +Apply lt_le_trans with (pred N). +Unfold N; Simpl; Apply lt_O_Sn. +Apply le_S_n. +Rewrite <- H12. +Replace (S (pred N)) with N. +Assumption. +Unfold N; Simpl; Reflexivity. +Cut (lt O N). +Intro. +Cut (lt O n). +Intro. +Apply S_pred with O; Assumption. +Apply lt_le_trans with N; Assumption. +Unfold N; Apply lt_O_Sn. +Qed.
\ No newline at end of file diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v new file mode 100644 index 0000000000..5072e2773f --- /dev/null +++ b/theories/Reals/Cos_rel.v @@ -0,0 +1,382 @@ +(***********************************************************************) +(* 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 Rbase. +Require Rseries. +Require Alembert. +Require Binome. +Require Rtrigo_def. +Require Rtrigo_alt. +Require Export Cauchy_prod. + +Lemma minus_sum : (An,Bn:nat->R;N:nat) (sum_f_R0 [i:nat]``(An i)-(Bn i)`` N)==``(sum_f_R0 An N)-(sum_f_R0 Bn N)``. +Intros; Induction N. +Simpl; Ring. +Do 3 Rewrite tech5; Rewrite HrecN; Ring. +Qed. + +Lemma sum_decomposition : (An:nat->R;N:nat) (Rplus (sum_f_R0 [l:nat](An (mult (2) l)) (S N)) (sum_f_R0 [l:nat](An (S (mult (2) l))) N))==(sum_f_R0 An (mult (2) (S N))). +Intros. +Induction N. +Simpl; Ring. +Rewrite tech5. +Rewrite (tech5 [l:nat](An (S (mult (2) l))) N). +Replace (mult (2) (S (S N))) with (S (S (mult (2) (S N)))). +Rewrite (tech5 An (S (mult (2) (S N)))). +Rewrite (tech5 An (mult (2) (S N))). +Rewrite <- HrecN. +Ring. +Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR;Repeat Rewrite S_INR. +Ring. +Qed. + +Definition A1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))`` N). + +Definition B1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))*(pow x (plus (mult (S (S O)) k) (S O)))`` N). + +Definition C1 [x,y:R] : nat -> R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow (x+y) (mult (S (S O)) k))`` N). + +Definition Reste1 [x,y:R] : nat -> R := [N:nat](sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(pow (-1) (S (plus l k)))/(INR (fact (mult (S (S O)) (S (plus l k)))))*(pow x (mult (S (S O)) (S (plus l k))))*(pow (-1) (minus N l))/(INR (fact (mult (S (S O)) (minus N l))))*(pow y (mult (S (S O)) (minus N l)))`` (pred (minus N k))) (pred N)). + +Definition Reste2 [x,y:R] : nat -> R := [N:nat](sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(pow (-1) (S (plus l k)))/(INR (fact (plus (mult (S (S O)) (S (plus l k))) (S O))))*(pow x (plus (mult (S (S O)) (S (plus l k))) (S O)))*(pow (-1) (minus N l))/(INR (fact (plus (mult (S (S O)) (minus N l)) (S O))))*(pow y (plus (mult (S (S O)) (minus N l)) (S O)))`` (pred (minus N k))) (pred N)). + +Definition Reste [x,y:R] : nat -> R := [N:nat]``(Reste2 x y N)-(Reste1 x y (S N))``. + +(* Here is the main result that will be used to prove that (cos (x+y))=(cos x)(cos y)-(sin x)(sin y) *) +Theorem cos_plus_form : (x,y:R;n:nat) (lt O n) -> ``(A1 x (S n))*(A1 y (S n))-(B1 x n)*(B1 y n)+(Reste x y n)``==(C1 x y (S n)). +Intros. +Unfold A1 B1. +Rewrite (cauchy_finite [k:nat] + ``(pow ( -1) k)/(INR (fact (mult (S (S O)) k)))* + (pow x (mult (S (S O)) k))`` [k:nat] + ``(pow ( -1) k)/(INR (fact (mult (S (S O)) k)))* + (pow y (mult (S (S O)) k))`` (S n)). +Rewrite (cauchy_finite [k:nat] + ``(pow ( -1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))* + (pow x (plus (mult (S (S O)) k) (S O)))`` [k:nat] + ``(pow ( -1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))* + (pow y (plus (mult (S (S O)) k) (S O)))`` n H). +Unfold Reste. +Replace (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (mult (S (S O)) (S (plus l k)))))* + (pow x (mult (S (S O)) (S (plus l k))))* + ((pow ( -1) (minus (S n) l))/ + (INR (fact (mult (S (S O)) (minus (S n) l))))* + (pow y (mult (S (S O)) (minus (S n) l))))`` + (pred (minus (S n) k))) (pred (S n))) with (Reste1 x y (S n)). +Replace (sum_f_R0 + [k:nat] + (sum_f_R0 + [l:nat] + ``(pow ( -1) (S (plus l k)))/ + (INR (fact (plus (mult (S (S O)) (S (plus l k))) (S O))))* + (pow x (plus (mult (S (S O)) (S (plus l k))) (S O)))* + ((pow ( -1) (minus n l))/ + (INR (fact (plus (mult (S (S O)) (minus n l)) (S O))))* + (pow y (plus (mult (S (S O)) (minus n l)) (S O))))`` + (pred (minus n k))) (pred n)) with (Reste2 x y n). +Ring. +Replace (sum_f_R0 + [k:nat] + (sum_f_R0 + [p:nat] + ``(pow ( -1) p)/(INR (fact (mult (S (S O)) p)))* + (pow x (mult (S (S O)) p))*((pow ( -1) (minus k p))/ + (INR (fact (mult (S (S O)) (minus k p))))* + (pow y (mult (S (S O)) (minus k p))))`` k) (S n)) with (sum_f_R0 [k:nat](Rmult ``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))`` (sum_f_R0 [l:nat]``(C (mult (S (S O)) k) (mult (S (S O)) l))*(pow x (mult (S (S O)) l))*(pow y (mult (S (S O)) (minus k l)))`` k)) (S n)). +Pose sin_nnn := [n:nat]Cases n of O => R0 | (S p) => (Rmult ``(pow (-1) (S p))/(INR (fact (mult (S (S O)) (S p))))`` (sum_f_R0 [l:nat]``(C (mult (S (S O)) (S p)) (S (mult (S (S O)) l)))*(pow x (S (mult (S (S O)) l)))*(pow y (S (mult (S (S O)) (minus p l))))`` p)) end. +Replace (Ropp (sum_f_R0 + [k:nat] + (sum_f_R0 + [p:nat] + ``(pow ( -1) p)/ + (INR (fact (plus (mult (S (S O)) p) (S O))))* + (pow x (plus (mult (S (S O)) p) (S O)))* + ((pow ( -1) (minus k p))/ + (INR (fact (plus (mult (S (S O)) (minus k p)) (S O))))* + (pow y (plus (mult (S (S O)) (minus k p)) (S O))))`` k) + n)) with (sum_f_R0 sin_nnn (S n)). +Rewrite <- sum_plus. +Unfold C1. +Apply sum_eq; Intros. +Induction i. +Simpl. +Rewrite Rplus_Ol. +Replace (C O O) with R1. +Unfold Rdiv; Rewrite Rinv_R1. +Ring. +Unfold C. +Rewrite <- minus_n_n. +Simpl. +Unfold Rdiv; Rewrite Rmult_1r; Rewrite Rinv_R1; Ring. +Unfold sin_nnn. +Rewrite <- Rmult_Rplus_distr. +Apply Rmult_mult_r. +Rewrite binome. +Pose Wn := [i0:nat]``(C (mult (S (S O)) (S i)) i0)*(pow x i0)* + (pow y (minus (mult (S (S O)) (S i)) i0))``. +Replace (sum_f_R0 + [l:nat] + ``(C (mult (S (S O)) (S i)) (mult (S (S O)) l))* + (pow x (mult (S (S O)) l))* + (pow y (mult (S (S O)) (minus (S i) l)))`` (S i)) with (sum_f_R0 [l:nat](Wn (mult (2) l)) (S i)). +Replace (sum_f_R0 + [l:nat] + ``(C (mult (S (S O)) (S i)) (S (mult (S (S O)) l)))* + (pow x (S (mult (S (S O)) l)))* + (pow y (S (mult (S (S O)) (minus i l))))`` i) with (sum_f_R0 [l:nat](Wn (S (mult (2) l))) i). +Rewrite Rplus_sym. +Apply sum_decomposition. +Apply sum_eq; Intros. +Unfold Wn. +Apply Rmult_mult_r. +Replace (minus (mult (2) (S i)) (S (mult (2) i0))) with (S (mult (2) (minus i i0))). +Reflexivity. +Apply INR_eq. +Rewrite S_INR; Rewrite mult_INR. +Repeat Rewrite minus_INR. +Rewrite mult_INR; Repeat Rewrite S_INR. +Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Replace (mult (2) (S i)) with (S (S (mult (2) i))). +Apply le_n_S. +Apply le_trans with (mult (2) i). +Apply mult_le; Assumption. +Apply le_n_Sn. +Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Assumption. +Apply sum_eq; Intros. +Unfold Wn. +Apply Rmult_mult_r. +Replace (minus (mult (2) (S i)) (mult (2) i0)) with (mult (2) (minus (S i) i0)). +Reflexivity. +Apply INR_eq. +Rewrite mult_INR. +Repeat Rewrite minus_INR. +Rewrite mult_INR; Repeat Rewrite S_INR. +Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Apply mult_le; Assumption. +Assumption. +Rewrite <- (Ropp_Ropp (sum_f_R0 sin_nnn (S n))). +Apply eq_Ropp. +Replace ``-(sum_f_R0 sin_nnn (S n))`` with ``-1*(sum_f_R0 sin_nnn (S n))``; [Idtac | Ring]. +Rewrite scal_sum. +Rewrite decomp_sum. +Replace (sin_nnn O) with R0. +Rewrite Rmult_Ol; Rewrite Rplus_Ol. +Replace (pred (S n)) with n; [Idtac | Reflexivity]. +Apply sum_eq; Intros. +Rewrite Rmult_sym. +Unfold sin_nnn. +Rewrite scal_sum. +Rewrite scal_sum. +Apply sum_eq; Intros. +Unfold Rdiv. +Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym ``/(INR (fact (mult (S (S O)) (S i))))``). +Repeat Rewrite <- Rmult_assoc. +Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (S i))))``). +Repeat Rewrite <- Rmult_assoc. +Replace ``/(INR (fact (mult (S (S O)) (S i))))* + (C (mult (S (S O)) (S i)) (S (mult (S (S O)) i0)))`` with ``/(INR (fact (plus (mult (S (S O)) i0) (S O))))*/(INR (fact (plus (mult (S (S O)) (minus i i0)) (S O))))``. +Replace (S (mult (2) i0)) with (plus (mult (2) i0) (1)); [Idtac | Ring]. +Replace (S (mult (2) (minus i i0))) with (plus (mult (2) (minus i i0)) (1)); [Idtac | Ring]. +Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i0)*(pow (-1) (minus i i0))``. +Ring. +Simpl. +Pattern 2 i; Replace i with (plus i0 (minus i i0)). +Rewrite pow_add. +Ring. +Symmetry; Apply le_plus_minus; Assumption. +Unfold C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite Rinv_Rmult. +Replace (S (mult (S (S O)) i0)) with (plus (mult (2) i0) (1)); [Apply Rmult_mult_r | Ring]. +Replace (minus (mult (2) (S i)) (plus (mult (2) i0) (1))) with (plus (mult (2) (minus i i0)) (1)). +Reflexivity. +Apply INR_eq. +Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite minus_INR. +Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Replace (plus (mult (2) i0) (1)) with (S (mult (2) i0)). +Replace (mult (2) (S i)) with (S (S (mult (2) i))). +Apply le_n_S. +Apply le_trans with (mult (2) i). +Apply mult_le; Assumption. +Apply le_n_Sn. +Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Assumption. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Reflexivity. +Apply lt_O_Sn. +Apply sum_eq; Intros. +Rewrite scal_sum. +Apply sum_eq; Intros. +Unfold Rdiv. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) i)))``). +Repeat Rewrite <- Rmult_assoc. +Replace ``/(INR (fact (mult (S (S O)) i)))* + (C (mult (S (S O)) i) (mult (S (S O)) i0))`` with ``/(INR (fact (mult (S (S O)) i0)))*/(INR (fact (mult (S (S O)) (minus i i0))))``. +Replace ``(pow (-1) i)`` with ``(pow (-1) i0)*(pow (-1) (minus i i0))``. +Ring. +Pattern 2 i; Replace i with (plus i0 (minus i i0)). +Rewrite pow_add. +Ring. +Symmetry; Apply le_plus_minus; Assumption. +Unfold C. +Unfold Rdiv; Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Rewrite Rinv_Rmult. +Replace (minus (mult (2) i) (mult (2) i0)) with (mult (2) (minus i i0)). +Reflexivity. +Apply INR_eq. +Rewrite mult_INR; Repeat Rewrite minus_INR. +Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. +Apply mult_le; Assumption. +Assumption. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Unfold Reste2; Apply sum_eq; Intros. +Apply sum_eq; Intros. +Unfold Rdiv; Ring. +Unfold Reste1; Apply sum_eq; Intros. +Apply sum_eq; Intros. +Unfold Rdiv; Ring. +Apply lt_O_Sn. +Qed. + +Lemma pow_sqr : (x:R;i:nat) (pow x (mult (2) i))==(pow ``x*x`` i). +Intros. +Assert H := (pow_Rsqr x i). +Unfold Rsqr in H; Exact H. +Qed. + +Lemma A1_cvg : (x:R) (Un_cv (A1 x) (cos x)). +Intro. +Assert H := (exist_cos ``x*x``). +Elim H; Intros. +Assert p_i := p. +Unfold cos_in in p. +Unfold cos_n infinit_sum in p. +Unfold R_dist in p. +Cut ``(cos x)==x0``. +Intro. +Rewrite H0. +Unfold Un_cv; Unfold R_dist; Intros. +Elim (p eps H1); Intros. +Exists x1; Intros. +Unfold A1. +Replace (sum_f_R0 ([k:nat]``(pow ( -1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))``) n) with (sum_f_R0 ([i:nat]``(pow ( -1) i)/(INR (fact (mult (S (S O)) i)))*(pow (x*x) i)``) n). +Apply H2; Assumption. +Apply sum_eq. +Intros. +Replace ``(pow (x*x) i)`` with ``(pow x (mult (S (S O)) i))``. +Reflexivity. +Apply pow_sqr. +Unfold cos. +Case (exist_cos (Rsqr x)). +Unfold Rsqr; Intros. +Unfold cos_in in p_i. +Unfold cos_in in c. +Apply unicite_sum with [i:nat]``(cos_n i)*(pow (x*x) i)``; Assumption. +Qed. + +Lemma C1_cvg : (x,y:R) (Un_cv (C1 x y) (cos (Rplus x y))). +Intros. +Assert H := (exist_cos ``(x+y)*(x+y)``). +Elim H; Intros. +Assert p_i := p. +Unfold cos_in in p. +Unfold cos_n infinit_sum in p. +Unfold R_dist in p. +Cut ``(cos (x+y))==x0``. +Intro. +Rewrite H0. +Unfold Un_cv; Unfold R_dist; Intros. +Elim (p eps H1); Intros. +Exists x1; Intros. +Unfold C1. +Replace (sum_f_R0 ([k:nat]``(pow ( -1) k)/(INR (fact (mult (S (S O)) k)))*(pow (x+y) (mult (S (S O)) k))``) n) with (sum_f_R0 ([i:nat]``(pow ( -1) i)/(INR (fact (mult (S (S O)) i)))*(pow ((x+y)*(x+y)) i)``) n). +Apply H2; Assumption. +Apply sum_eq. +Intros. +Replace ``(pow ((x+y)*(x+y)) i)`` with ``(pow (x+y) (mult (S (S O)) i))``. +Reflexivity. +Apply pow_sqr. +Unfold cos. +Case (exist_cos (Rsqr ``x+y``)). +Unfold Rsqr; Intros. +Unfold cos_in in p_i. +Unfold cos_in in c. +Apply unicite_sum with [i:nat]``(cos_n i)*(pow ((x+y)*(x+y)) i)``; Assumption. +Qed. + +Lemma B1_cvg : (x:R) (Un_cv (B1 x) (sin x)). +Intro. +Case (Req_EM x R0); Intro. +Rewrite H. +Rewrite sin_0. +Unfold B1. +Unfold Un_cv; Unfold R_dist; Intros; Exists O; Intros. +Replace (sum_f_R0 ([k:nat]``(pow ( -1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))*(pow 0 (plus (mult (S (S O)) k) (S O)))``) n) with R0. +Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Induction n. +Simpl; Ring. +Rewrite tech5; Rewrite <- Hrecn. +Simpl; Ring. +Unfold ge; Apply le_O_n. +Assert H0 := (exist_sin ``x*x``). +Elim H0; Intros. +Assert p_i := p. +Unfold sin_in in p. +Unfold sin_n infinit_sum in p. +Unfold R_dist in p. +Cut ``(sin x)==x*x0``. +Intro. +Rewrite H1. +Unfold Un_cv; Unfold R_dist; Intros. +Cut ``0<eps/(Rabsolu x)``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption]]. +Elim (p ``eps/(Rabsolu x)`` H3); Intros. +Exists x1; Intros. +Unfold B1. +Replace (sum_f_R0 ([k:nat]``(pow ( -1) k)/(INR (fact (plus (mult (S (S O)) k) (S O))))*(pow x (plus (mult (S (S O)) k) (S O)))``) n) with (Rmult x (sum_f_R0 ([i:nat]``(pow ( -1) i)/(INR (fact (plus (mult (S (S O)) i) (S O))))*(pow (x*x) i)``) n)). +Replace (Rminus (Rmult x (sum_f_R0 ([i:nat]``(pow ( -1) i)/(INR (fact (plus (mult (S (S O)) i) (S O))))*(pow (x*x) i)``) n)) (Rmult x x0)) with (Rmult x (Rminus (sum_f_R0 ([i:nat]``(pow ( -1) i)/(INR (fact (plus (mult (S (S O)) i) (S O))))*(pow (x*x) i)``) n) x0)); [Idtac | Ring]. +Rewrite Rabsolu_mult. +Apply Rlt_monotony_contra with ``/(Rabsolu x)``. +Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. +Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H4; Apply H4; Assumption. +Apply Rabsolu_no_R0; Assumption. +Rewrite scal_sum. +Apply sum_eq. +Intros. +Rewrite pow_add. +Rewrite pow_sqr. +Simpl. +Ring. +Unfold sin. +Case (exist_sin (Rsqr x)). +Unfold Rsqr; Intros. +Unfold sin_in in p_i. +Unfold sin_in in s. +Assert H1 := (unicite_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). +Rewrite H1; Reflexivity. +Qed.
\ No newline at end of file |