Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-zeta Unicode version

Definition df-zeta 24751
Description: Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except  1, but going from the alternating zeta function to the regular zeta function requires dividing by  1  -  2 ^ ( 1  -  s ), which has zeroes other than  1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)
Assertion
Ref Expression
df-zeta  |-  zeta  =  ( iota_ f  e.  ( ( CC  \  {
1 } ) -cn-> CC ) A. s  e.  ( CC  \  {
1 } ) ( ( 1  -  (
2  ^ c  ( 1  -  s ) ) )  x.  (
f `  s )
)  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 ) ) ) )
Distinct variable group:    f, k, n, s

Detailed syntax breakdown of Definition df-zeta
StepHypRef Expression
1 czeta 24750 . 2  class  zeta
2 c1 8947 . . . . . . 7  class  1
3 c2 10005 . . . . . . . 8  class  2
4 vs . . . . . . . . . 10  set  s
54cv 1648 . . . . . . . . 9  class  s
6 cmin 9247 . . . . . . . . 9  class  -
72, 5, 6co 6040 . . . . . . . 8  class  ( 1  -  s )
8 ccxp 20406 . . . . . . . 8  class  ^ c
93, 7, 8co 6040 . . . . . . 7  class  ( 2  ^ c  ( 1  -  s ) )
102, 9, 6co 6040 . . . . . 6  class  ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )
11 vf . . . . . . . 8  set  f
1211cv 1648 . . . . . . 7  class  f
135, 12cfv 5413 . . . . . 6  class  ( f `
 s )
14 cmul 8951 . . . . . 6  class  x.
1510, 13, 14co 6040 . . . . 5  class  ( ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )  x.  ( f `
 s ) )
16 cn0 10177 . . . . . 6  class  NN0
17 cc0 8946 . . . . . . . . 9  class  0
18 vn . . . . . . . . . 10  set  n
1918cv 1648 . . . . . . . . 9  class  n
20 cfz 10999 . . . . . . . . 9  class  ...
2117, 19, 20co 6040 . . . . . . . 8  class  ( 0 ... n )
222cneg 9248 . . . . . . . . . . 11  class  -u 1
23 vk . . . . . . . . . . . 12  set  k
2423cv 1648 . . . . . . . . . . 11  class  k
25 cexp 11337 . . . . . . . . . . 11  class  ^
2622, 24, 25co 6040 . . . . . . . . . 10  class  ( -u
1 ^ k )
27 cbc 11548 . . . . . . . . . . 11  class  _C
2819, 24, 27co 6040 . . . . . . . . . 10  class  ( n  _C  k )
2926, 28, 14co 6040 . . . . . . . . 9  class  ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )
30 caddc 8949 . . . . . . . . . . 11  class  +
3124, 2, 30co 6040 . . . . . . . . . 10  class  ( k  +  1 )
3231, 5, 8co 6040 . . . . . . . . 9  class  ( ( k  +  1 )  ^ c  s )
3329, 32, 14co 6040 . . . . . . . 8  class  ( ( ( -u 1 ^ k )  x.  (
n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3421, 33, 23csu 12434 . . . . . . 7  class  sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3519, 2, 30co 6040 . . . . . . . 8  class  ( n  +  1 )
363, 35, 25co 6040 . . . . . . 7  class  ( 2 ^ ( n  + 
1 ) )
37 cdiv 9633 . . . . . . 7  class  /
3834, 36, 37co 6040 . . . . . 6  class  ( sum_ k  e.  ( 0 ... n ) ( ( ( -u 1 ^ k )  x.  ( n  _C  k
) )  x.  (
( k  +  1 )  ^ c  s ) )  /  (
2 ^ ( n  +  1 ) ) )
3916, 38, 18csu 12434 . . . . 5  class  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 ) ) )
4015, 39wceq 1649 . . . 4  wff  ( ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )  x.  ( f `
 s ) )  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n ) ( ( ( -u
1 ^ k )  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c 
s ) )  / 
( 2 ^ (
n  +  1 ) ) )
41 cc 8944 . . . . 5  class  CC
422csn 3774 . . . . 5  class  { 1 }
4341, 42cdif 3277 . . . 4  class  ( CC 
\  { 1 } )
4440, 4, 43wral 2666 . . 3  wff  A. s  e.  ( CC  \  {
1 } ) ( ( 1  -  (
2  ^ c  ( 1  -  s ) ) )  x.  (
f `  s )
)  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 ) ) )
45 ccncf 18859 . . . 4  class  -cn->
4643, 41, 45co 6040 . . 3  class  ( ( CC  \  { 1 } ) -cn-> CC )
4744, 11, 46crio 6501 . 2  class  ( iota_ f  e.  ( ( CC 
\  { 1 } ) -cn-> CC ) A. s  e.  ( CC  \  {
1 } ) ( ( 1  -  (
2  ^ c  ( 1  -  s ) ) )  x.  (
f `  s )
)  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 ) ) ) )
481, 47wceq 1649 1  wff  zeta  =  ( iota_ f  e.  ( ( CC  \  {
1 } ) -cn-> CC ) A. s  e.  ( CC  \  {
1 } ) ( ( 1  -  (
2  ^ c  ( 1  -  s ) ) )  x.  (
f `  s )
)  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator