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

Definition df-lgam 25703
 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 25700 . 2 class log Γ
2 vz . . 3 setvar 𝑧
3 cc 10573 . . . 4 class
4 cz 12020 . . . . 5 class
5 cn 11674 . . . . 5 class
64, 5cdif 3855 . . . 4 class (ℤ ∖ ℕ)
73, 6cdif 3855 . . 3 class (ℂ ∖ (ℤ ∖ ℕ))
82cv 1537 . . . . . . 7 class 𝑧
9 vm . . . . . . . . . . 11 setvar 𝑚
109cv 1537 . . . . . . . . . 10 class 𝑚
11 c1 10576 . . . . . . . . . 10 class 1
12 caddc 10578 . . . . . . . . . 10 class +
1310, 11, 12co 7150 . . . . . . . . 9 class (𝑚 + 1)
14 cdiv 11335 . . . . . . . . 9 class /
1513, 10, 14co 7150 . . . . . . . 8 class ((𝑚 + 1) / 𝑚)
16 clog 25245 . . . . . . . 8 class log
1715, 16cfv 6335 . . . . . . 7 class (log‘((𝑚 + 1) / 𝑚))
18 cmul 10580 . . . . . . 7 class ·
198, 17, 18co 7150 . . . . . 6 class (𝑧 · (log‘((𝑚 + 1) / 𝑚)))
208, 10, 14co 7150 . . . . . . . 8 class (𝑧 / 𝑚)
2120, 11, 12co 7150 . . . . . . 7 class ((𝑧 / 𝑚) + 1)
2221, 16cfv 6335 . . . . . 6 class (log‘((𝑧 / 𝑚) + 1))
23 cmin 10908 . . . . . 6 class
2419, 22, 23co 7150 . . . . 5 class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
255, 24, 9csu 15090 . . . 4 class Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
268, 16cfv 6335 . . . 4 class (log‘𝑧)
2725, 26, 23co 7150 . . 3 class 𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))
282, 7, 27cmpt 5112 . 2 class (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
291, 28wceq 1538 1 wff log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
 Colors of variables: wff setvar class This definition is referenced by:  lgamgulm2  25720  lgamf  25726  iprodgam  33223
 Copyright terms: Public domain W3C validator