From ec4e2d514350f79d32c0eb562b3b25864d837b09 Mon Sep 17 00:00:00 2001
From: vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4>
Date: Mon, 18 Dec 2017 14:44:33 +0000
Subject: [doc/algorithms.tex] mpfr_tanh: resolved both FIXME's.

git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@12001 280ebfd0-de03-0410-8827-d642c229c3f4
---
 doc/algorithms.tex | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'doc/algorithms.tex')

diff --git a/doc/algorithms.tex b/doc/algorithms.tex
index 4e2ff3766..bb595c45b 100644
--- a/doc/algorithms.tex
+++ b/doc/algorithms.tex
@@ -1863,35 +1863,35 @@ then the error on $r$ is bounded by $\frac{1}{2} (2^k+1) \ulp(r)$.
 We can thus write $r = (e^{2x}-1) (1+\theta_3)^{2^k+1}$,
 and then $s = \tanh(x) \cdot (1+\theta_4)^{2^k+4}$.
 
-% FIXME: Simplify/improve the lemma since x > 0 and y > 0.
 \begin{lemma}
-For $|x| \leq 1/2$, and $|y| \leq |x|^{-1/2}$, we have:
-\[ |(1+x)^y-1| \leq 2.5 \cdot |y| \cdot |x|. \]
+For $0 < x \leq 1/2$ and $0 < y \leq x^{-1/2}$, we have:
+\[ 0 < (1+x)^y - 1 \leq 1.2 \cdot y \cdot x. \]
 \end{lemma}
 \begin{proof}
-We have $(1+x)^y = e^{y \cdot \log (1+x)}$,
-with $|y \cdot \log (1+x)| \leq |x|^{-1/2} \cdot \left|\log (1+x)\right|$.
-The function $|x|^{-1/2} \cdot \log (1+x)$ is increasing on $[-1/2,1/2]$, and
-takes as values $\approx -0.980$ in $x=-1/2$ and $\approx 0.573$ in $x=1/2$,
-thus is bounded in absolute value by $1$.
-This yields $|y \cdot \log (1+x)| \leq 1$.
-Now it is easy to see that for $|t| \leq 1$, we have
-$|e^t-1| \leq 1.72 |t|$.
-Thus $|(1+x)^y-1| \leq 1.72 \cdot |y| \cdot \left|\log (1+x)\right|$.
-The result follows from $\left|\log (1+x)\right| \leq 1.4 |x|$ for
-$|x| \leq 1/2$, and $1.72 \times 1.4 \leq 2.5$.
+We have $(1+x)^y = e^{y \cdot \log(1+x)}$, with
+$0 < y \cdot \log(1+x) \leq x^{-1/2} \cdot \log(1+x)$.
+The function $x^{-1/2} \cdot \log(1+x)$ is increasing on $]0,1/2]$,
+and reaches $\approx 0.573$ for $x = 1/2$.
+Thus $0 < y \cdot \log(1+x) < 0.574$.
+Now it is easy to see that for $0 < t < 0.574$, we have
+$|e^t-1| \leq 1.4\,t$.
+Thus $0 < (1+x)^y - 1 \leq 1.4 \cdot y \cdot \log(1+x)$.
+The result follows from $\log(1+x) \leq 0.82\,x$ for
+$0 < x \leq 1/2$, and $1.4 \times 0.82 \leq 1.2$.
 \end{proof}
 
+% Because for t > 0 and q >= 1, |(1-t)^q - 1| <= |(1+t)^q - 1|...
+
 Applying the above lemma for $x=2^{-p}$ and $y=2^k+4$,
 assuming $2^k+4 \leq 2^{p/2}$,
 we get $|(1+\theta_4)^{2^k+4} - 1| \leq |(1+2^{-p})^{2^k+4} - 1|
-\leq 2.5 (2^k+4) 2^{-p}$, and thus
-we can write $s = \tanh(x) [1 + 2.5 (2^k+4)\theta_5]$ with
+\leq 1.2 (2^k+4) 2^{-p}$, and thus
+we can write $s = \tanh(x) [1 + 1.2 (2^k+4)\theta_5]$ with
 $|\theta_5| \leq 2^{-p}$.
 Since $2^k+4 \leq 2^{{\rm max}(3,k+1)}$,
-the relative error on $s$ is thus bounded by $2^{{\rm max}(5,k+3)-p}$.
+the relative error on $s$ is thus bounded by $2^{{\rm max}(4,k+2)-p}$.
 
-% FIXME: What about "assuming $2^k+4 \leq 2^{p/2}$"?
+The condition $2^k+4 \leq 2^{p/2}$ is checked in the code.
 
 \subsection{The inverse hyperbolic tangent function}
 
-- 
cgit v1.2.1

