proposition: Lemma Datan_CVU_prelim : forall c (r : posreal), Rabs c + r < 1 -> CVU (fun N x => sum_f_R0 (tg_alt (Datan_seq x)) N) (fun y : R => / (1 + y ^ 2)) c r.
proof: Proof. intros c r ub_ub eps eps_pos. apply (Alt_CVU (fun x n => Datan_seq n x) (fun x => /(1 + x ^ 2)) (Datan_seq (Rabs c + r)) c r). - intros x inb; apply Datan_seq_decreasing; apply Boule_lt in inb; apply Rabs_def2 in inb; destruct inb; lra. - intros x inb; apply Datan_seq_CV_0; apply Boule_lt in inb; apply Rabs_def2 in inb; destruct inb; lra. - intros x inb; apply (Datan_lim x); apply Boule_lt in inb; apply Rabs_def2 in inb; destruct inb; lra. - intros x [ | n] inb. { solve[unfold Datan_seq; apply Rle_refl]. } rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. { lia. } apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. - apply Datan_seq_CV_0. { apply Rlt_trans with 0;[lra | ]. apply Rplus_le_lt_0_compat. { solve[apply Rabs_pos]. } destruct r; assumption. } assumption. - assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia