Theorem: Binet's Formula for Logarithm of Gamma Function/Formulation 1

Let $z$ be a complex number with a strictly positive real part.
Then: 
:$\ds \Ln \map \Gamma z = \paren {z - \frac 1 2} \Ln z - z + \frac 1 2 \ln 2 \pi + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t$
where: 
:$\Gamma$ is the Gamma function
:$\Ln$ is the principal branch of the complex logarithm.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d z} } {\Ln \map \Gamma {z + 1} }
      | r = \int_0^\infty \paren {\frac {e^{-t} } t - \frac {e^{-t \paren {z + 1} } } {1 - e^{-t} } } \rd t
      | c = Gauss's Integral Form of Digamma Function and {{Defof|Digamma Function}}
}}
{{eqn | r = \int_0^\infty \frac {e^{-t} } t  \rd t - \int_0^\infty \frac {e^{-z t} e^{-t} } {1 - e^{-t} } \rd t
      | c = Linear Combination of Integrals
}}
{{eqn | r = \int_0^\infty \frac {e^{-t} } t  \rd t - \int_0^\infty \frac {e^{-z t} e^{-t} } {1 - e^{-t} } \times \dfrac {e^t} {e^t} \rd t
      | c = multiplying top and bottom by $e^t$
}}
{{eqn | r = \int_0^\infty \frac {e^{-t} } t  \rd t - \int_0^\infty \frac {e^{-t z} } {e^t - 1} \rd t
      | c = Product of Powers
}}
{{eqn | r = \int_0^\infty \frac {e^{-t} } t  \rd t - \int_0^\infty \frac {e^{-t z} } {e^t - 1} \rd t + \paren {\frac 1 2 \int_0^\infty e^{-t z} \rd t - \frac 1 2 \int_0^\infty e^{-t z} \rd t} + \paren {\int_0^\infty \frac {e^{-t z} } t  \rd t - \int_0^\infty \frac {e^{-t z} } t \rd t}
      | c = adding $0$
}}
{{eqn | r = \frac 1 2 \int_0^\infty e^{-t z} \rd t + \int_0^\infty \frac {e^{-t} - e^{-t z} } t  \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } e^{-t z} \rd t 
      | c = rearranging and Linear Combination of Integrals
}}
{{eqn | r = \frac 1 2 \intlimits {-\frac 1 z e^{-t z} } 0 \infty + \int_0^\infty \frac {e^{-t} - e^{-t z} } t  \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } e^{-t z} \rd t 
      | c = Primitive of Exponential of a x
}}
{{eqn | r = \frac 1 {2 z} + \map \ln z - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } e^{-t z} \rd t 
      | c = Logarithm as definite integral of difference of exponentials: $\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } x \rd x = \ln \frac b a$
}}
{{eqn | ll= \leadsto
      | l = \int_1^z \map {\dfrac \d {\d z} } {\Ln \map \Gamma {z + 1} } \d z
      | r = \int_1^z \paren {\frac 1 {2 z} + \map \ln z - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } e^{-t z} \rd t} \d z
      | c = integrating over $z$ from $1$ to $z$
}}
{{eqn | ll= \leadsto
      | l = \Ln \map \Gamma {z + 1}
      | r = \frac 1 2 \bigintlimits {\map \ln z} 1 z + \bigintlimits {\map z \ln z - z} 1 z - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \intlimits {-\frac 1 t e^{-t z} } 1 z \rd t 
      | c = Primitive of Reciprocal, Primitive of Logarithm of x, Primitive of Exponential of a x
}}
{{eqn | r = \frac 1 2 \map \ln z + z \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} - e^{-t} } t \rd t
      | c = 
}}
{{eqn | r = \frac 1 2 \map \ln z + z \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t} } t \rd t
      | c = Linear Combination of Integrals
}}
{{eqn | ll= \leadsto
      | l = \map \Ln {z \map \Gamma z}
      | r = \frac 1 2 \map \ln z + z \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t} } t \rd t
      | c = Gamma Difference Equation
}}
{{eqn | ll= \leadsto
      | l = \map \Ln {\map \Gamma z} + \map \ln z
      | r = \frac 1 2 \map \ln z + z \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t } } t \rd t
      | c = Sum of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \map \Ln {\map \Gamma z}
      | r = \paren {z - \frac 1 2} \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t } } t \rd t
      | c = rearranging
}}
{{end-eqn}}
Setting $z:= \dfrac 1 2$, we obtain:
{{begin-eqn}}
{{eqn | l = \map \Ln {\map \Gamma {\frac 1 2} }
      | r = \paren {\frac 1 2 - \frac 1 2} \map \ln {\frac 1 2} - \frac 1 2 + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t } } t \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \Ln {\pi^{\frac 1 2} }
      | r = \frac 1 2 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t } } t \rd t
      | c = Gamma Function of One Half
}}
{{eqn | ll= \leadsto
      | l = \frac 1 2 \map \Ln {\pi }
      | r = \frac 1 2 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t } } t \rd t
      | c = Logarithm of Power
}}
{{end-eqn}}
Let:
:$\ds J = \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2} } t \rd t$
:$\ds I = \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t} } t \rd t$
Then our last equation becomes:
:$\ds \frac 1 2 \map \Ln {\pi } = \dfrac 1 2 + J - I$
Setting $t:= \dfrac 1 2 u$ and $\rd t = \dfrac 1 2 \rd u$ we can rewrite $I$ as:
{{begin-eqn}}
{{eqn | l = I
      | r = \int_0^\infty \paren {\frac 1 2 - \frac 1 {\frac 1 2 u} + \frac 1 {e^{u/2} - 1} } \frac {e^{-u/2 } } {\frac 1 2 u} \paren {\frac 1 2 \rd u}
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 2 - \frac 2 u + \frac 1 {e^{u/2} - 1} } \frac {e^{-u/2} } u \rd u
      | c = simplifying
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 2 - \frac 2 t + \frac 1 {e^{t/2} - 1} } \frac {e^{-t/2} } t \rd t
      | c = rewriting with $t$
}}
{{end-eqn}}
Therefore, taking the difference of $J$ and $I$, we obtain:
{{begin-eqn}}
{{eqn | l = J - I
      | r = \paren {\int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2 } } t \rd t} - \paren {\int_0^\infty \paren {\frac 1 2 - \frac 2 t + \frac 1 {e^{t/2} - 1} } \frac {e^{-t/2 } } t \rd t}
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\paren {\frac 1 2 - \frac 1 2} + \paren { -\frac 1 t + \frac 2 t} + \paren {\frac 1 {e^t - 1} - \frac 1 {e^{t/2} - 1} } } \frac {e^{-t/2 } } t \rd t
      | c = Linear Combination of Integrals
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 t + \paren {\frac {\paren {e^{t/2} - 1} - \paren {e^t - 1} } {\paren {e^t - 1} \paren {e^{t/2} - 1} } } } \frac {e^{-t/2 } } t \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 t - \paren {\frac {e^{t/2} \paren {e^{t/2} - 1} } {\paren {e^t - 1} \paren {e^{t/2} - 1} } } } \frac {e^{-t/2 } } t \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 t - \frac {e^{t/2} } {\paren {e^t - 1} } } \frac {e^{-t/2 } } t \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} } t - \frac 1 {\paren {e^t - 1} } } \frac 1 t \rd t
      | c = 
}}
{{end-eqn}}
Solving for $J$, we obtain:
{{begin-eqn}}
{{eqn | l = J
      | r = \paren {J - I} + I
      | c = 
}}
{{eqn | r = \paren {\int_0^\infty \paren {\frac {e^{-t/2} } t - \frac 1 {\paren {e^t - 1} } } \frac 1 t \rd t } + \paren {\int_0^\infty \paren {\frac {e^{-t} } 2 - \frac {e^{-t} } t + \frac {e^{-t} } {e^t - 1} } \frac 1 t \rd t}
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {e^{-t} } 2 - \frac 1 {\paren {e^t - 1} } + \frac {e^{-t} } {e^t - 1} } } \frac 1 t \rd t 
      | c = Linear Combination of Integrals
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {e^{-t} \paren {e^t - 1} - 2 + 2 e^{-t} } {2 \paren {e^t - 1} } } } \frac 1 t \rd t 
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {1 - e^{-t} - 2 + 2 e^{-t} } {2 \paren {e^t - 1} } } } \frac 1 t \rd t 
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {e^{-t} - 1} {2 \paren {e^t - 1} } } } \frac 1 t \rd t 
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {e^{-t} - 1} {2 \paren {e^t - 1} } \times \frac {e^t} {e^t} } } \frac 1 t \rd t 
      | c = multiplying top and bottom by $e^t$
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t + \paren {\frac {1 - e^t} {2 e^t \paren {e^t - 1} } } } \frac 1 t \rd t 
      | c = Product of Powers
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } t - \frac 1 {2 e^t} } \frac 1 t \rd t 
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {e^{-t/2} - e^{-t} } {t^2} - \frac {e^{-t} } {2 t} } \rd t 
      | c = 
}}
{{eqn | r = \int_0^\infty \paren {\frac {- \paren {e^{-t} - e^{t/2} } } {t^2} + \paren {\paren { \frac {e^{-t/2 } - 2 e^{-t} } {2 t} } - \paren { \frac {e^{-t/2 } - 2 e^{-t} } {2 t} } } - \frac {e^{-t} } {2 t} } \rd t 
      | c = adding $0$
}}
{{eqn | r = \int_0^\infty \paren {\frac {t \paren {-e^{-t} + \frac 1 2 e^{-t/2} } - \paren {e^{-t} - e^{t/2} } } {t^2} - \paren { \frac {e^{-t/2 } - 2 e^{-t} } {2 t} } - \frac {e^{-t} } {2 t} } \rd t 
      | c = rearranging
}}
{{eqn | r = \int_0^\infty \paren {\map {\dfrac \d {\d t} } {\frac {e^{-t} - e^{-t/2 } } t }  - \paren { \frac {e^{-t/2 } - 2 e^{-t} } {2 t} } - \frac {e^{-t} } {2 t} } \rd t 
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \int_0^\infty \paren {\map {\dfrac \d {\d t} } {\frac {e^{-t} - e^{-t/2 } } t }  + \paren { \frac { e^{-t} - e^{-t/2 } } {2 t} } } \rd t 
      | c = 
}}
{{eqn | r = \intlimits {\frac {e^{-t} - e^{-t/2 } } t } 0 \infty + \frac 1 2 \int_0^\infty \paren { \frac { e^{-t} - e^{-t/2 } } t }  \rd t 
      | c = Linear Combination of Integrals
}}
{{eqn | r = 0 - \paren {\frac {-e^{-0} + \frac 1 2 e^{-0/2 } } 1 }  + \frac 1 2 \int_0^\infty \paren { \frac { e^{-t} - e^{-t/2 } } t }  \rd t 
      | c = L'Hôpital's Rule, Derivative of Power, Derivative of Exponential Function
}}
{{eqn | r = 0 - \paren {-\frac 1 2}  + \frac 1 2 \int_0^\infty \paren { \frac { e^{-t} - e^{-t/2 } } t }  \rd t 
      | c = Exponential of Zero
}}
{{eqn | r = \frac 1 2 + \frac 1 2 \map \ln {\frac 1 2 } 
      | c = Logarithm as definite integral of difference of exponentials: $\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } x \rd x = \ln \frac b a$
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \frac 1 2 \map \Ln {\pi }
      | r = \dfrac 1 2 + \paren {\frac 1 2 + \frac 1 2 \map \ln {\frac 1 2 } } - I
      | c = 
}}
{{eqn | ll= \leadsto
      | l = I
      | r = 1 - \frac 1 2 \map \ln \pi + \frac 1 2 \paren {\map \ln 1 - \map \ln 2}
      | c = rearranging, Difference of Logarithms
}}
{{eqn | ll= \leadsto
      | l = I
      | r = 1 - \frac 1 2 \map \ln {2 \pi}
      | c = Sum of Logarithms and Logarithm of 1 is 0
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \map \Ln {\map \Gamma z}
      | r = \paren {z - \frac 1 2} \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t} } t \rd t
      | c = 
}}
{{eqn | r = \paren {z - \frac 1 2} \ln z - z + 1 + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t - \paren {1 - \frac 1 2 \map \ln {2 \pi} }
      | c = substituting $I = 1 - \dfrac 1 2 \map \ln {2 \pi}$
}}
{{eqn | r = \paren {z - \frac 1 2} \Ln z - z + \frac 1 2 \ln 2 \pi + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Jacques Philippe Marie Binet}}