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 24966
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 24963 . 2 class log Γ
2 vz . . 3 setvar 𝑧
3 cc 10136 . . . 4 class
4 cz 11579 . . . . 5 class
5 cn 11222 . . . . 5 class
64, 5cdif 3720 . . . 4 class (ℤ ∖ ℕ)
73, 6cdif 3720 . . 3 class (ℂ ∖ (ℤ ∖ ℕ))
82cv 1630 . . . . . . 7 class 𝑧
9 vm . . . . . . . . . . 11 setvar 𝑚
109cv 1630 . . . . . . . . . 10 class 𝑚
11 c1 10139 . . . . . . . . . 10 class 1
12 caddc 10141 . . . . . . . . . 10 class +
1310, 11, 12co 6793 . . . . . . . . 9 class (𝑚 + 1)
14 cdiv 10886 . . . . . . . . 9 class /
1513, 10, 14co 6793 . . . . . . . 8 class ((𝑚 + 1) / 𝑚)
16 clog 24522 . . . . . . . 8 class log
1715, 16cfv 6031 . . . . . . 7 class (log‘((𝑚 + 1) / 𝑚))
18 cmul 10143 . . . . . . 7 class ·
198, 17, 18co 6793 . . . . . 6 class (𝑧 · (log‘((𝑚 + 1) / 𝑚)))
208, 10, 14co 6793 . . . . . . . 8 class (𝑧 / 𝑚)
2120, 11, 12co 6793 . . . . . . 7 class ((𝑧 / 𝑚) + 1)
2221, 16cfv 6031 . . . . . 6 class (log‘((𝑧 / 𝑚) + 1))
23 cmin 10468 . . . . . 6 class
2419, 22, 23co 6793 . . . . 5 class ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
255, 24, 9csu 14624 . . . 4 class Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))
268, 16cfv 6031 . . . 4 class (log‘𝑧)
2725, 26, 23co 6793 . . 3 class 𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧))
282, 7, 27cmpt 4863 . 2 class (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
291, 28wceq 1631 1 wff log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
Colors of variables: wff setvar class
This definition is referenced by:  lgamgulm2  24983  lgamf  24989  iprodgam  31966
  Copyright terms: Public domain W3C validator