MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lgam Structured version   Visualization version   GIF version

Definition df-lgam 27077
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
StepHypRef Expression
1 clgam 27074 . 2 class log Γ
2 vz . . 3 setvar 𝑧
3 cc 11151 . . . 4 class
4 cz 12611 . . . . 5 class
5 cn 12264 . . . . 5 class
64, 5cdif 3960 . . . 4 class (ℤ ∖ ℕ)
73, 6cdif 3960 . . 3 class (ℂ ∖ (ℤ ∖ ℕ))
82cv 1536 . . . . . . 7 class 𝑧
9 vm . . . . . . . . . . 11 setvar 𝑚
109cv 1536 . . . . . . . . . 10 class 𝑚
11 c1 11154 . . . . . . . . . 10 class 1
12 caddc 11156 . . . . . . . . . 10 class +
1310, 11, 12co 7431 . . . . . . . . 9 class (𝑚 + 1)
14 cdiv 11918 . . . . . . . . 9 class /
1513, 10, 14co 7431 . . . . . . . 8 class ((𝑚 + 1) / 𝑚)
16 clog 26611 . . . . . . . 8 class log
1715, 16cfv 6563 . . . . . . 7 class (log‘((𝑚 + 1) / 𝑚))
18 cmul 11158 . . . . . . 7 class ·
198, 17, 18co 7431 . . . . . 6 class (𝑧 · (log‘((𝑚 + 1) / 𝑚)))
208, 10, 14co 7431 . . . . . . . 8 class (𝑧 / 𝑚)
2120, 11, 12co 7431 . . . . . . 7 class ((𝑧 / 𝑚) + 1)
2221, 16cfv 6563 . . . . . 6 class (log‘((𝑧 / 𝑚) + 1))
23 cmin 11490 . . . . . 6 class
2419, 22, 23co 7431 . . . . 5 class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
255, 24, 9csu 15719 . . . 4 class Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
268, 16cfv 6563 . . . 4 class (log‘𝑧)
2725, 26, 23co 7431 . . 3 class 𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))
282, 7, 27cmpt 5231 . 2 class (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
291, 28wceq 1537 1 wff log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  lgamgulm2  27094  lgamf  27100  iprodgam  35722
  Copyright terms: Public domain W3C validator