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	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
2	1	logdivsum	⊢ ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) : ℝ⁺ ⟶ ℝ ∧ ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝_𝑟 ∧ ( ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 1 ∧ 1 ∈ ℝ⁺ ∧ e ≤ 1 ) → ( abs ‘ ( ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ‘ 1 ) − 1 ) ) ≤ ( ( log ‘ 1 ) / 1 ) ) )
3	2	simp2i	⊢ ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝_𝑟
4		eldmg	⊢ ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝_𝑟 → ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝_𝑟 ↔ ∃ 𝑧 ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 ) )
5	4	ibi	⊢ ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝_𝑟 → ∃ 𝑧 ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 )
6		id	⊢ ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 → ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 )
7	1 6	mulog2sumlem3	⊢ ( ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
8	7	exlimiv	⊢ ( ∃ 𝑧 ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) ⇝_𝑟 𝑧 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
9	3 5 8	mp2b	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)