A nice series for b^^h , base sqrt(2), by diagonalization

[bo198214]

I attempted a proof this way. Don't know, whether this is sufficient...

If you write it from bottom up Ok, let me verify. We want to prove:
\( \lim_{\delta\to 0+}b[4]\delta - \log_b(\delta) = \lim_{n\to\infty} {\exp_b}^{\circ n}=:t \)
for each tetration [4] and \( 1<b\le e^{1/e} \).

First tetration should be differentiable at -1. As b[4](-1)=0 this means
\( \lim_{\delta \to 0+} \frac{b[4](\delta-1)}{\delta} = \left.\frac{\partial b[4]x}{\partial x}\right|_{x=-1}=:c>0 \)
then we can take on both sides the logarithm \( \log_b \), which is a continous function and hence can be put under the limit.
\( \lim_{\delta \to 0+} \log_b(b[4](\delta -1)) - \log_b(\delta) = \log_b( c) \)
hence
\( \lim_{\delta \to 0+} b[4](\delta -2) - \log_b(\delta) = \log_b( c) \)

So we see that the limit exists, but it exists even for \( b>e^{1/e} \) and depends on the derivation of \( b[4]x \) at \( x=-1 \).

The derivation at -1 can be derived from the value at 0 by:
\( \text{sexp}(x+1)' = \exp_b(\text{sexp}_b(x))' = \ln(b)\text{sexp}(x+1)\text{sexp}_b(x)' \)
hence for \( x=-1 \)
\( \text{sexp}'(0)=\ln(b)c \)

then the limit can be given as
\( \lim_{\delta \to 0+} b[4](\delta -2) - \log_b(\delta)=\log_b\left(\frac{\text{sexp}'(0)}{\ln(b)}\right) \)