Definition df-lgam 26905

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(Γ(𝑥)) because the branch cuts are placed differently (we do have exp(log Γ(𝑥)) = Γ(𝑥), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers ℤ ∖ ℕ, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)

Assertion

Ref	Expression
df-lgam	⊢ log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))

Distinct variable group:   𝑧,𝑚

Detailed syntax breakdown of Definition df-lgam

Step	Hyp	Ref	Expression
1		clgam 26902	. 2 class log Γ
2		vz	. . 3 setvar 𝑧
3		cc 11042	. . . 4 class ℂ
4		cz 12505	. . . . 5 class ℤ
5		cn 12162	. . . . 5 class ℕ
6	4, 5	cdif 3908	. . . 4 class (ℤ ∖ ℕ)
7	3, 6	cdif 3908	. . 3 class (ℂ ∖ (ℤ ∖ ℕ))
8	2	cv 1539	. . . . . . 7 class 𝑧
9		vm	. . . . . . . . . . 11 setvar 𝑚
10	9	cv 1539	. . . . . . . . . 10 class 𝑚
11		c1 11045	. . . . . . . . . 10 class 1
12		caddc 11047	. . . . . . . . . 10 class +
13	10, 11, 12	co 7369	. . . . . . . . 9 class (𝑚 + 1)
14		cdiv 11811	. . . . . . . . 9 class /
15	13, 10, 14	co 7369	. . . . . . . 8 class ((𝑚 + 1) / 𝑚)
16		clog 26439	. . . . . . . 8 class log
17	15, 16	cfv 6499	. . . . . . 7 class (log‘((𝑚 + 1) / 𝑚))
18		cmul 11049	. . . . . . 7 class ·
19	8, 17, 18	co 7369	. . . . . 6 class (𝑧 · (log‘((𝑚 + 1) / 𝑚)))
20	8, 10, 14	co 7369	. . . . . . . 8 class (𝑧 / 𝑚)
21	20, 11, 12	co 7369	. . . . . . 7 class ((𝑧 / 𝑚) + 1)
22	21, 16	cfv 6499	. . . . . 6 class (log‘((𝑧 / 𝑚) + 1))
23		cmin 11381	. . . . . 6 class −
24	19, 22, 23	co 7369	. . . . 5 class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
25	5, 24, 9	csu 15628	. . . 4 class Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
26	8, 16	cfv 6499	. . . 4 class (log‘𝑧)
27	25, 26, 23	co 7369	. . 3 class (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))
28	2, 7, 27	cmpt 5183	. 2 class (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
29	1, 28	wceq 1540	1 wff log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))

This definition is referenced by:  lgamgulm2  26922  lgamf  26928  iprodgam  35702