diff options
Diffstat (limited to 'theories7/Reals/Cos_rel.v')
| -rw-r--r-- | theories7/Reals/Cos_rel.v | 360 |
1 files changed, 0 insertions, 360 deletions
diff --git a/theories7/Reals/Cos_rel.v b/theories7/Reals/Cos_rel.v deleted file mode 100644 index e29825ab..00000000 --- a/theories7/Reals/Cos_rel.v +++ /dev/null @@ -1,360 +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_rel.v,v 1.1.2.1 2004/07/16 19:31:32 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo_def. -V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. -Open Local Scope R_scope. - -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 binomial. -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 unicity_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 unicity_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 := (unicity_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). -Rewrite H1; Reflexivity. -Qed. |