Description: Lemma for rpvmasum . Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n ) Lam ( n ) / n ) = log x + O(1) , where .1. ( x ) is the principal Dirichlet character. Equation 9.4.7 of Shapiro, p. 376. (Contributed by Mario Carneiro, 2-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rpvmasum.z | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
rpvmasum.g | |
||
rpvmasum.d | |
||
rpvmasum.1 | |
||
Assertion | rpvmasumlem | |