Definition df-lgam

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 ( logG ( 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)

	Ref	Expression
Assertion	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 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clgam	|- log_G
1		vz	|- z
2		cc	|- CC
3		cz	|- ZZ
4		cn	|- NN
5	3 4	cdif	|- ( ZZ \ NN )
6	2 5	cdif	|- ( CC \ ( ZZ \ NN ) )
7		vm	|- m
8	1	cv	|- z
9		cmul	|- x.
10		clog	|- log
11	7	cv	|- m
12		caddc	|- +
13		c1	|- 1
14	11 13 12	co	|- ( m + 1 )
15		cdiv	|- /
16	14 11 15	co	|- ( ( m + 1 ) / m )
17	16 10	cfv	|- ( log ` ( ( m + 1 ) / m ) )
18	8 17 9	co	|- ( z x. ( log ` ( ( m + 1 ) / m ) ) )
19		cmin	|- -
20	8 11 15	co	|- ( z / m )
21	20 13 12	co	|- ( ( z / m ) + 1 )
22	21 10	cfv	|- ( log ` ( ( z / m ) + 1 ) )
23	18 22 19	co	|- ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) )
24	4 23 7	csu	|- sum_ m e. NN ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) )
25	8 10	cfv	|- ( log ` z )
26	24 25 19	co	|- ( sum_ m e. NN ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) - ( log ` z ) )
27	1 6 26	cmpt	|- ( z e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ m e. NN ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) - ( log ` z ) ) )
28	0 27	wceq	|- log_G = ( z e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ m e. NN ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) - ( log ` z ) ) )