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

Definition df-lgam 23692
Description: Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to  log ( _G ( x ) ) because the branch cuts are placed differently (we do have  exp ( log  _G ( x ) )  =  _G ( x ), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers  ZZ  \  NN, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
Assertion
Ref Expression
df-lgam  |-  log  _G  =  ( z  e.  ( CC  \  ( ZZ  \  NN ) ) 
|->  (  ~~>  `  ( n  e.  NN  |->  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z
) )  -  sum_ m  e.  ( 1 ... n ) ( log `  ( ( z  /  m )  +  1 ) ) ) ) ) )
Distinct variable group:    z, n, m

Detailed syntax breakdown of Definition df-lgam
StepHypRef Expression
1 clgam 23690 . 2  class  log  _G
2 vz . . 3  set  z
3 cc 8735 . . . 4  class  CC
4 cz 10024 . . . . 5  class  ZZ
5 cn 9746 . . . . 5  class  NN
64, 5cdif 3149 . . . 4  class  ( ZZ 
\  NN )
73, 6cdif 3149 . . 3  class  ( CC 
\  ( ZZ  \  NN ) )
8 vn . . . . 5  set  n
92cv 1622 . . . . . . . 8  class  z
108cv 1622 . . . . . . . . 9  class  n
11 clog 19912 . . . . . . . . 9  class  log
1210, 11cfv 5255 . . . . . . . 8  class  ( log `  n )
13 cmul 8742 . . . . . . . 8  class  x.
149, 12, 13co 5858 . . . . . . 7  class  ( z  x.  ( log `  n
) )
159, 11cfv 5255 . . . . . . 7  class  ( log `  z )
16 cmin 9037 . . . . . . 7  class  -
1714, 15, 16co 5858 . . . . . 6  class  ( ( z  x.  ( log `  n ) )  -  ( log `  z ) )
18 c1 8738 . . . . . . . 8  class  1
19 cfz 10782 . . . . . . . 8  class  ...
2018, 10, 19co 5858 . . . . . . 7  class  ( 1 ... n )
21 vm . . . . . . . . . . 11  set  m
2221cv 1622 . . . . . . . . . 10  class  m
23 cdiv 9423 . . . . . . . . . 10  class  /
249, 22, 23co 5858 . . . . . . . . 9  class  ( z  /  m )
25 caddc 8740 . . . . . . . . 9  class  +
2624, 18, 25co 5858 . . . . . . . 8  class  ( ( z  /  m )  +  1 )
2726, 11cfv 5255 . . . . . . 7  class  ( log `  ( ( z  /  m )  +  1 ) )
2820, 27, 21csu 12158 . . . . . 6  class  sum_ m  e.  ( 1 ... n
) ( log `  (
( z  /  m
)  +  1 ) )
2917, 28, 16co 5858 . . . . 5  class  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z
) )  -  sum_ m  e.  ( 1 ... n ) ( log `  ( ( z  /  m )  +  1 ) ) )
308, 5, 29cmpt 4077 . . . 4  class  ( n  e.  NN  |->  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z
) )  -  sum_ m  e.  ( 1 ... n ) ( log `  ( ( z  /  m )  +  1 ) ) ) )
31 cli 11958 . . . 4  class  ~~>
3230, 31cfv 5255 . . 3  class  (  ~~>  `  (
n  e.  NN  |->  ( ( ( z  x.  ( log `  n
) )  -  ( log `  z ) )  -  sum_ m  e.  ( 1 ... n ) ( log `  (
( z  /  m
)  +  1 ) ) ) ) )
332, 7, 32cmpt 4077 . 2  class  ( z  e.  ( CC  \ 
( ZZ  \  NN ) )  |->  (  ~~>  `  (
n  e.  NN  |->  ( ( ( z  x.  ( log `  n
) )  -  ( log `  z ) )  -  sum_ m  e.  ( 1 ... n ) ( log `  (
( z  /  m
)  +  1 ) ) ) ) ) )
341, 33wceq 1623 1  wff  log  _G  =  ( z  e.  ( CC  \  ( ZZ  \  NN ) ) 
|->  (  ~~>  `  ( n  e.  NN  |->  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z
) )  -  sum_ m  e.  ( 1 ... n ) ( log `  ( ( z  /  m )  +  1 ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator