Metamath Proof Explorer

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Γ=z∈ℂ∖ℤ∖ℕ⟼∑m∈ℕz⁢log⁡m+1m−log⁡zm+1−log⁡z

Detailed syntax breakdown

Step Hyp Ref Expression
0 clgam classlogΓ
1 vz setvarz
2 cc classℂ
3 cz classℤ
4 cn classℕ
5 3 4 cdif classℤ∖ℕ
6 2 5 cdif classℂ∖ℤ∖ℕ
7 vm setvarm
8 1 cv setvarz
9 cmul class×
10 clog classlog
11 7 cv setvarm
12 caddc class+
13 c1 class1
14 11 13 12 co classm+1
15 cdiv class÷
16 14 11 15 co classm+1m
17 16 10 cfv classlog⁡m+1m
18 8 17 9 co classz⁢log⁡m+1m
19 cmin class−
20 8 11 15 co classzm
21 20 13 12 co classzm+1
22 21 10 cfv classlog⁡zm+1
23 18 22 19 co classz⁢log⁡m+1m−log⁡zm+1
24 4 23 7 csu class∑m∈ℕz⁢log⁡m+1m−log⁡zm+1
25 8 10 cfv classlog⁡z
26 24 25 19 co class∑m∈ℕz⁢log⁡m+1m−log⁡zm+1−log⁡z
27 1 6 26 cmpt classz∈ℂ∖ℤ∖ℕ⟼∑m∈ℕz⁢log⁡m+1m−log⁡zm+1−log⁡z
28 0 27 wceq wfflogΓ=z∈ℂ∖ℤ∖ℕ⟼∑m∈ℕz⁢log⁡m+1m−log⁡zm+1−log⁡z