Theorem 2vmadivsum

Description: The sum sum_ m n <_ x , Lam ( m ) Lam ( n ) / m n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . (Contributed by Mario Carneiro, 30-May-2016)

	Ref	Expression
Assertion	2vmadivsum	$$⊢\left(x\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\sum _{m=1}^{⌊\frac{x}{n}⌋}\left(\frac{\Lambda \left(m\right)}{m}\right)}{\log x}\right)-\left(\frac{\log x}{2}\right)\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		vmadivsumb	$$⊢\exists c\in {ℝ}^{+}\forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c$$
2		simpl	$$⊢\left(c\in {ℝ}^{+}\wedge \forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c\right)\to c\in {ℝ}^{+}$$
3		simpr	$$⊢\left(c\in {ℝ}^{+}\wedge \forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c\right)\to \forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c$$
4	2 3	2vmadivsumlem	$$⊢\left(c\in {ℝ}^{+}\wedge \forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c\right)\to \left(x\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\sum _{m=1}^{⌊\frac{x}{n}⌋}\left(\frac{\Lambda \left(m\right)}{m}\right)}{\log x}\right)-\left(\frac{\log x}{2}\right)\right)\in 𝑂\left(1\right)$$
5	4	rexlimiva	$$⊢\exists c\in {ℝ}^{+}\forall y\in \left[1,\mathrm{+\infty }\right)\left|\sum _{i=1}^{⌊y⌋}\left(\frac{\Lambda \left(i\right)}{i}\right)-\log y\right|\le c\to \left(x\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\sum _{m=1}^{⌊\frac{x}{n}⌋}\left(\frac{\Lambda \left(m\right)}{m}\right)}{\log x}\right)-\left(\frac{\log x}{2}\right)\right)\in 𝑂\left(1\right)$$
6	1 5	ax-mp	$$⊢\left(x\in \left(1,\mathrm{+\infty }\right)⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\left(\frac{\Lambda \left(n\right)}{n}\right)\sum _{m=1}^{⌊\frac{x}{n}⌋}\left(\frac{\Lambda \left(m\right)}{m}\right)}{\log x}\right)-\left(\frac{\log x}{2}\right)\right)\in 𝑂\left(1\right)$$