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

Definition df-zeta 23688
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 23687 . 2  class  zeta
2 c1 8738 . . . . . . 7  class  1
3 c2 9795 . . . . . . . 8  class  2
4 vs . . . . . . . . . 10  set  s
54cv 1622 . . . . . . . . 9  class  s
6 cmin 9037 . . . . . . . . 9  class  -
72, 5, 6co 5858 . . . . . . . 8  class  ( 1  -  s )
8 ccxp 19913 . . . . . . . 8  class  ^ c
93, 7, 8co 5858 . . . . . . 7  class  ( 2  ^ c  ( 1  -  s ) )
102, 9, 6co 5858 . . . . . 6  class  ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )
11 vf . . . . . . . 8  set  f
1211cv 1622 . . . . . . 7  class  f
135, 12cfv 5255 . . . . . 6  class  ( f `
 s )
14 cmul 8742 . . . . . 6  class  x.
1510, 13, 14co 5858 . . . . 5  class  ( ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )  x.  ( f `
 s ) )
16 cn0 9965 . . . . . 6  class  NN0
17 cc0 8737 . . . . . . . . 9  class  0
18 vn . . . . . . . . . 10  set  n
1918cv 1622 . . . . . . . . 9  class  n
20 cfz 10782 . . . . . . . . 9  class  ...
2117, 19, 20co 5858 . . . . . . . 8  class  ( 0 ... n )
222cneg 9038 . . . . . . . . . . 11  class  -u 1
23 vk . . . . . . . . . . . 12  set  k
2423cv 1622 . . . . . . . . . . 11  class  k
25 cexp 11104 . . . . . . . . . . 11  class  ^
2622, 24, 25co 5858 . . . . . . . . . 10  class  ( -u
1 ^ k )
27 cbc 11315 . . . . . . . . . . 11  class  _C
2819, 24, 27co 5858 . . . . . . . . . 10  class  ( n  _C  k )
2926, 28, 14co 5858 . . . . . . . . 9  class  ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )
30 caddc 8740 . . . . . . . . . . 11  class  +
3124, 2, 30co 5858 . . . . . . . . . 10  class  ( k  +  1 )
3231, 5, 8co 5858 . . . . . . . . 9  class  ( ( k  +  1 )  ^ c  s )
3329, 32, 14co 5858 . . . . . . . 8  class  ( ( ( -u 1 ^ k )  x.  (
n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3421, 33, 23csu 12158 . . . . . . 7  class  sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3519, 2, 30co 5858 . . . . . . . 8  class  ( n  +  1 )
363, 35, 25co 5858 . . . . . . 7  class  ( 2 ^ ( n  + 
1 ) )
37 cdiv 9423 . . . . . . 7  class  /
3834, 36, 37co 5858 . . . . . 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 12158 . . . . 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 1623 . . . 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 8735 . . . . 5  class  CC
422csn 3640 . . . . 5  class  { 1 }
4341, 42cdif 3149 . . . 4  class  ( CC 
\  { 1 } )
4440, 4, 43wral 2543 . . 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 18380 . . . 4  class  -cn->
4643, 41, 45co 5858 . . 3  class  ( ( CC  \  { 1 } ) -cn-> CC )
4744, 11, 46crio 6297 . 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 1623 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