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 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 )
3 1 2 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) )
4 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 ) ) )
5 4 simp2i 
 |-  ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) e. dom ~~>r
6 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 ) )
7 6 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 )
8 5 7 ax-mp 
 |-  E. z ( y e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) ~~>r z
9 3 8 exlimiiv 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)