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 e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) = ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
2 1 logdivsum 
 |-  ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) : RR+ --> RR /\ ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r /\ ( ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r 1 /\ 1 e. RR+ /\ _e <_ 1 ) -> ( abs ` ( ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ` 1 ) - 1 ) ) <_ ( ( log ` 1 ) / 1 ) ) )
3 2 simp2i 
 |-  ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r
4 eldmg 
 |-  ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r -> ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r <-> E. z ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z ) )
5 4 ibi 
 |-  ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r -> E. z ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z )
6 id 
 |-  ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z -> ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z )
7 1 6 mulog2sumlem3 
 |-  ( ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
8 7 exlimiv 
 |-  ( E. z ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
9 3 5 8 mp2b 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)