0
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Some change variable like $1/\ln^{1+\epsilon}x:=t$ may help, so you have to prove an inequality for small positive $t$, for which the Taylor expansion at $0$ may suffice. $\endgroup$ Feb 21, 2015 at 11:36

1 Answer 1

3
$\begingroup$

When $x\to \infty$ we have $$\left(1-\frac1{b\ln^{1+\epsilon}x}\right)^p = 1 -\frac p{b\ln^{1+\epsilon}x} + o\left(\frac1{\ln^{1+\epsilon}x}\right),$$ and $$\frac1{\ln^{\epsilon/2}\left(bx + \frac x{\ln^{1+\epsilon}x}\right)}= (\ln bx)^{-\epsilon/2} \left(\frac1{1+ \frac1{\ln bx} \ln\left(1 + \frac1{b\ln^{1+\epsilon}x}\right)}\right)^{\epsilon/2}= (\ln bx)^{-\epsilon/2} + o\left(\frac1{\ln^{1+\epsilon/2}x}\right).$$ Hence $$\left(1-\frac1{b\ln^{1+\epsilon}x}\right)^p\left(1+ \frac1{\ln^{\epsilon/2}\left(bx + \frac x{\ln^{1+\epsilon}x}\right)}\right) = 1 + \frac1{(\ln bx)^{\epsilon/2}} + o\left(\frac1{\ln^{1+\epsilon/2}x}\right).$$ The existence of $x_0$ now follows from the assumption $b\in (0,1)$.

$\endgroup$
2
  • $\begingroup$ This looks very nice, thanks for your effort. I am, however, not familiar with this kind of reasoning. Could you perhaps provide me with some more details on some of these estimates? $\endgroup$ Feb 21, 2015 at 18:06
  • $\begingroup$ Okay, it took me three full days to retrace the steps of your proofs formally and formalise the entire thing in Isabelle/HOL, but now I'm done. Thanks again for your help, I probably wouldn't have found the solution this quickly otherwise. $\endgroup$ Feb 24, 2015 at 21:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.