proposition: Lemma Log_series : forall c : IR, forall (Hs:fun_series_convergent_IR (olor [0] Two) Log_ps) Hc0 Hc1, FSeries_Sum Hs c Hc0[=]Log c Hc1.
proof: Proof. intros c Hs Hc0 Hc1. Transparent Logarithm. assert (Z:fun_series_convergent_IR (olor [0] Two) (fun n : nat => Log_ps (S n))). generalize Log_ps Hs. intros p Hp; clear - Hp. intros a b Hab Hinc. destruct (Hp a b Hab Hinc) as [A B]. exists (fun n => (A (S n))). intros e He. destruct (B e He) as [C D]. exists (C). intros m n Hm Hn x Hx. assert (D' := (D (S m) (S n))). stepl (AbsIR (fun_seq_part_sum p (S m) x (contin_imp_inc a b Hab (fun_seq_part_sum p (S m)) (fun_seq_part_sum_cont a b Hab p A (S m)) x Hx)[-] fun_seq_part_sum p (S n) x (contin_imp_inc a b Hab (fun_seq_part_sum p (S n)) (fun_seq_part_sum_cont a b Hab p A (S n)) x Hx))). apply D'; auto with *. apply AbsIR_wd. set (g:=(fun (y n0 : nat) => Part (p n0) x (contin_imp_inc a b Hab (fun_seq_part_sum p y) (fun_seq_part_sum_cont a b Hab p A y) x Hx n0))). set (g':=(fun y n0 : nat => Part (p (S n0)) x (contin_imp_inc a b Hab (fun_seq_part_sum (fun n1 : nat => p (S n1)) y) (fun_seq_part_sum_cont a b Hab (fun n1 : nat => p (S n1)) (fun n1 : nat => A (S n1)) y) x Hx n0))). change (Sum0 (G:=IR) (S m) (g (S m))[-](Sum0 (G:=IR) (S n) (g (S n)))[=] Sum0 (G:=IR) m (g' m)[-]Sum0 (G:=IR) n (g' n)). stepr ((g (S m) 0[+]Sum0 (G:=IR) m (g' m))[-](g (S n) 0[+]Sum0 (G:=IR) n (g' n))). unfold cg_minus. apply eq_symmetric; apply bin_op_wd_unfolded; try apply un_op_wd_unfolded; apply Sum0_shift; intros i; unfold g', g; apply pfwdef; apply eq_reflexive. apply cg_cancel_lft with (g (S n) 0[-](Sum0 (G:=IR) m (g' m)[-]Sum0 (G:=IR) n (g' n))). rstepr (g (S n) 0). rstepl (g (S m) 0). unfold g; apply pfwdef; apply eq_reflexive. assert (Z0:=insert_series_sum _ _ Z). set (Hs':=(insert_series_conv (olor [0] Two) (fun n : nat => Log_ps (S n)) Z)) in *. apply eq_transitive with (FSeries_Sum (J:=olor [0] Two) (f:=insert_series (fun n : nat => Log_ps (S n))) Hs' c Hc0). simpl. apply series_sum_wd. intros [|n]. simpl; rational. simpl; rational. apply eq_transitive with (FSeries_Sum Z c Hc0). apply Feq_imp_eq with (olor [0] Two). apply Feq_symmetric. apply (insert_series_sum _ _ Z). assumption. simpl. unfold series_sum. apply eq_symmetric. apply Limits_unique. simpl. unfold Log, Logarithm. simpl. assert (X:forall n, Continuous_I (Min_leEq_Max [1] c) (([-C-][1]{-}FId){^}n)). Contin. apply Cauchy_Lim_prop2_wd with (fun n => Integral (fun_seq_part_sum_cont _ _ _ _ X n)). assert (A0:Continuous (olor [0] Two) ({1/}FId)). apply Continuous_recip. Contin. intros a b Hab Hinc. split. Included. exists a. destruct (Hinc _ (compact_inc_lft _ _ Hab)); assumption. simpl. intros y _ Hy. stepr y. destruct Hy; assumption. apply eq_symmetric. apply AbsIR_eq_x. apply less_leEq; destruct (Hinc _ Hy); assumption. assert (A1:forall n : nat, Continuous (olor [0] Two) (fun_seq_part_sum (Fnth (R:=IR) ([-C-][1]{-}FId)) n)). intros n. split. repeat constructor. intros a b Hab Hinc. Contin. eapply (limit_of_Integral (olor [0] Two) _ _ A1 A0). unfold fun_seq_part_sum. assert (A2:fun_series_convergent_IR (olor [0] Two) (Fnth (R:=IR) ([-C-][1]{-}FId))). cut (fun_series_convergent_IR (olor [0] Two) (fun n => FId{^}n[o]([-C-][1]{-}FId))). apply fun_series_convergent_wd_IR. intros n. FEQ. intros x Hx. assert (W:Dom ([-C-][1]{-}FId) x). repeat constructor. exists W. repeat constructor. apply FSeries_Sum_comp_conv with (olor [--][1] [1]). intros a b Hab Hinc. exists ([1][-]b). exists ([1][-]a). assert (W:[1][-]b[<=][1][-]a). unfold cg_minus. apply plus_resp_leEq_lft. apply inv_resp_leEq. assumption. exists W. split. intros x [Hx0 Hx1]. split. eapply less_leEq_trans;[|apply Hx0]. apply shift_less_minus. apply shift_plus_less'. rstepr (Two:IR). destruct (Hinc _ (compact_inc_rht _ _ Hab)); assumption. eapply leEq_less_trans;[apply Hx1|]. apply shift_minus_less. apply shift_less_plus'. rstepl ([0]:IR). destruct (Hinc _ (compact_inc_lft _ _ Hab)); assumption. intros x Hx [Hx0 Hx1]. split; simpl. apply shift_leEq_minus'. apply shift_plus_leEq. rstepr b. assumption. apply shift_leEq_minus'. apply shift_plus_leEq. rstepr x. assumption. Contin. apply fun_power_series_conv_IR. assert (A3:Continuous (olor [0] Two) (FSeries_Sum (J:=olor [0] Two) (f:=Fnth (R:=IR) ([-C-][1]{-}FId)) A2)). Contin. eapply (conv_fun_seq'_wdr_IR);[|apply (FSeries_conv _ _ A2 A1 A3)]. FEQ. assert (Y:AbsIR ([1][-]x)[<][1]). destruct X0. apply AbsIR_less. apply shift_minus_less. apply shift_less_plus'. rstepl ([0]:IR); assumption. apply shift_less_minus'. apply shift_plus_less. rstepr (Two:IR); assumption. assert (Y0:[1][-]([1][-]x)[#][0]). rstepl (x). apply Greater_imp_ap. destruct X0; assumption. apply eq_transitive with ([1][/]_[//]Y0). eapply eq_transitive;[|apply (power_series_sum _ Y Y0 (power_series_conv _ Y))]. simpl. apply series_sum_wd. intros n; apply eq_reflexive. simpl. rational. intros x [Hx0 Hx1]. split. apply less_leEq_trans with (Min [1] c); try assumption. apply less_Min; try assumption. apply pos_one. apply leEq_less_trans with (Max [1] c); try assumption. destruct Hc0. apply Max_less; try assumption. apply one_less_two. intros n. induction n. simpl. rstepr ([0][*](c[-][1])). eapply eq_transitive;[|apply (Integral_const _ _ (Min_leEq_Max [1] c) [0] (Continuous_I_const _ _ _ _))]. apply Integral_wd. FEQ. auto with *. simpl. csetoid_rewrite_rev IHn. assert (Y:Continuous_I (Min_leEq_Max [1] c) (([-C-][1]{-}FId){^}n)). Contin. csetoid_replace ((nexp IR n [--][1][*][--][1][*][--][1][/]nring (R:=IR) n[+][1][//] nringS_ap_zero IR n)[*](nexp IR n (c[-][1])[*](c[-][1]))) (Integral Y). assert (Y0:=Continuous_I_plus _ _ _ _ _ (fun_seq_part_sum_cont (Min [1] c) (Max [1] c) (Min_leEq_Max [1] c) (Fnth (R:=IR) ([-C-][1]{-}FId)) X n) Y). stepl (Integral Y0). apply Integral_plus. apply Integral_wd. apply eq_imp_Feq; try Included. intros x Hx; split; constructor. intros x H Hx Hx'. simpl. apply eq_reflexive. rstepl ((nexp IR n [--][1][/]nring (R:=IR) n[+][1][//] nringS_ap_zero IR n)[*](nexp IR n (c[-][1])[*](c[-][1]))). change ((nexp IR n [--][1][/]nring (R:=IR) n[+][1][//]nringS_ap_zero IR n)[*] (nexp IR n (c[-][1])[*](c[-][1]))) with (([--][1][^]n[/]_[//]nringS_ap_zero IR n)[*](c[-][1])[^](S n)). pose (G:=(([--][1][/]_[//]nringS_ap_zero IR n){**}([-C-][1]{-}FId){^}(S n))). assert (X0:Derivative (olor [0] Two) (pos_two IR) G (([-C-][1]{-}FId){^}n)). unfold G. eapply Derivative_wdr; simpl in |- *; [|apply Derivative_scal;refine (Derivative_nth _ _ _ _ _ _);Deriv]. FEQ. repeat constructor. assert (X1:Continuous (olor [0] Two) (([-C-][1]{-}FId){^}n)). Contin. assert (X2:(olor [0] Two [1])). split. apply pos_one. apply one_less_two. eapply eq_transitive. 2:apply eq_symmetric. 2:apply (fun A => Barrow (olor [0] Two) _ X1 _ _ X0 _ _ A X2 Hc0). simpl. rstepr (([--][1][/]nring (R:=IR) n[+][1][//]nringS_ap_zero IR n)[*] (nexp IR n ([1][-]c)[*]([1][-]c))). change (([--][1][^]n[/]_[//]nringS_ap_zero IR n)[*] ((c[-][1])[^](S n))[=] ([--][1][/]_[//]nringS_ap_zero IR n)[*] (([1][-]c)[^](S n))). rstepr (([--][1][/]nring (R:=IR) (S n)[//]nringS_ap_zero IR n)[*] ([--][1][*](c[-][1]))[^]S n). csetoid_rewrite (mult_nexp IR ([--][1]) (c[-][1]) (S n)). simpl. rational. Qed.
imports: CoRN.transc.TaylorSeries