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		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$
3	1 2	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)$
4	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}))$
5	4	simp2i	$⊢ (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \in dom \underset{ℝ}{⇝}$
6		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)$
7	6	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$
8	5 7	ax-mp	$⊢ \exists z (y \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊y⌋} (\frac{\log m}{m}) - (\frac{{\log y}^{2}}{2})) \underset{ℝ}{⇝} z$
9	3 8	exlimiiv	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$