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

Definition df-zeta 24047
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 24046 . 2  class  zeta
2 c1 8828 . . . . . . 7  class  1
3 c2 9885 . . . . . . . 8  class  2
4 vs . . . . . . . . . 10  set  s
54cv 1641 . . . . . . . . 9  class  s
6 cmin 9127 . . . . . . . . 9  class  -
72, 5, 6co 5945 . . . . . . . 8  class  ( 1  -  s )
8 ccxp 20020 . . . . . . . 8  class  ^ c
93, 7, 8co 5945 . . . . . . 7  class  ( 2  ^ c  ( 1  -  s ) )
102, 9, 6co 5945 . . . . . 6  class  ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )
11 vf . . . . . . . 8  set  f
1211cv 1641 . . . . . . 7  class  f
135, 12cfv 5337 . . . . . 6  class  ( f `
 s )
14 cmul 8832 . . . . . 6  class  x.
1510, 13, 14co 5945 . . . . 5  class  ( ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )  x.  ( f `
 s ) )
16 cn0 10057 . . . . . 6  class  NN0
17 cc0 8827 . . . . . . . . 9  class  0
18 vn . . . . . . . . . 10  set  n
1918cv 1641 . . . . . . . . 9  class  n
20 cfz 10874 . . . . . . . . 9  class  ...
2117, 19, 20co 5945 . . . . . . . 8  class  ( 0 ... n )
222cneg 9128 . . . . . . . . . . 11  class  -u 1
23 vk . . . . . . . . . . . 12  set  k
2423cv 1641 . . . . . . . . . . 11  class  k
25 cexp 11197 . . . . . . . . . . 11  class  ^
2622, 24, 25co 5945 . . . . . . . . . 10  class  ( -u
1 ^ k )
27 cbc 11408 . . . . . . . . . . 11  class  _C
2819, 24, 27co 5945 . . . . . . . . . 10  class  ( n  _C  k )
2926, 28, 14co 5945 . . . . . . . . 9  class  ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )
30 caddc 8830 . . . . . . . . . . 11  class  +
3124, 2, 30co 5945 . . . . . . . . . 10  class  ( k  +  1 )
3231, 5, 8co 5945 . . . . . . . . 9  class  ( ( k  +  1 )  ^ c  s )
3329, 32, 14co 5945 . . . . . . . 8  class  ( ( ( -u 1 ^ k )  x.  (
n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3421, 33, 23csu 12255 . . . . . . 7  class  sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3519, 2, 30co 5945 . . . . . . . 8  class  ( n  +  1 )
363, 35, 25co 5945 . . . . . . 7  class  ( 2 ^ ( n  + 
1 ) )
37 cdiv 9513 . . . . . . 7  class  /
3834, 36, 37co 5945 . . . . . 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 12255 . . . . 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 1642 . . . 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 8825 . . . . 5  class  CC
422csn 3716 . . . . 5  class  { 1 }
4341, 42cdif 3225 . . . 4  class  ( CC 
\  { 1 } )
4440, 4, 43wral 2619 . . 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 18483 . . . 4  class  -cn->
4643, 41, 45co 5945 . . 3  class  ( ( CC  \  { 1 } ) -cn-> CC )
4744, 11, 46crio 6384 . 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 1642 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