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 26523
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 26520 . 2 class log ฮ“
2 vz . . 3 setvar ๐‘ง
3 cc 11108 . . . 4 class โ„‚
4 cz 12558 . . . . 5 class โ„ค
5 cn 12212 . . . . 5 class โ„•
64, 5cdif 3946 . . . 4 class (โ„ค โˆ– โ„•)
73, 6cdif 3946 . . 3 class (โ„‚ โˆ– (โ„ค โˆ– โ„•))
82cv 1541 . . . . . . 7 class ๐‘ง
9 vm . . . . . . . . . . 11 setvar ๐‘š
109cv 1541 . . . . . . . . . 10 class ๐‘š
11 c1 11111 . . . . . . . . . 10 class 1
12 caddc 11113 . . . . . . . . . 10 class +
1310, 11, 12co 7409 . . . . . . . . 9 class (๐‘š + 1)
14 cdiv 11871 . . . . . . . . 9 class /
1513, 10, 14co 7409 . . . . . . . 8 class ((๐‘š + 1) / ๐‘š)
16 clog 26063 . . . . . . . 8 class log
1715, 16cfv 6544 . . . . . . 7 class (logโ€˜((๐‘š + 1) / ๐‘š))
18 cmul 11115 . . . . . . 7 class ยท
198, 17, 18co 7409 . . . . . 6 class (๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š)))
208, 10, 14co 7409 . . . . . . . 8 class (๐‘ง / ๐‘š)
2120, 11, 12co 7409 . . . . . . 7 class ((๐‘ง / ๐‘š) + 1)
2221, 16cfv 6544 . . . . . 6 class (logโ€˜((๐‘ง / ๐‘š) + 1))
23 cmin 11444 . . . . . 6 class โˆ’
2419, 22, 23co 7409 . . . . 5 class ((๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š))) โˆ’ (logโ€˜((๐‘ง / ๐‘š) + 1)))
255, 24, 9csu 15632 . . . 4 class ฮฃ๐‘š โˆˆ โ„• ((๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š))) โˆ’ (logโ€˜((๐‘ง / ๐‘š) + 1)))
268, 16cfv 6544 . . . 4 class (logโ€˜๐‘ง)
2725, 26, 23co 7409 . . 3 class (ฮฃ๐‘š โˆˆ โ„• ((๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š))) โˆ’ (logโ€˜((๐‘ง / ๐‘š) + 1))) โˆ’ (logโ€˜๐‘ง))
282, 7, 27cmpt 5232 . 2 class (๐‘ง โˆˆ (โ„‚ โˆ– (โ„ค โˆ– โ„•)) โ†ฆ (ฮฃ๐‘š โˆˆ โ„• ((๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š))) โˆ’ (logโ€˜((๐‘ง / ๐‘š) + 1))) โˆ’ (logโ€˜๐‘ง)))
291, 28wceq 1542 1 wff log ฮ“ = (๐‘ง โˆˆ (โ„‚ โˆ– (โ„ค โˆ– โ„•)) โ†ฆ (ฮฃ๐‘š โˆˆ โ„• ((๐‘ง ยท (logโ€˜((๐‘š + 1) / ๐‘š))) โˆ’ (logโ€˜((๐‘ง / ๐‘š) + 1))) โˆ’ (logโ€˜๐‘ง)))
Colors of variables: wff setvar class
This definition is referenced by:  lgamgulm2  26540  lgamf  26546  iprodgam  34743
  Copyright terms: Public domain W3C validator