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

Definition df-zeta 24803
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 24802 . 2  class  zeta
2 c1 8996 . . . . . . 7  class  1
3 c2 10054 . . . . . . . 8  class  2
4 vs . . . . . . . . . 10  set  s
54cv 1652 . . . . . . . . 9  class  s
6 cmin 9296 . . . . . . . . 9  class  -
72, 5, 6co 6084 . . . . . . . 8  class  ( 1  -  s )
8 ccxp 20458 . . . . . . . 8  class  ^ c
93, 7, 8co 6084 . . . . . . 7  class  ( 2  ^ c  ( 1  -  s ) )
102, 9, 6co 6084 . . . . . 6  class  ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )
11 vf . . . . . . . 8  set  f
1211cv 1652 . . . . . . 7  class  f
135, 12cfv 5457 . . . . . 6  class  ( f `
 s )
14 cmul 9000 . . . . . 6  class  x.
1510, 13, 14co 6084 . . . . 5  class  ( ( 1  -  ( 2  ^ c  ( 1  -  s ) ) )  x.  ( f `
 s ) )
16 cn0 10226 . . . . . 6  class  NN0
17 cc0 8995 . . . . . . . . 9  class  0
18 vn . . . . . . . . . 10  set  n
1918cv 1652 . . . . . . . . 9  class  n
20 cfz 11048 . . . . . . . . 9  class  ...
2117, 19, 20co 6084 . . . . . . . 8  class  ( 0 ... n )
222cneg 9297 . . . . . . . . . . 11  class  -u 1
23 vk . . . . . . . . . . . 12  set  k
2423cv 1652 . . . . . . . . . . 11  class  k
25 cexp 11387 . . . . . . . . . . 11  class  ^
2622, 24, 25co 6084 . . . . . . . . . 10  class  ( -u
1 ^ k )
27 cbc 11598 . . . . . . . . . . 11  class  _C
2819, 24, 27co 6084 . . . . . . . . . 10  class  ( n  _C  k )
2926, 28, 14co 6084 . . . . . . . . 9  class  ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )
30 caddc 8998 . . . . . . . . . . 11  class  +
3124, 2, 30co 6084 . . . . . . . . . 10  class  ( k  +  1 )
3231, 5, 8co 6084 . . . . . . . . 9  class  ( ( k  +  1 )  ^ c  s )
3329, 32, 14co 6084 . . . . . . . 8  class  ( ( ( -u 1 ^ k )  x.  (
n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3421, 33, 23csu 12484 . . . . . . 7  class  sum_ k  e.  ( 0 ... n
) ( ( (
-u 1 ^ k
)  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )
3519, 2, 30co 6084 . . . . . . . 8  class  ( n  +  1 )
363, 35, 25co 6084 . . . . . . 7  class  ( 2 ^ ( n  + 
1 ) )
37 cdiv 9682 . . . . . . 7  class  /
3834, 36, 37co 6084 . . . . . 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 12484 . . . . 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 1653 . . . 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 8993 . . . . 5  class  CC
422csn 3816 . . . . 5  class  { 1 }
4341, 42cdif 3319 . . . 4  class  ( CC 
\  { 1 } )
4440, 4, 43wral 2707 . . 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 18911 . . . 4  class  -cn->
4643, 41, 45co 6084 . . 3  class  ( ( CC  \  { 1 } ) -cn-> CC )
4744, 11, 46crio 6545 . 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 1653 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