proposition: Lemma arctan_series_convergent_IR : fun_series_convergent_IR (olor ([--][1]) [1]) (fun (i:nat) => (([--][1])[^]i[/]nring (S (2*i))[//]nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1)).
proof: Proof. intros y z Hyz Hinc. pose (C:=Max (AbsIR y) (AbsIR z)). assert (C[<][1]). unfold C. destruct (Hinc _ (compact_inc_lft _ _ Hyz)). destruct (Hinc _ (compact_inc_rht _ _ Hyz)). apply Max_less; apply AbsIR_less; assumption. assert ([0][<=]C). unfold C. eapply leEq_transitive. apply AbsIR_nonneg. apply lft_leEq_Max. apply fun_ratio_test_conv. intros n. Contin. exists 0. exists C. assumption. split. assumption. intros x Hx n _ Hx0 Hx1. generalize (nringS_ap_zero IR (2 * S n)). generalize (nringS_ap_zero IR (2 * n)). intros Z0 Z1. set (a := S (2 * S n)). set (b := 2*S n + 1). set (c:= S (2 * n)). set (d:= 2*n + 1). change (AbsIR (([--][1][^]S n[/]nring (R:=IR) a[//]Z1)[*]x[^]b)[<=] C[*]AbsIR (([--][1][^]n[/]nring (R:=IR) c[//]Z0)[*]x[^]d)). stepl (AbsIR (([--][1][^]S n[/]nring (R:=IR) a[//]Z1))[*]AbsIR (x[^]b)); [| now apply eq_symmetric; apply AbsIR_resp_mult]. stepr (C[*](AbsIR (([--][1][^]n[/]nring (R:=IR) c[//]Z0))[*]AbsIR(x[^]d))); [| now apply mult_wdr; apply eq_symmetric; apply AbsIR_resp_mult]. rstepr (AbsIR (([--][1][^]n[/]nring (R:=IR) c[//]Z0))[*](C[*]AbsIR(x[^]d))). apply mult_resp_leEq_both; try apply AbsIR_nonneg. stepl (AbsIR ([--][1][^]S n)[/]_[//](AbsIR_resp_ap_zero _ Z1)); [| now apply eq_symmetric; apply AbsIR_division]. stepr ((AbsIR ([--][1][^]n)[/]_[//](AbsIR_resp_ap_zero _ Z0))); [| now apply eq_symmetric; apply AbsIR_division]. assert (H0:forall n, AbsIR([--][1][^]n)[=][1]). intros i. csetoid_rewrite (AbsIR_nexp_op i ([--][1]:IR)). csetoid_rewrite_rev (AbsIR_inv [1]). stepl (([1]:IR)[^]i). apply one_nexp. apply nexp_wd. apply eq_symmetric; apply AbsIR_eq_x. apply less_leEq; apply pos_one. stepl ([1][/]AbsIR (nring (R:=IR) (S (2 * S n)))[//] AbsIR_resp_ap_zero (nring (R:=IR) (S (2 * S n))) Z1); [| now apply div_wd; try apply eq_reflexive; apply eq_symmetric; apply H0]. stepr ([1][/]AbsIR (nring (R:=IR) (S (2 * n)))[//] AbsIR_resp_ap_zero (nring (R:=IR) (S (2 * n))) Z0); [| now apply div_wd; try apply eq_reflexive; apply eq_symmetric; apply H0]. apply recip_resp_leEq; try (apply AbsIR_pos; assumption). eapply leEq_transitive;[|apply leEq_AbsIR]. apply AbsSmall_imp_AbsIR. apply leEq_imp_AbsSmall. apply nring_nonneg. apply nring_leEq. auto with *. replace b with (2+d);[|unfold b, d; auto with *]. stepl (AbsIR x[^](2+d)); [| now apply eq_symmetric; apply AbsIR_nexp_op]. stepl (AbsIR x[^]2[*]AbsIR x[^]d); [| now apply nexp_plus]. stepr (C[*]AbsIR x[^]d); [| now apply mult_wdr; apply eq_symmetric; apply AbsIR_nexp_op]. apply mult_resp_leEq_rht; try (apply nexp_resp_nonneg; apply AbsIR_nonneg). apply leEq_transitive with (C[^]2). stepl (AbsIR(x[^]2)); [| now apply AbsIR_nexp_op]. stepl (x[^]2); [| now apply eq_symmetric; apply AbsIR_eq_x; apply sqr_nonneg]. apply shift_zero_leEq_minus'. rstepr ((C[-]x)[*](C[-][--]x)). unfold C. destruct Hx as [Y0 Y1]. apply mult_resp_nonneg; apply shift_zero_leEq_minus. eapply leEq_transitive. apply Y1. eapply leEq_transitive. apply leEq_AbsIR. apply rht_leEq_Max. eapply leEq_transitive. apply inv_resp_leEq. apply Y0. eapply leEq_transitive. apply inv_leEq_AbsIR. apply lft_leEq_Max. rstepl (C[*]C). rstepr (C[*][1]). apply mult_resp_leEq_lft. apply less_leEq; assumption. assumption. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac