proposition: Lemma Log_series_convergent_IR : fun_series_convergent_IR (olor [0] Two) Log_ps.
proof: Proof. intros a b Hab Hinc. apply fun_ratio_test_conv. unfold Log_ps; unfold FPowerSeries; Contin. exists 1. pose (c:=Max (AbsIR (a[-][1])) (AbsIR (b[-][1]))). assert (Z0:c[<][1]). unfold c. destruct (Hinc _ (compact_inc_lft _ _ Hab)). destruct (Hinc _ (compact_inc_rht _ _ Hab)). apply Max_less; apply AbsIR_less; first [apply shift_minus_less; rstepr (Two:IR) |apply shift_less_minus; rstepl ([0]:IR)]; assumption. assert (Z1:[0][<=]c). unfold c. eapply leEq_transitive. apply AbsIR_nonneg. apply lft_leEq_Max. exists c. assumption. split. assumption. intros x [Hx0 Hx1] n Hn Hx Hx'. destruct n. exfalso; auto with *. unfold Log_ps, FPowerSeries, Log_series_coef. generalize (nringS_ap_zero IR (S n)). generalize (nringS_ap_zero IR (n)). intros Y0 Y1. stepl ( (nexp IR (S (S n)) (AbsIR (x[-][1])))[/]nring (R:=IR) (S (S n))[//]Y1). apply shift_div_leEq. apply nring_pos; auto with *. stepr ((((nexp IR (S n) (AbsIR (x[-][1]))[*]c)[*](nring (R:=IR) (S (S n))))[/]nring (R:=IR) (S n)[//]Y0)). apply shift_leEq_div. apply nring_pos; auto with *. apply mult_resp_leEq_both. apply (nexp_resp_nonneg _ (AbsIR (x[-][1])) (S (S n))). apply AbsIR_nonneg. apply nring_nonneg; auto with *. change (nexp IR (S (S n)) (AbsIR (x[-][1]))) with ((nexp IR (S n) (AbsIR (x[-][1])))[*](AbsIR (x[-][1]))). apply mult_resp_leEq_lft. apply AbsSmall_imp_AbsIR. split. apply shift_zero_leEq_minus'. rstepr (c[-]([--](x[-][1]))). apply shift_zero_leEq_minus. unfold c. eapply leEq_transitive;[|apply lft_leEq_Max]. eapply leEq_transitive;[|apply inv_leEq_AbsIR]. apply inv_resp_leEq. apply minus_resp_leEq. assumption. unfold c. eapply leEq_transitive;[|apply rht_leEq_Max]. eapply leEq_transitive;[|apply leEq_AbsIR]. apply minus_resp_leEq. assumption. apply (nexp_resp_nonneg _ (AbsIR (x[-][1])) (S n)). apply AbsIR_nonneg. apply nring_leEq; auto with *. rstepl (c[*](nexp IR (S n) (AbsIR (x[-][1]))[/] nring (R:=IR) (S n)[//]Y0)[*]nring (R:=IR) (S (S n))). apply mult_wdl. apply mult_wdr. stepl (AbsIR ((x[-][1])[^](S n))[/]_[//](AbsIR_resp_ap_zero _ Y0)). eapply eq_transitive. apply eq_symmetric. apply (AbsIR_division ((x[-][1])[^]S n) _ Y0). stepr (AbsIR (([--][1])[^](S (S n)))[*]AbsIR ((x[-][1])[^]S n[/]nring (R:=IR) (S n)[//]Y0)). rstepl ([1][*]AbsIR ((x[-][1])[^]S n[/]nring (R:=IR) (S n)[//]Y0)). apply mult_wdl. csetoid_rewrite (AbsIR_nexp_op (S (S n)) ([--][1])). csetoid_replace (AbsIR ([--][1])) ([1]:IR). apply eq_symmetric. apply (one_nexp IR (S (S n))). rstepr ([--][--][1]:IR). apply AbsIR_eq_inv_x. apply shift_zero_leEq_minus'. rstepr ([1]:IR). apply less_leEq; apply pos_one. eapply eq_transitive. apply eq_symmetric; apply AbsIR_resp_mult. apply AbsIR_wd. change ((([--][1][^]S (S n)[/]nring (R:=IR) (S n)[//]Y0){**}(FId{-}[-C-][1]){^}S n) x Hx) with ((([--][1][^]S (S n)[/]nring (R:=IR) (S n)[//]Y0)[*](x[-][1])[^]S n)). rational. apply div_wd. apply (AbsIR_nexp (x[-][1]) (S n)). apply AbsIR_eq_x. apply nring_nonneg. stepl (AbsIR ((x[-][1])[^](S (S n)))[/]_[//](AbsIR_resp_ap_zero _ Y1)). eapply eq_transitive. apply eq_symmetric. apply (AbsIR_division ((x[-][1])[^]S (S n)) _ Y1). stepr (AbsIR (([--][1][^]S (S (S n))[*]((x[-][1])[^]S (S n)[/]_[//]Y1)))). eapply eq_transitive;[|apply eq_symmetric; apply AbsIR_resp_mult]. rstepl ([1][*]AbsIR ((x[-][1])[^]S (S n)[/]nring (R:=IR) (S (S n))[//]Y1)). apply mult_wdl. csetoid_rewrite (AbsIR_nexp_op (S (S (S n))) [--][1]). csetoid_replace (AbsIR ([--][1])) ([1]:IR). apply eq_symmetric. apply (one_nexp IR). rstepr ([--][--][1]:IR). apply AbsIR_eq_inv_x. apply shift_zero_leEq_minus'. rstepr ([1]:IR). apply less_leEq; apply pos_one. apply AbsIR_wd. change ((([--][1][^]S (S (S n))[/]nring (R:=IR) (S (S n))[//]Y1){**}(FId{-}[-C-][1]){^}S (S n)) x Hx') with ((([--][1][^]S (S (S n))[/]nring (R:=IR) (S (S n))[//]Y1)[*](x[-][1])[^]S (S n))). rational. apply div_wd. apply (AbsIR_nexp (x[-][1]) (S (S n))). apply AbsIR_eq_x. apply nring_nonneg. Qed.
imports: CoRN.transc.TaylorSeries