I am currently formalising some results from complexity theory with a theorem prover. For that, I have to prove the following statement:
Let $p, b, \varepsilon \in \mathbb R$ with $\varepsilon>0$ and $b \in (0,1)$. Then there exists some $x_0\in\mathbb R$ such that for all $x \geq x_0$:
$$\left(1-\frac{1}{b \ln^{1+\varepsilon} x}\right)^p\left(1+\frac{1}{\ln^{\varepsilon/2}\left(bx + \frac{x}{\ln^{1+\varepsilon} x}\right)}\right) \geq 1 + \frac{1}{\ln^{\varepsilon/2} x}$$
The paper from which I have this statement says that this can be shown by Taylor series expansions and asymptotic analysis, but gives no further details.
I have given this a lot of thought, but don't see how I could employ Taylor series or anything else to prove this.