Dyadic sum of $\frac{x}{\ln x}$ (i.e. dyadic asymptotic for prime number theorem)

Question

For $x\geq 10$, denote $j=j_x$ s.t. $4 \geq \frac{x}{2^j}\geq 2$. I want to prove that $$\sum_{i=0}^j \frac{x/2^i}{\log(x/2^i)} \sim \frac{2x}{\log x}$$

The reason I care is because the prime number theorem $\sum_{x<p\leq 2x} 1 \sim \frac{x}{\log x}$ implies that $\sum_{x<p\leq 2x} 1 \sim \frac{x}{\log x}$, and I need the above asymptotic to go backward.

Based on graphical evidence, this seems true https://www.desmos.com/calculator/qku5msur6w.

---

I can manage to show that these are comparable (i.e. $\asymp$), but not $\sim$. My method is to write $$\frac{x/2^i}{\log(x/2^i)} = \frac{x/2^i}{\log(x)} \cdot \frac{\log(x)}{\log(x/2^i)},$$ where the 2nd factor $$\frac{\log(x)}{\log(x/2^i)} = 1+\frac{\log(2^i)}{\log(x/2^i)} \leq 1+\frac{i\log(2)}{\log(x/2^j)} \leq 1+ \frac{i\log 2}{\log 2}= (1+i),$$ and of course $\frac{1+i}{2^i} \ll \frac{1}{(1.5)^i}$, which is summable to some constant.

Answer 1

Trying Gary's comment, I couldn't get summing to $j/2$ to work, but I did get summing to $j'=\log\log x$ to work (we don't need to be careful about including/excluding the pivot point from either sum, since one term of the sum will wash away in the asymptotic anyway): $$\sum_{i=0}^j \frac{x/2^i}{\log(x/2^i)} = \sum_{i=0}^{\log \log x} \frac{x/2^i}{\log(x/2^i)} + \sum_{i=\log\log x}^j \frac{x/2^i}{\log(x/2^i)}$$ where for the first term: $$\log x - \log\log x \leq \log x - j' \log(2) \leq \log(x/2^i) \leq \log x$$ so $$\frac{1}{\log x}\sum_{i=0}^{\log\log x} \frac{x}{2^i} \leq \sum_{i=0}^{\log\log x} \frac{x/2^i}{\log(x/2^i)} \leq \frac{1}{\log x-\log\log x}\sum_{i=0}^{\log\log x} \frac{x}{2^i} $$ and the geometric series (as before, even if I'm off by one somewhere, it washes away in the asymptotic) $$\sum_{i=0}^{\log\log x} \frac{x}{2^i} = 2x - \frac{x}{2^{\log\log x}} = 2x-c\frac{x}{\log x}$$ and so indeed $$\sum_{i=0}^{\log\log x} \frac{x/2^i}{\log(x/2^i)} \sim \frac{2x}{\log x}.$$

Similarly for the second term: $$\sum_{i=\log\log x}^j \frac{x/2^i}{\log(x/2^i)} \leq \frac{1}{\log(x/2^{\log\log x} ) } \sum_{i=\log\log x} ^j \frac{x}{2^i} \leq \frac{1}{\log x - \log\log x} \sum_{i=\log\log x} ^\infty \frac{x}{2^i}$$ and this geometric series is (again I may be off by 1) $$\sum_{i=\log\log x} ^\infty \frac{x}{2^i} = \frac{x}{2^{\log\log x}} \ll \frac{x}{\log x}$$ so the 2nd term is bounded by $\ll \frac{x}{\log^2 x}$.

Answer 2

We split the sum into two parts at $i=j/2$ and estimate each part separately. For the first half, we note that $$ \frac{{\log x}}{x}\sum\limits_{i = 0}^{j/2} {\frac{{x/2^i }}{{\log (x/2^i )}}} = \sum\limits_{i = 0}^{j/2} {\frac{1}{{2^i }}\frac{{\log x}}{{\log (x/2^i )}}} $$ and $$ 1 \le \color{red}{\frac{{\log x}}{{\log (x/2^i )}}} \le \frac{{\log x}}{{\log (x/2^{j/2} )}} \le \frac{{\log x}}{{\frac{1}{2}\log (2x)}} \le 2 $$ for $0\le i\le j/2$. Consequently, by Tannery's theorem, $$ \frac{{\log x}}{x}\sum\limits_{i = 0}^{j/2} {\frac{{x/2^i }}{{\log (x/2^i )}}} \to \sum\limits_{i = 0}^\infty {\frac{1}{{2^i }}} = 2 $$ as $x\to+\infty$ (i.e., as $j\to+\infty$). In other words, $$ \sum\limits_{i = 0}^{j/2} {\frac{{x/2^i }}{{\log (x/2^i )}}} \sim \frac{{2x}}{{\log x}} $$ as $x\to+\infty$. For the second half of the sum, note that $$ \sum\limits_{i = j/2 + 1}^j {\frac{{x/2^i }}{{\log (x/2^i )}}} \ll j\frac{x}{{2^{j/2} }}\frac{1}{{\log (x/2^{j/2} )}} \ll (\log x)\sqrt x \frac{1}{{\log x}} = \sqrt x =o\!\left( \frac{x}{{\log x}}\right), $$ as $x\to+\infty$. Therefore, $$ \sum\limits_{i = 0}^j {\frac{{x/2^i }}{{\log (x/2^i )}}} \sim \frac{{2x}}{{\log x}} $$ as $x\to+\infty$.