proposition: 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).
proof: Proof. intros. unfold A1, B1. 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)). 2:nia. 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. 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)). 2:{ unfold Reste1; apply sum_eq; intros. apply sum_eq; intros. nra. } 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). 2:{ unfold Reste2; apply sum_eq; intros. apply sum_eq; intros. nra. } 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)). 2:{ apply sum_eq; intros. rewrite scal_sum. apply sum_eq; intros. unfold Rdiv. 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; replace i with (i0 + (i - i0))%nat by nia. rewrite pow_add. ring. } unfold C. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. 2:apply INR_fact_neq_0. rewrite Rmult_1_l. rewrite Rinv_mult. replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat by lia. reflexivity. } pose (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). ring_simplify. unfold Rminus. 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. apply sum_eq; intros. induction i as [| i Hreci]. { unfold C; simpl. nra. } unfold sin_nnn. rewrite <- Rmult_plus_distr_l. apply Rmult_eq_compat_l. rewrite binomial. pose (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)). 2:{ apply sum_eq; intros. unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat by lia. reflexivity. } 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). { apply sum_decomposition. } apply sum_eq; intros. unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))) by lia. reflexivity. - match goal with |- _ = - ?r => replace (- r) with (-1 * r) by ring end. rewrite scal_sum. rewrite decomp_sum. 2:nia. replace (sin_nnn 0%nat) with 0 by reflexivity. rewrite Rplus_0_l. change (pred (S n)) with n. apply sum_eq; intros. rewrite Rmult_comm. unfold sin_nnn. rewrite scal_sum. rewrite scal_sum. apply sum_eq; intros. unfold Rdiv. 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. pattern i at 2; replace i with (i0 + (i - i0))%nat by nia. rewrite pow_add. ring. } unfold C. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. 2:apply INR_fact_neq_0. rewrite Rmult_1_l. rewrite Rinv_mult. 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 by lia. reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Lia Lra