Harmonic-mean refinement of an asymptotic sequence (source code)

= Harmonic-mean refinement of an asymptotic sequence

For a positive asymptotic sequence $(\phi_n)$, define $\psi_0=\phi_0$ and
$$
\psi_n=\frac{\phi_{n-1}\phi_n}{\phi_{n-1}+\phi_n}.
$$
Then $\psi_n\sim\phi_n$ term by term and $(\psi_n)$ is again an asymptotic sequence.