proposition: Lemma Ratan_CVU' : CVU (fun N x => sum_f_R0 (tg_alt (Ratan_seq x)) N) ps_atan (/2) posreal_half.
proof: Proof. apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) posreal_half); lazy beta. - now intros; apply Ratan_seq_decreasing, Boule_half_to_interval. - now intros; apply Ratan_seq_converging, Boule_half_to_interval. - intros x b; apply Boule_half_to_interval in b. unfold ps_atan; destruct (in_int x) as [inside | outside]; [ | destruct b; case outside; split; lra]. destruct (ps_atan_exists_1 x inside) as [v Pv]. apply Un_cv_ext with (2 := Pv);[reflexivity]. - intros x n b; apply Boule_half_to_interval in b. rewrite <- (Rmult_1_l (PI_tg n)); unfold Ratan_seq, PI_tg. apply Rmult_le_compat_r. { apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); lia. } rewrite <- (pow1 (2 * n + 1)); apply pow_incr; assumption. - exact PI_tg_cv. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia