Tetration extension for bases between 1 and eta

[bo198214]

We have now \( f(x+k)-g_k(x+k)\downarrow 0 \) for \( k\to\infty \). But I think that does not directly show the convergence \( f(x) - \log_b^{\circ k} g_k(x+k)\downarrow 0 \).

Any ideas?

Actually I think one can show that \( \log_b^{\circ k} g_k(x+k) \) is strictly increasing with \( k \) because \( \log_b g_k(x+k) \) is concave and hence
\( g_{k-1}(x+k-1) < \log_b g_k(x+k) \) and thatswhy
\( \log_b^{\circ k-1} g_{k-1}(x+k-1)<\log_b^{\circ k} g_{k}(x+k) \)
also it is bounded and hence must have a limit.

But now there is still the question why the limit \( f(x) \) indeed satisfies
\( f(x+1)=b^{f(x)} \)?