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 + 1 m − log ⁡ z m + 1 − log ⁡ z

Detailed syntax breakdown

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