MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lgam Structured version   Unicode version

Definition df-lgam 23817
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 ) ) 
|->  ( sum_ m  e.  NN  ( ( z  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )  -  ( log `  z
) ) )
Distinct variable group:    z, m

Detailed syntax breakdown of Definition df-lgam
StepHypRef Expression
1 clgam 23814 . 2  class  log _G
2 vz . . 3  setvar  z
3 cc 9536 . . . 4  class  CC
4 cz 10937 . . . . 5  class  ZZ
5 cn 10609 . . . . 5  class  NN
64, 5cdif 3439 . . . 4  class  ( ZZ 
\  NN )
73, 6cdif 3439 . . 3  class  ( CC 
\  ( ZZ  \  NN ) )
82cv 1436 . . . . . . 7  class  z
9 vm . . . . . . . . . . 11  setvar  m
109cv 1436 . . . . . . . . . 10  class  m
11 c1 9539 . . . . . . . . . 10  class  1
12 caddc 9541 . . . . . . . . . 10  class  +
1310, 11, 12co 6305 . . . . . . . . 9  class  ( m  +  1 )
14 cdiv 10268 . . . . . . . . 9  class  /
1513, 10, 14co 6305 . . . . . . . 8  class  ( ( m  +  1 )  /  m )
16 clog 23377 . . . . . . . 8  class  log
1715, 16cfv 5601 . . . . . . 7  class  ( log `  ( ( m  + 
1 )  /  m
) )
18 cmul 9543 . . . . . . 7  class  x.
198, 17, 18co 6305 . . . . . 6  class  ( z  x.  ( log `  (
( m  +  1 )  /  m ) ) )
208, 10, 14co 6305 . . . . . . . 8  class  ( z  /  m )
2120, 11, 12co 6305 . . . . . . 7  class  ( ( z  /  m )  +  1 )
2221, 16cfv 5601 . . . . . 6  class  ( log `  ( ( z  /  m )  +  1 ) )
23 cmin 9859 . . . . . 6  class  -
2419, 22, 23co 6305 . . . . 5  class  ( ( z  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )
255, 24, 9csu 13730 . . . 4  class  sum_ m  e.  NN  ( ( z  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )
268, 16cfv 5601 . . . 4  class  ( log `  z )
2725, 26, 23co 6305 . . 3  class  ( sum_ m  e.  NN  ( ( z  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )  -  ( log `  z ) )
282, 7, 27cmpt 4484 . 2  class  ( z  e.  ( CC  \ 
( ZZ  \  NN ) )  |->  ( sum_ m  e.  NN  ( ( z  x.  ( log `  ( ( m  + 
1 )  /  m
) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )  -  ( log `  z ) ) )
291, 28wceq 1437 1  wff  log _G  =  ( z  e.  ( CC  \  ( ZZ  \  NN ) ) 
|->  ( sum_ m  e.  NN  ( ( z  x.  ( log `  (
( m  +  1 )  /  m ) ) )  -  ( log `  ( ( z  /  m )  +  1 ) ) )  -  ( log `  z
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  lgamgulm2  23834  lgamf  23840  iprodgam  30173
  Copyright terms: Public domain W3C validator