proposition: Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x).
proof: Proof. intro. case (Req_dec x 0); intro. { rewrite H. rewrite sin_0. unfold B1. unfold Un_cv; unfold Rdist; 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; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. } - induction n as [| n Hrecn]. { simpl; ring. } rewrite tech5; rewrite <- Hrecn. { simpl; ring. } unfold ge; apply Nat.le_0_l. } unfold sin. destruct (exist_sin (Rsqr x)) as (x0,p). unfold sin_in, sin_n, infinite_sum, Rdist in p. unfold Un_cv, Rdist; intros. cut (0 < eps / Rabs x); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ] ]. destruct (p (eps / Rabs x) H1) as (x1,H2). exists x1; intros. unfold B1. 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). 2:{ rewrite scal_sum. apply sum_eq. intros. rewrite pow_add. rewrite pow_sqr. simpl. ring. } 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, Rinv_l, Rmult_1_l, <- (Rmult_comm eps). - apply H2; assumption. - apply Rabs_no_R0; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Lia Lra