Description
Close the sorry on zeta_pow_four_eq in IwaniecKowalskiCh1.lean (IK (1.29)):
[
\zeta(s)^4 = \zeta(2s)\sum_{n=1}^{\infty}\tau(n)^2 n^{-s}
\qquad(\operatorname{Re}(s)>1).
]
Suggested approach
Direct Euler-product proof (independent of the general Ramanujan identity #1688):
- local factor (\sum_k (k+1)^2 x^k = (1+x)/(1-x)^3);
- compare with (\zeta(2s)) to recover (1/(1-x)^4);
- absolute convergence via (\tau(n)^2 \le d_4(n)).
Notes
This unlocks the written dependency of zeta_pow_three_eq on the corollary once zeta_mul_tau_square_eq is also proved.
Description
Close the
sorryonzeta_pow_four_eqinIwaniecKowalskiCh1.lean(IK (1.29)):[
\zeta(s)^4 = \zeta(2s)\sum_{n=1}^{\infty}\tau(n)^2 n^{-s}
\qquad(\operatorname{Re}(s)>1).
]
Suggested approach
Direct Euler-product proof (independent of the general Ramanujan identity
#1688):Notes
This unlocks the written dependency of
zeta_pow_three_eqon the corollary oncezeta_mul_tau_square_eqis also proved.