diff options
Diffstat (limited to 'theories7/Reals/Cos_plus.v')
| -rw-r--r-- | theories7/Reals/Cos_plus.v | 1017 |
1 files changed, 0 insertions, 1017 deletions
diff --git a/theories7/Reals/Cos_plus.v b/theories7/Reals/Cos_plus.v deleted file mode 100644 index 481e51bf..00000000 --- a/theories7/Reals/Cos_plus.v +++ /dev/null @@ -1,1017 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Cos_plus.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo_def. -Require Cos_rel. -Require Max. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -V7only [Import R_scope.]. Open Local Scope R_scope. - -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 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 ``(Binomial.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 ``(Binomial.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 Binomial.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 Binomial.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 ``(Binomial.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 ``(Binomial.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 Binomial.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 Binomial.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_sequence 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. |