The hyperbolic distance between two points $z_1, z_2 \in D_1(0)$ is defined as \begin{equation} d(z_1, z_2)= \inf_\gamma \int_0^1 \frac{|\gamma'(t)|} {1- |\gamma(t)|^2} dt \, , \end{equation}where the infimum is taken over all smooth curves $\gamma:[0,1] \to D_1(0)$ joining $z_1$ and $z_2$. Now I want to prove that \begin{equation} d(0,s) = \frac{1}{2} \log \left( \frac{1+s}{1-s}\right) \end{equation} for $s \in [0,1)$.
I think I know where I have to go, since \begin{equation} \int_0^s \frac{1}{1-x^2} dx = \frac{1}{2} \log \left( \frac{1+s}{1-s}\right) \,, \end{equation} but I don't know how to get there. Any ideas?
If you consider a smooth path $\gamma(t)=x(t)$ with $x(t)$ a real function satisfying $x(0)=0$ and $x(1)=s$, you can easily integrate and use the fundamental theorem of calculus to show that $$\int_\gamma \frac{|\gamma '(t)|}{1-|\gamma(t)|^2}dt = \frac{1}{2}\log \left(\frac{1+s}{1-s} \right).$$ Notice that this works for any such smooth path. Now let $\gamma(t) = x(t) + iy(t)$ be a smooth path from $0$ to $s$ with $x(t)$ and $y(t)$ real functions. Then $x'(t) \leq \sqrt{x'(t)^2} \leq \sqrt{x'(t)^2 + y'(t)^2} = |\gamma'(t)|$. Furthermore, $1-x(t)^2 \geq 1-(x(t)^2 + y(t)^2) = 1-|\gamma(t)|^2$ since $x(t)^2 + y(t)^2 \leq 1$. Hence, $$\frac{1}{2}\log \left(\frac{1+s}{1-s} \right) = \int_0^1 \frac{x'(t)}{1-x(t)^2}dt \leq \int_0^1 \frac{|\gamma'(t)|}{1-|\gamma(t)|^2} dt$$ as required.