proposition: Lemma ps_atan_continuity_pt_1 : forall eps : R, eps > 0 -> exists alp : R, alp > 0 /\ (forall x, x < 1 -> 0 < x -> Rdist x 1 < alp -> dist R_met (ps_atan x) (Alt_PI/4) < eps).
proof: Proof. intros eps eps_pos. assert (eps_3_pos : eps / 3 > 0) by lra. elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1. unfold Alt_PI. destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field. assert (Pv' : Un_cv (sum_f_R0 (tg_alt (Ratan_seq 1))) v). { apply Un_cv_ext with (2:= Pv). intros; apply sum_eq; intros; unfold tg_alt; rewrite Alt_PI_tg; tauto. } destruct (Pv' (eps / 3) eps_3_pos) as [N2 HN2]. set (N := (N1 + N2)%nat). assert (O_lb : 0 <= 1) by intuition ; assert (O_ub : 1 <= 1) by intuition ; elim (ps_atanSeq_continuity_pt_1 N 1 O_lb O_ub (eps / 3) eps_3_pos) ; intros alpha Halpha ; clear -HN1 HN2 Halpha eps_3_pos; destruct Halpha as (alpha_pos, Halpha). exists alpha ; split;[assumption | ]. intros x x_ub x_lb x_bounds. simpl ; unfold Rdist. replace (ps_atan x - v) with ((ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) N) + (sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N) + (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v)) by ring. apply Rle_lt_trans with (r2:=Rabs (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) N) + Rabs ((sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N) + (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v))). { rewrite Rplus_assoc ; apply Rabs_triang. } replace eps with (2 / 3 * eps + eps / 3) by field. rewrite Rplus_comm. apply Rplus_lt_compat. { apply Rle_lt_trans with (r2 := Rabs (sum_f_R0 (tg_alt (Ratan_seq x)) N - sum_f_R0 (tg_alt (Ratan_seq 1)) N) + Rabs (sum_f_R0 (tg_alt (Ratan_seq 1)) N - v)). { apply Rabs_triang. } apply Rlt_le_trans with (r2:= eps / 3 + eps / 3). { apply Rplus_lt_compat. { simpl in Halpha ; unfold Rdist in Halpha. apply Halpha ; split. { unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. } intuition. } apply HN2; unfold N; lia. } lra. } rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. - unfold N; lia. - lra. - assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia