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 Γ = ( 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑚 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clgam	⊢ log Γ
1		vz	⊢ 𝑧
2		cc	⊢ ℂ
3		cz	⊢ ℤ
4		cn	⊢ ℕ
5	3 4	cdif	⊢ ( ℤ ∖ ℕ )
6	2 5	cdif	⊢ ( ℂ ∖ ( ℤ ∖ ℕ ) )
7		vm	⊢ 𝑚
8	1	cv	⊢ 𝑧
9		cmul	⊢ ·
10		clog	⊢ log
11	7	cv	⊢ 𝑚
12		caddc	⊢ +
13		c1	⊢ 1
14	11 13 12	co	⊢ ( 𝑚 + 1 )
15		cdiv	⊢ /
16	14 11 15	co	⊢ ( ( 𝑚 + 1 ) / 𝑚 )
17	16 10	cfv	⊢ ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) )
18	8 17 9	co	⊢ ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) )
19		cmin	⊢ −
20	8 11 15	co	⊢ ( 𝑧 / 𝑚 )
21	20 13 12	co	⊢ ( ( 𝑧 / 𝑚 ) + 1 )
22	21 10	cfv	⊢ ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) )
23	18 22 19	co	⊢ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) )
24	4 23 7	csu	⊢ Σ 𝑚 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) )
25	8 10	cfv	⊢ ( log ‘ 𝑧 )
26	24 25 19	co	⊢ ( Σ 𝑚 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) − ( log ‘ 𝑧 ) )
27	1 6 26	cmpt	⊢ ( 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑚 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )
28	0 27	wceq	⊢ log Γ = ( 𝑧 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↦ ( Σ 𝑚 ∈ ℕ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) − ( log ‘ 𝑧 ) ) )