proposition: Lemma CVN_R_cos : forall fn:nat -> R -> R, fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) -> CVN_R fn.
proof: Proof. unfold CVN_R in |- *; intros. assert (hyp_r:(r:R) <> 0). { assert (H0 := cond_pos r); lra. } unfold CVN_r in |- *. exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)). cut { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) n) l }. { intros (x,p). exists x. split. - apply p. - intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult. rewrite pow_1_abs; rewrite Rmult_1_l. assert (0 < / INR (fact (2 * n))). { 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. } 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 (H0 := Alembert_cos). unfold cos_n in H0; unfold Un_cv in H0; unfold Un_cv in |- *; intros. assert (0 < eps / Rsqr r). { unfold Rdiv in |- *; apply Rmult_lt_0_compat. - apply H1. - apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. } elim (H0 _ H2); intros N0 H3. exists N0; intros. unfold Rdist in |- *; assert (H5 := H3 _ H4). unfold Rdist in H5; replace (Rabs (Rabs (/ INR (fact (2 * S n)) * r ^ (2 * S n)) / Rabs (/ INR (fact (2 * n)) * r ^ (2 * n)))) with (Rsqr r * Rabs ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))). { apply Rmult_lt_reg_l with (/ Rsqr r). { apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. } pattern (/ Rsqr r) at 1 in |- *; replace (/ Rsqr r) with (Rabs (/ Rsqr r)). 2:{ rewrite Rabs_inv. rewrite Rabs_right. - reflexivity. - apply Rle_ge; apply Rle_0_sqr. } rewrite <- Rabs_mult; rewrite Rmult_minus_distr_l; rewrite Rmult_0_r; rewrite <- Rmult_assoc; rewrite Rinv_l. 2:{ unfold Rsqr in |- *; apply prod_neq_R0; assumption. } rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); apply H5. } rewrite (Rmult_comm (Rsqr r)); unfold Rdiv in |- *; 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 Rabs_inv. rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l; rewrite <- Rabs_inv. rewrite Rinv_inv. rewrite Rinv_mult. rewrite Rabs_inv. rewrite Rinv_inv. rewrite (Rmult_comm (Rabs (Rabs (r ^ (2 * S n))))); rewrite Rabs_mult; rewrite Rabs_Rabsolu; rewrite Rmult_assoc; apply Rmult_eq_compat_l. rewrite Rabs_inv. do 2 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))) by ring. simpl; ring. } repeat rewrite <- Rmult_assoc; rewrite Rinv_l. 2:{ apply pow_nonzero; assumption. } unfold Rsqr; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg