Inverse Hyperbolic Tangent Function
The definition of the inverse hyperbolic tangent function.area tangens hyperbolicus
Definition ArTangH : PartIR := ½{**}(Logarithm[o](([-C-]1{+}FId){/}([-C-]1{-}FId))).
Definition DomArTanH := (⋅,⋅) ([--]1) 1.
Lemma proper_DomArTanH : proper DomArTanH.
Lemma DomArTanH_Dom_ArTanH : ⊆ DomArTanH (Dom ArTangH).
Lemma Dom_ArTanH_DomArTanH : ⊆ (Dom ArTangH) DomArTanH.
Definition ArTanH (x:IR) (Hx:DomArTanH x) := ArTangH x (DomArTanH_Dom_ArTanH x Hx).
Lemma ArTanH_wd : forall (x y : IR) Hx Hy, x[=]y -> ArTanH x Hx[=]ArTanH y Hy.
Lemma ArTanH_maps_compact_lemma : maps_compacts_into DomArTanH ((⋅,+∞) 0)
(([-C-]1{+}FId){/}([-C-]1{-}FId)).
Lemma Derivative_ArTanH : forall H, Derivative DomArTanH H ArTangH (Frecip ([-C-]1{-}FId{^}2)).
Included.
Included.
Qed.
Lemma Continuous_ArTanH : Continuous DomArTanH ArTangH.
Properties ofthe Inverse Hyperbolic Tangent Function.
Lemma ArTanH_inv : forall x Hx Hx', ArTanH [--]x Hx[=][--](ArTanH x Hx').
Lemma ArTanH_zero : forall H, ArTanH 0 H[=]0.
PowerSeries for the Inverse Hyperbolic Tangent Function.
Lemma ArTanH_series_coef_lemma : forall (R:COrdField) n, odd n -> (nring (R:=R) n)[#]0.
Definition ArTanH_series_coef (n:nat) :=
match (even_odd_dec n) with
| left _ => 0
| right H => 1[/](nring n)[//](ArTanH_series_coef_lemma IR n H)
end.
Definition ArTanH_ps := FPowerSeries 0 ArTanH_series_coef.
Lemma ArTanH_series_lemma :
forall n : N,
≈ DomArTanH
(½ (R:=IR){**}
((Log_ps n[o][-C-]1{+}FId){-}(Log_ps n[o][-C-]1{-}FId)))
(ArTanH_ps n).
Lemma ArTanH_series_lemma2 :
fun_series_convergent_IR DomArTanH
(fun n : N =>
½ (R:=IR){**}
((Log_ps n[o][-C-]1{+}FId){-}(Log_ps n[o][-C-]1{-}FId))).
Lemma ArTanH_series_convergent_IR : fun_series_convergent_IR DomArTanH ArTanH_ps.
Lemma ArTanH_series : forall c : IR,
forall (Hs:fun_series_convergent_IR DomArTanH ArTanH_ps) Hc0 Hc1,
∑'∞ Hs c Hc0[=]ArTanH c Hc1.
Included.
Qed.
Definition ArTanH_series_coef (n:nat) :=
match (even_odd_dec n) with
| left _ => 0
| right H => 1[/](nring n)[//](ArTanH_series_coef_lemma IR n H)
end.
Definition ArTanH_ps := FPowerSeries 0 ArTanH_series_coef.
Lemma ArTanH_series_lemma :
forall n : N,
≈ DomArTanH
(½ (R:=IR){**}
((Log_ps n[o][-C-]1{+}FId){-}(Log_ps n[o][-C-]1{-}FId)))
(ArTanH_ps n).
Lemma ArTanH_series_lemma2 :
fun_series_convergent_IR DomArTanH
(fun n : N =>
½ (R:=IR){**}
((Log_ps n[o][-C-]1{+}FId){-}(Log_ps n[o][-C-]1{-}FId))).
Lemma ArTanH_series_convergent_IR : fun_series_convergent_IR DomArTanH ArTanH_ps.
Lemma ArTanH_series : forall c : IR,
forall (Hs:fun_series_convergent_IR DomArTanH ArTanH_ps) Hc0 Hc1,
∑'∞ Hs c Hc0[=]ArTanH c Hc1.
Included.
Qed.