proposition: Lemma CVN_R_sin : forall fn:nat -> R -> R, fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)) -> CVN_R fn.
proof: Proof. unfold CVN_R; unfold CVN_r; intros fn H r. exists (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)). cut { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n) l }. { intros (x,p). exists x. split. { apply p. } intros; rewrite H; unfold Rdiv; do 2 rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l. assert (0 < / INR (fact (2 * n + 1))). { apply Rinv_0_lt_compat; apply INR_fact_lt_0. } rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))). apply Rmult_le_compat_l. { left; apply H1. } rewrite <- RPow_abs; apply pow_maj_Rabs. rewrite Rabs_Rabsolu; unfold Boule in H0; rewrite Rminus_0_r in H0; left; apply H0. } assert ((r:R) <> 0). { assert (H0 := cond_pos r); red; intro; rewrite H1 in H0; elim (Rlt_irrefl _ H0). } apply Alembert_C2. { intro; apply Rabs_no_R0. apply prod_neq_R0. { apply Rinv_neq_0_compat; apply INR_fact_neq_0. } apply pow_nonzero; assumption. } assert (H1 := Alembert_sin). unfold sin_n in H1; unfold Un_cv in H1; unfold Un_cv; intros. assert (0 < eps / Rsqr r). { unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption ]. } elim (H1 _ H3); intros N0 H4. exists N0; intros. unfold Rdist; assert (H6 := H4 _ H5). unfold Rdist in H5; replace (Rabs (Rabs (/ INR (fact (2 * S n + 1)) * r ^ (2 * S n)) / Rabs (/ INR (fact (2 * n + 1)) * r ^ (2 * n)))) with (Rsqr r * Rabs ((-1) ^ S n / INR (fact (2 * S n + 1)) / ((-1) ^ n / INR (fact (2 * n + 1))))). { apply Rmult_lt_reg_l with (/ Rsqr r). { apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. } pattern (/ Rsqr r) at 1; rewrite <- (Rabs_right (/ Rsqr r)). 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. } rewrite <- Rabs_mult. rewrite Rmult_minus_distr_l. rewrite Rmult_0_r; rewrite <- Rmult_assoc; rewrite Rinv_l. 2:{ unfold Rsqr; apply prod_neq_R0; assumption. } rewrite Rmult_1_l; rewrite <- (Rmult_comm eps). apply H6. } unfold Rdiv; rewrite (Rmult_comm (Rsqr r)); repeat rewrite Rabs_mult; rewrite Rabs_Rabsolu; rewrite pow_1_abs. rewrite Rmult_1_l. repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l. rewrite Rinv_mult. rewrite Rinv_inv. rewrite Rabs_mult. rewrite Rabs_inv. rewrite pow_1_abs; rewrite Rinv_1; rewrite Rmult_1_l. rewrite Rinv_mult. rewrite <- Rabs_inv. rewrite Rinv_inv. rewrite Rabs_mult. do 2 rewrite Rabs_Rabsolu. rewrite (Rmult_comm (Rabs (r ^ (2 * S n)))). rewrite Rmult_assoc; apply Rmult_eq_compat_l. rewrite Rabs_inv. rewrite Rabs_Rabsolu. repeat rewrite Rabs_right. 2,3:apply Rle_ge; apply pow_le; left; apply (cond_pos r). replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r). 2:{ replace (2 * S n)%nat with (S (S (2 * n)));simpl;ring. } do 2 rewrite <- Rmult_assoc. rewrite Rinv_l. 2:{ apply pow_nonzero; assumption. } unfold Rsqr; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra