proposition: Lemma PI_2_3_7_ineq : forall N : nat, sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N).
proof: Proof. assert (dec3 : 0 <= /3 <= 1) by (split; lra). assert (dec7 : 0 <= /7 <= 1) by (split; lra). assert (decr : Un_decreasing PI_2_3_7_tg). { apply Ratan_seq_decreasing in dec3. apply Ratan_seq_decreasing in dec7. intros n; apply Rplus_le_compat. { apply Rmult_le_compat_l; [ lra | exact (dec3 n)]. } exact (dec7 n). } assert (cv : Un_cv PI_2_3_7_tg 0). { apply Ratan_seq_converging in dec3. apply Ratan_seq_converging in dec7. intros eps ep. assert (ep' : 0 < eps /3) by lra. destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2]. exists (N1 + N2)%nat; intros n Nn. unfold PI_2_3_7_tg. rewrite <- (Rplus_0_l 0). apply Rle_lt_trans with (1 := Rdist_plus (2 * Ratan_seq (/3) n) 0 (Ratan_seq (/7) n) 0). replace eps with (2 * eps/3 + eps/3) by field. apply Rplus_lt_compat. { unfold Rdist, Rminus, Rdiv. rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. apply (Pn1 n); lia. } apply (Pn2 n); lia. } rewrite Machin_2_3_7. rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); try match goal with id : ~ _ |- _ => case id; split; lra end. destruct (ps_atan_exists_1 (/3)) as [v3 Pv3]. destruct (ps_atan_exists_1 (/7)) as [v7 Pv7]. assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)). { assert (main :Un_cv (fun n => 2 * sum_f_R0 (tg_alt (Ratan_seq (/3))) n + sum_f_R0 (tg_alt (Ratan_seq (/7))) n) (2 * v3 + v7)). { apply CV_plus;[ | assumption]. apply CV_mult;[ | assumption]. exists 0%nat; intros; rewrite Rdist_eq; assumption. } apply Un_cv_ext with (2 := main). intros n; rewrite scal_sum, <- plus_sum; apply sum_eq; intros. rewrite Rmult_comm; unfold PI_2_3_7_tg, tg_alt; field. } intros N; apply (alternated_series_ineq _ _ _ decr cv main). Qed.
imports: Lia Lra Rbase Rtrigo1 Ranalysis_reg Rfunctions AltSeries Rseries SeqProp PartSum Ratan