proposition: Lemma ArTanH_series : forall c : IR, forall (Hs:fun_series_convergent_IR DomArTanH ArTanH_ps) Hc0 Hc1, FSeries_Sum Hs c Hc0[=]ArTanH c Hc1.
proof: Proof. intros c Hs Hc0 Hc1. unfold ArTanH. set (F:=([-C-](Half (R:=IR)){*} ((Logarithm[o][-C-][1]{+}FId){-}(Logarithm[o][-C-][1]{-}FId)))). assert (F0:Dom F c). destruct Hc0 as [A B]. repeat (constructor || exists (I, I)); simpl. apply shift_less_plus'. rstepl ([--][1]:IR). assumption. apply shift_zero_less_minus. assumption. apply eq_transitive with (F c F0). apply (Feq_imp_eq DomArTanH); try assumption. eapply Feq_transitive. apply Feq_symmetric. apply (FSeries_Sum_wd' _ _ _ ArTanH_series_lemma2 Hs ArTanH_series_lemma). assert (B0:maps_compacts_into_weak DomArTanH (olor [0] Two) ([-C-][1]{+}FId)). intros a b Hab H; simpl. exists ([1][+]a); exists ([1][+]b). assert (H0:[1][+]a[<=][1][+]b). apply plus_resp_leEq_lft; assumption. exists H0. split. clear c Hc0 Hc1 F0. intros c [Hc0 Hc1]. split. eapply less_leEq_trans;[|apply Hc0]. destruct (H _ (compact_inc_lft _ _ Hab)) as [A _]. apply shift_less_plus'. rstepl ([--][1]:IR). assumption. eapply leEq_less_trans;[apply Hc1|]. rstepr ([1][+][1]:IR). apply plus_resp_less_lft. destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. assumption. intros x _ [Hx0 Hx1]. split; apply plus_resp_leEq_lft; assumption. assert (A0:fun_series_convergent_IR DomArTanH (fun n : nat => Log_ps n[o]([-C-][1]{+}FId))). apply FSeries_Sum_comp_conv with (olor [0] Two); try apply Log_series_convergent_IR; try Contin. assert (B1:maps_compacts_into_weak DomArTanH (olor [0] Two) ([-C-][1]{-}FId)). intros a b Hab H; simpl. exists ([1][-]b); exists ([1][-]a). assert (H0:[1][-]b[<=][1][-]a). apply plus_resp_leEq_lft. apply inv_resp_leEq; assumption. exists H0. split. clear c Hc0 Hc1 F0. intros c [Hc0 Hc1]. split. eapply less_leEq_trans;[|apply Hc0]. destruct (H _ (compact_inc_rht _ _ Hab)) as [_ A]. apply shift_zero_less_minus. assumption. eapply leEq_less_trans;[apply Hc1|]. rstepr ([1][+][--][--][1]:IR). apply plus_resp_less_lft. apply inv_resp_less. destruct (H _ (compact_inc_lft _ _ Hab)) as [A _]. assumption. intros x _ [Hx0 Hx1]. split; apply plus_resp_leEq_lft; apply inv_resp_leEq; assumption. assert (A1:fun_series_convergent_IR DomArTanH (fun n : nat => Log_ps n[o]([-C-][1]{-}FId))). apply FSeries_Sum_comp_conv with (olor [0] Two); try apply Log_series_convergent_IR; try Contin. assert (A2:fun_series_convergent_IR DomArTanH (fun n : nat => ((Log_ps n[o][-C-][1]{+}FId){-}(Log_ps n[o][-C-][1]{-}FId)))). apply FSeries_Sum_minus_conv; assumption. assert (A3:Feq (olor [0] Two) (FSeries_Sum (J:=olor [0] Two) (f:=Log_ps) Log_series_convergent_IR) Logarithm). split. Included. split. intros x [H _]. assumption. intros; apply Log_series. eapply Feq_transitive. unfold Fscalmult. eapply (FSeries_Sum_scal _ _ A2). Contin. unfold F. apply Feq_mult. apply Feq_reflexive. repeat constructor. eapply Feq_transitive. apply (FSeries_Sum_minus _ _ _ A0 A1). apply Feq_minus. eapply Feq_transitive. apply (FSeries_Sum_comp DomArTanH (olor [0] Two)); try assumption. Contin. assert (X:forall (x : IR) (Hx : Dom ([-C-][1]{+}FId) x), DomArTanH x -> olor [0] Two (([-C-][1]{+}FId) x Hx)). intros x Hx [C0 C1]. simpl; split. apply shift_less_plus'. rstepl ([--][1]:IR). assumption. rstepr ([1][+][1]:IR). apply plus_resp_less_lft. assumption. eapply Feq_comp; try apply A3; try (apply Feq_reflexive; Included); assumption. eapply Feq_transitive. apply (FSeries_Sum_comp DomArTanH (olor [0] Two)); try assumption. Contin. assert (X:forall (x : IR) (Hx : Dom ([-C-][1]{-}FId) x), DomArTanH x -> olor [0] Two (([-C-][1]{-}FId) x Hx)). intros x Hx [C0 C1]. simpl; split. apply shift_less_minus. rstepl (x:IR). assumption. rstepr ([1][-][--][1]:IR). apply plus_resp_less_lft. apply inv_resp_less. assumption. eapply Feq_comp; try apply A3; try (apply Feq_reflexive; Included); assumption. apply: mult_wdr. apply eq_symmetric. apply: Log_div. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac