$a_{n+1} = a_n+\int_{a_n}^{+\infty}1-\exp(-\exp(-x))dx$ I have the following recursive equation:
$$a_{n+1} = a_n+\int_{a_n}^{+\infty}1-\exp(-\exp(-x))dx$$
with the initial condition $a_0 = 0$.
I would like to show that there exists a sequence $b_n$ which is asymptotically equivalent to $\ln n$ as $n$ goes to infinity, such that $a_n\geq b_n$ (at least for every $n$ large enough).
I have tried several things, such as upper bounding $1-\exp(-\exp(-x))$ by $\exp(-x)$ but I have not been successful so far.
 A: Let $(a_n)$ be a sequence defined by a recursion $a_{n+1} = a_n + f(a_n) =: F(a_n)$, where $f$ is a nice positive function which decays to $0$. There is a general method to study the speed of divergence of $(a_n)$: comparison with the solution of a differential equation. Here I'll get a lower bound.
We know that $e^u \leq 1+(1+e^{-1})u$ for all $u \in [-1,0]$. Putting $u=-e^{-x}$, we get $1-e^{-e^{-x}} \geq (1+e^{-1}) e^{-x}$ for all $x \geq 0$. Since $(a_n)$ is nonnegative, we get:
$$a_{n+1} \geq a_n+\int_{a_n}^{+ \infty} (1+e^{-1}) e^{-x} \ dx = a_n+(1+e^{-1}) e^{-a_n}.$$
Let $C := (1+e^{-1})$, $y_0 \geq 0$ and $y$ be the solution of the system:
$$y(0)= y_0, \quad \quad y'(t) = Ce^{-y(t)} \ \ \forall t\geq 0.$$
This function is increasing. In addition, since the function $u \mapsto Ce^{-u}$ is decreasing, the function $t \mapsto Ce^{-y(t)}$ is decreasing. Hence, for $t \in [n,n+1]$, we have $y'(t) \leq y'(n) = Ce^{-y(n)}$. Integrating over $[n,n+1]$, we get
$$y(n+1)-y(n) \leq Ce^{-y(n)}.$$
Let $G$ be the function which maps $y_0$ to $y(1)$. Then the inequality above implies that $G \leq F$. Composing these functions $n$ times, we get $G^{n} \leq F^{n}$, and then $G^n (0) \leq F^n (0)$. But $F^n(0) = a_n$ and $G^n(0) = y(n)$, where we chose $y_0=0$.
In addition, the differential equation above can be solved explicitely:
$$dy = Ce^{-y} dt,$$
$$d(e^y) = C dt,$$
$$e^{y(t)}-e^{y_0} = Ct.$$
So, for $y_0 = 0$ we have $y(t) = \ln (1+Ct)$. Putting everything together, we finally get:
$$a_n \geq y(n) = \ln (1+Cn) \sim \ln(n).$$
