diff options
Diffstat (limited to 'theories7/Reals/Cos_rel.v')
| -rw-r--r-- | theories7/Reals/Cos_rel.v | 360 |
1 files changed, 360 insertions, 0 deletions
diff --git a/theories7/Reals/Cos_rel.v b/theories7/Reals/Cos_rel.v new file mode 100644 index 00000000..e29825ab --- /dev/null +++ b/theories7/Reals/Cos_rel.v @@ -0,0 +1,360 @@ +(************************************************************************) +(* 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. |