proposition: Lemma Datan_lim : forall x, -1 < x -> x < 1 -> Un_cv (fun N : nat => sum_f_R0 (tg_alt (Datan_seq x)) N) (/ (1 + x ^ 2)).
proof: Proof. intros x x_lb x_ub eps eps_pos. assert (Tool0 : 0 <= x ^ 2) by apply pow2_ge_0. assert (Tool1 : 0 < (1 + x ^ 2)). { solve[apply Rplus_lt_le_0_compat ; intuition]. } assert (Tool2 : / (1 + x ^ 2) > 0). { apply Rinv_0_lt_compat ; tauto. } assert (x_ub2' : 0<= Rabs (x^2) < 1). { rewrite Rabs_pos_eq, <- pow2_abs;[ | apply pow2_ge_0]. apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | lia]. apply Rabs_def1; assumption. } assert (x_ub2 : Rabs (x^2) < 1) by tauto. assert (eps'_pos : ((1 + x^2)*eps) > 0). { apply Rmult_gt_0_compat ; assumption. } elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N. intros n Hn. assert (H1 : - x^2 <> 1). { apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1). assert (t := pow2_ge_0 x); lra. } rewrite Datan_sum_eq. unfold Rdist. assert (tool : forall a b, a / b - /b = (-1 + a) /b). { intros a b; rewrite <- (Rmult_1_l (/b)); unfold Rdiv, Rminus. rewrite <- Ropp_mult_distr_l_reverse, Rmult_plus_distr_r, Rplus_comm. reflexivity. } set (u := 1 + x ^ 2); rewrite tool; unfold Rminus; rewrite <- Rplus_assoc. unfold Rdiv, u. change (-1) with (-(1)). rewrite Rplus_opp_l, Rplus_0_l, Ropp_mult_distr_l_reverse, Rabs_Ropp. rewrite Rabs_mult; clear tool u. assert (tool : forall k, Rabs ((-x ^ 2) ^ k) = Rabs ((x ^ 2) ^ k)). { clear -Tool0; induction k;[simpl; rewrite Rabs_R1;tauto | ]. rewrite <- !(tech_pow_Rmult _ k), !Rabs_mult, Rabs_Ropp, IHk, Rabs_pos_eq. { reflexivity. } exact Tool0. } rewrite tool, (Rabs_pos_eq (/ _)); clear tool;[ | apply Rlt_le; assumption]. assert (tool : forall a b c, 0 < b -> a < b * c -> a * / b < c). { intros a b c bp h; replace c with (b * c * /b). { apply Rmult_lt_compat_r. { apply Rinv_0_lt_compat; assumption. } assumption. } field; apply Rgt_not_eq; exact bp. } apply tool;[exact Tool1 | ]. apply HN; lia. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia