Definition df-lgam 27403

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 27400	. 2 class log Γ
2		vz	. . 3 setvar 𝑧
3		cc 11237	. . . 4 class ℂ
4		cz 12733	. . . . 5 class ℤ
5		cn 12375	. . . . 5 class ℕ
6	4, 5	cdif 4048	. . . 4 class (ℤ ∖ ℕ)
7	3, 6	cdif 4048	. . 3 class (ℂ ∖ (ℤ ∖ ℕ))
8	2	cv 1569	. . . . . . 7 class 𝑧
9		vm	. . . . . . . . . . 11 setvar 𝑚
10	9	cv 1569	. . . . . . . . . 10 class 𝑚
11		c1 11240	. . . . . . . . . 10 class 1
12		caddc 11242	. . . . . . . . . 10 class +
13	10, 11, 12	co 7451	. . . . . . . . 9 class (𝑚 + 1)
14		cdiv 12013	. . . . . . . . 9 class /
15	13, 10, 14	co 7451	. . . . . . . 8 class ((𝑚 + 1) / 𝑚)
16		clog 26939	. . . . . . . 8 class log
17	15, 16	cfv 6566	. . . . . . 7 class (log‘((𝑚 + 1) / 𝑚))
18		cmul 11244	. . . . . . 7 class ·
19	8, 17, 18	co 7451	. . . . . 6 class (𝑧 · (log‘((𝑚 + 1) / 𝑚)))
20	8, 10, 14	co 7451	. . . . . . . 8 class (𝑧 / 𝑚)
21	20, 11, 12	co 7451	. . . . . . 7 class ((𝑧 / 𝑚) + 1)
22	21, 16	cfv 6566	. . . . . 6 class (log‘((𝑧 / 𝑚) + 1))
23		cmin 11580	. . . . . 6 class −
24	19, 22, 23	co 7451	. . . . 5 class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
25	5, 24, 9	csu 15897	. . . 4 class Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
26	8, 16	cfv 6566	. . . 4 class (log‘𝑧)
27	25, 26, 23	co 7451	. . 3 class (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))
28	2, 7, 27	cmpt 5192	. 2 class (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
29	1, 28	wceq 1570	1 wff log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))

This definition is used by:  lgamgulm2  27420  lgamf  27426  iprodgam  36722