Area Tangens Hyperbolicus (artanh)
artanh is implemented by as the GeometricSum of it's taylor series.Lemma arctanSequence_Gs : forall a, GeometricSeries (a^2) (arctanSequence a).
Lemma Qsqr_lt_one : forall (a:Q), (-(1) < a) -> a < 1 -> (a^2 < 1).
Lemma artanh_DomArTanH : forall a, (a^2 < 1) -> DomArTanH (inj_Q IR a).
Although this function works on the entire domain of artanh, it is
only reasonably fast for values close to 0, say [-(2/3), 2/3].
Definition rational_artanh_slow (a:Q) (p1: a^2 < 1) : CR :=
InfiniteGeometricSum (Qsqr_nonneg a) p1 (arctanSequence_Gs a).
Lemma rational_artanh_slow_correct : forall (a:Q) Ha Ha0,
(@rational_artanh_slow a Ha == IRasCR (ArTanH (inj_Q IR a) Ha0))%CR.
InfiniteGeometricSum (Qsqr_nonneg a) p1 (arctanSequence_Gs a).
Lemma rational_artanh_slow_correct : forall (a:Q) Ha Ha0,
(@rational_artanh_slow a Ha == IRasCR (ArTanH (inj_Q IR a) Ha0))%CR.