Metamath Proof Explorer

Theorem mulog2sum

Description: Asymptotic formula for sum_ n <_ x , ( mmu ( n ) / n ) log ^ 2 ( x / n ) = 2 log x + O(1) . Equation 10.2.8 of Shapiro, p. 407. (Contributed by Mario Carneiro, 19-May-2016)

		Ref	Expression
	Assertion	mulog2sum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) = (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2}))$
2	1	logdivsum	$⊢ ((y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) : ℝ^{+} ⟶ ℝ \land (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝} \land (((y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} 1 \land 1 \in ℝ^{+} \land e \leq 1) \to \|(y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) (1) - 1\| \leq \frac{\log 1}{1}))$
3	2	simp2i	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝}$
4		eldmg	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝} \to ((y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝} \leftrightarrow \exists z (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z)$
5	4	ibi	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝} \to \exists z (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z$
6		id	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z \to (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z$
7	1 6	mulog2sumlem3	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$
8	7	exlimiv	$⊢ \exists z (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$
9	3 5 8	mp2b	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$