diff options
Diffstat (limited to 'theories/Reals/Cos_rel.v')
| -rw-r--r-- | theories/Reals/Cos_rel.v | 420 |
1 files changed, 420 insertions, 0 deletions
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v new file mode 100644 index 00000000..9f76a5ad --- /dev/null +++ b/theories/Reals/Cos_rel.v @@ -0,0 +1,420 @@ +(************************************************************************) +(* 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.12.2.1 2004/07/16 19:31:10 herbelin Exp $ i*) + +Require Import Rbase. +Require Import Rfunctions. +Require Import SeqSeries. +Require Import Rtrigo_def. +Open Local Scope R_scope. + +Definition A1 (x:R) (N:nat) : R := + sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) N. + +Definition B1 (x:R) (N:nat) : R := + sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1)) + N. + +Definition C1 (x y:R) (N:nat) : R := + sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) N. + +Definition Reste1 (x y:R) (N:nat) : R := + sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) * + x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) * + y ^ (2 * (N - l))) (pred (N - k))) (pred N). + +Definition Reste2 (x y:R) (N:nat) : R := + sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) * + x ^ (2 * S (l + k) + 1) * + ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) * + y ^ (2 * (N - l) + 1)) (pred (N - k))) ( + pred N). + +Definition Reste (x y:R) (N:nat) : R := 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 : + forall (x y:R) (n:nat), + (0 < n)%nat -> + 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 in |- *. +rewrite + (cauchy_finite (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) + (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * y ^ (2 * k)) ( + S n)). +rewrite + (cauchy_finite + (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1)) + (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * y ^ (2 * k + 1)) n H) + . +unfold Reste in |- *. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) * + x ^ (2 * S (l + k)) * + ((-1) ^ (S n - l) / INR (fact (2 * (S n - l))) * + y ^ (2 * (S n - l)))) (pred (S n - k))) ( + pred (S n))) with (Reste1 x y (S n)). +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun l:nat => + (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) * + x ^ (2 * S (l + k) + 1) * + ((-1) ^ (n - l) / INR (fact (2 * (n - l) + 1)) * + y ^ (2 * (n - l) + 1))) (pred (n - k))) ( + pred n)) with (Reste2 x y n). +ring. +replace + (sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun p:nat => + (-1) ^ p / INR (fact (2 * p)) * x ^ (2 * p) * + ((-1) ^ (k - p) / INR (fact (2 * (k - p))) * y ^ (2 * (k - p)))) + k) (S n)) with + (sum_f_R0 + (fun k:nat => + (-1) ^ k / INR (fact (2 * k)) * + sum_f_R0 + (fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k) + (S n)). +set + (sin_nnn := + fun n:nat => + match n with + | O => 0 + | S p => + (-1) ^ S p / INR (fact (2 * S p)) * + sum_f_R0 + (fun l:nat => + C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p + end). +replace + (- + sum_f_R0 + (fun k:nat => + sum_f_R0 + (fun p:nat => + (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) * + ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) * + y ^ (2 * (k - p) + 1))) k) n) with (sum_f_R0 sin_nnn (S n)). +rewrite <- sum_plus. +unfold C1 in |- *. +apply sum_eq; intros. +induction i as [| i Hreci]. +simpl in |- *. +rewrite Rplus_0_l. +replace (C 0 0) with 1. +unfold Rdiv in |- *; rewrite Rinv_1. +ring. +unfold C in |- *. +rewrite <- minus_n_n. +simpl in |- *. +unfold Rdiv in |- *; rewrite Rmult_1_r; rewrite Rinv_1; ring. +unfold sin_nnn in |- *. +rewrite <- Rmult_plus_distr_l. +apply Rmult_eq_compat_l. +rewrite binomial. +set (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)). +replace + (sum_f_R0 + (fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l))) + (S i)) with (sum_f_R0 (fun l:nat => Wn (2 * l)%nat) (S i)). +replace + (sum_f_R0 + (fun l:nat => + C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with + (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i). +rewrite Rplus_comm. +apply sum_decomposition. +apply sum_eq; intros. +unfold Wn in |- *. +apply Rmult_eq_compat_l. +replace (2 * S i - S (2 * i0))%nat with (S (2 * (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 (2 * S i)%nat with (S (S (2 * i))). +apply le_n_S. +apply le_trans with (2 * i)%nat. +apply (fun m n p:nat => mult_le_compat_l p n m); 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 in |- *. +apply Rmult_eq_compat_l. +replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat. +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 (fun m n p:nat => mult_le_compat_l p n m); assumption. +assumption. +rewrite <- (Ropp_involutive (sum_f_R0 sin_nnn (S n))). +apply Ropp_eq_compat. +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 0%nat) with 0. +rewrite Rmult_0_l; rewrite Rplus_0_l. +replace (pred (S n)) with n; [ idtac | reflexivity ]. +apply sum_eq; intros. +rewrite Rmult_comm. +unfold sin_nnn in |- *. +rewrite scal_sum. +rewrite scal_sum. +apply sum_eq; intros. +unfold Rdiv in |- *. +repeat rewrite Rmult_assoc. +rewrite (Rmult_comm (/ INR (fact (2 * S i)))). +repeat rewrite <- Rmult_assoc. +rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))). +repeat rewrite <- Rmult_assoc. +replace (/ INR (fact (2 * S i)) * C (2 * S i) (S (2 * i0))) with + (/ INR (fact (2 * i0 + 1)) * / INR (fact (2 * (i - i0) + 1))). +replace (S (2 * i0)) with (2 * i0 + 1)%nat; [ idtac | ring ]. +replace (S (2 * (i - i0))) with (2 * (i - i0) + 1)%nat; [ idtac | ring ]. +replace ((-1) ^ S i) with (-1 * (-1) ^ i0 * (-1) ^ (i - i0)). +ring. +simpl in |- *. +pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat. +rewrite pow_add. +ring. +symmetry in |- *; apply le_plus_minus; assumption. +unfold C in |- *. +unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc. +rewrite <- Rinv_l_sym. +rewrite Rmult_1_l. +rewrite Rinv_mult_distr. +replace (S (2 * i0)) with (2 * i0 + 1)%nat; + [ apply Rmult_eq_compat_l | ring ]. +replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat. +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 (2 * i0 + 1)%nat with (S (2 * i0)). +replace (2 * S i)%nat with (S (S (2 * i))). +apply le_n_S. +apply le_trans with (2 * i)%nat. +apply (fun m n p:nat => mult_le_compat_l p n m); 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 in |- *. +repeat rewrite <- Rmult_assoc. +rewrite <- (Rmult_comm (/ INR (fact (2 * i)))). +repeat rewrite <- Rmult_assoc. +replace (/ INR (fact (2 * i)) * C (2 * i) (2 * i0)) with + (/ INR (fact (2 * i0)) * / INR (fact (2 * (i - i0)))). +replace ((-1) ^ i) with ((-1) ^ i0 * (-1) ^ (i - i0)). +ring. +pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat. +rewrite pow_add. +ring. +symmetry in |- *; apply le_plus_minus; assumption. +unfold C in |- *. +unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc. +rewrite <- Rinv_l_sym. +rewrite Rmult_1_l. +rewrite Rinv_mult_distr. +replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat. +reflexivity. +apply INR_eq. +rewrite mult_INR; repeat rewrite minus_INR. +do 2 rewrite mult_INR; repeat rewrite S_INR; ring. +apply (fun m n p:nat => mult_le_compat_l p n m); assumption. +assumption. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +unfold Reste2 in |- *; apply sum_eq; intros. +apply sum_eq; intros. +unfold Rdiv in |- *; ring. +unfold Reste1 in |- *; apply sum_eq; intros. +apply sum_eq; intros. +unfold Rdiv in |- *; ring. +apply lt_O_Sn. +Qed. + +Lemma pow_sqr : forall (x:R) (i:nat), x ^ (2 * i) = (x * x) ^ i. +intros. +assert (H := pow_Rsqr x i). +unfold Rsqr in H; exact H. +Qed. + +Lemma A1_cvg : forall 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 in |- *; unfold R_dist in |- *; intros. +elim (p eps H1); intros. +exists x1; intros. +unfold A1 in |- *. +replace + (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) n) with + (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * (x * x) ^ i) n). +apply H2; assumption. +apply sum_eq. +intros. +replace ((x * x) ^ i) with (x ^ (2 * i)). +reflexivity. +apply pow_sqr. +unfold cos in |- *. +case (exist_cos (Rsqr x)). +unfold Rsqr in |- *; intros. +unfold cos_in in p_i. +unfold cos_in in c. +apply uniqueness_sum with (fun i:nat => cos_n i * (x * x) ^ i); assumption. +Qed. + +Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (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 in |- *; unfold R_dist in |- *; intros. +elim (p eps H1); intros. +exists x1; intros. +unfold C1 in |- *. +replace + (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) n) + with + (sum_f_R0 + (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * ((x + y) * (x + y)) ^ i) n). +apply H2; assumption. +apply sum_eq. +intros. +replace (((x + y) * (x + y)) ^ i) with ((x + y) ^ (2 * i)). +reflexivity. +apply pow_sqr. +unfold cos in |- *. +case (exist_cos (Rsqr (x + y))). +unfold Rsqr in |- *; intros. +unfold cos_in in p_i. +unfold cos_in in c. +apply uniqueness_sum with (fun i:nat => cos_n i * ((x + y) * (x + y)) ^ i); + assumption. +Qed. + +Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x). +intro. +case (Req_dec x 0); intro. +rewrite H. +rewrite sin_0. +unfold B1 in |- *. +unfold Un_cv in |- *; unfold R_dist in |- *; intros; exists 0%nat; intros. +replace + (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k + 1)) + n) with 0. +unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. +induction n as [| n Hrecn]. +simpl in |- *; ring. +rewrite tech5; rewrite <- Hrecn. +simpl in |- *; ring. +unfold ge in |- *; 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 in |- *; unfold R_dist in |- *; intros. +cut (0 < eps / Rabs x); + [ intro + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ] ]. +elim (p (eps / Rabs x) H3); intros. +exists x1; intros. +unfold B1 in |- *. +replace + (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1)) + n) with + (x * + sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n). +replace + (x * + sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n - + x * x0) with + (x * + (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n - + x0)); [ idtac | ring ]. +rewrite Rabs_mult. +apply Rmult_lt_reg_l with (/ Rabs x). +apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. +rewrite <- Rmult_assoc. +rewrite <- Rinv_l_sym. +rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H4; apply H4; + assumption. +apply Rabs_no_R0; assumption. +rewrite scal_sum. +apply sum_eq. +intros. +rewrite pow_add. +rewrite pow_sqr. +simpl in |- *. +ring. +unfold sin in |- *. +case (exist_sin (Rsqr x)). +unfold Rsqr in |- *; intros. +unfold sin_in in p_i. +unfold sin_in in s. +assert + (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s). +rewrite H1; reflexivity. +Qed.
\ No newline at end of file |