Theorem: Definite Integral to Infinity of Exponential of -a x by One minus Cosine x over x Squared

:$\ds \int_0^\infty \frac {e^{-a x} \paren {1 - \cos x} } {x^2} \rd x = \arccot a - \frac a 2 \map \ln {a^2 + 1} + a \ln a$

Proof:
Set: 
:$\ds \map I a = \int_0^\infty \frac {e^{-a x} \paren {1 - \cos x} } {x^2} \rd x$
for $a > 0$.
We have: 
{{begin-eqn}}
{{eqn | l = \map {I''} a
      | r = \frac {\d^2} {\d a^2} \int_0^\infty \frac {e^{-a x} \paren {1 - \cos x} } {x^2} \rd x
}}
{{eqn | r = \frac \d {\d a} \int_0^\infty \frac \partial {\partial a} \paren {\frac {e^{-a x} \paren {1 - \cos x} } {x^2} } \rd x
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = -\frac \d {\d a} \int_0^\infty \frac {e^{-a x} \paren {1 - \cos x} } x \rd x
      | c = Derivative of $e^{a x}$
}}
{{eqn | r = -\int_0^\infty \frac \partial {\partial a} \paren {\frac {e^{-a x} \paren {1 - \cos x} } x} \rd x
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = \int_0^\infty e^{-a x} \paren {1 - \cos x} \rd x
      | c = Derivative of $e^{a x}$
}}
{{eqn | r = \int_0^\infty e^{-a x} \rd x - \int_0^\infty e^{-a x} \cos x \rd x
}}
{{eqn | r = \intlimits {-\frac {e^{-a x} } a} 0 \infty - \frac a {a^2 + 1}
      | c = Primitive of $e^{a x}$, Definite Integral to Infinity of $e^{-a x} \cos b x$
}}
{{eqn | r = \frac 1 a - \frac a {a^2 + 1}
      | c = Exponential of Zero, Exponential Tends to Zero and Infinity
}}
{{end-eqn}}
We then have, from Primitive of $\dfrac 1 x$ and Primitive of $\dfrac x {x^2 + a^2}$:
:$\ds \map {I'} a = \ln a - \frac 1 2 \map \ln {a^2 + 1} + C$
for some constant $C \in \R$. 
Note that: 
{{begin-eqn}}
{{eqn | l = \lim_{a \mathop \to \infty} \map {I'} a
      | r = \lim_{a \mathop \to \infty} \int_0^\infty \frac {e^{-a x} \cos x} x \rd x
}}
{{eqn | r = \int_0^\infty \frac 0 x \rd x
}}
{{eqn | r = 0
}}
{{end-eqn}}
On the other hand: 
{{begin-eqn}}
{{eqn | l = \lim_{a \mathop \to \infty} \map {I'} a
      | r = \lim_{a \mathop \to \infty} \paren {\ln a - \frac 1 2 \map \ln {a^2 + 1} + C}
}}
{{eqn | r = C + \lim_{a \mathop \to \infty} \paren {\map \ln {\frac a {\sqrt {a^2 + 1} } } }
      | c = Logarithm of Power, Difference of Logarithms
}}
{{eqn | r = C + \lim_{a \mathop \to \infty} \paren {\map \ln {\frac 1 {\sqrt {1 + \frac 1 {a^2} } } } }
}}
{{eqn | r = C + \ln 1
}}
{{eqn | r = C
      | c = Logarithm of 1 is 0
}}
{{end-eqn}}
so:
:$\ds \map {I'} a = \ln a - \frac 1 2 \map \ln {a^2 + 1}$
We have: 
{{begin-eqn}}
{{eqn | l = \map I a
      | r = \int \map {I'} a \rd a
}}
{{eqn | r = \int \ln a \rd a - \frac 1 2 \int \map \ln {a^2 + 1} \rd a
}}
{{eqn | r = a \ln a - a - \frac 1 2 \paren {a \map \ln {a^ 2 + 1} - 2 a + 2 \arctan a} + C_2
      | c = Primitive of $\ln x$, Primitive of $\map \ln {x^2 + a^2}$
}}
{{eqn | r = a \ln a - a - \frac 1 2 a \map \ln {a^2 + 1} + a - \arctan a + C_2
}}
{{eqn | r = a \ln a - \frac 1 2 a \map \ln {a^2 + 1} - \arctan a + C_2
}}
{{end-eqn}}
for some constant $C_2 \in \R$.
Similarly we have: 
{{begin-eqn}}
{{eqn | l = \lim_{a \mathop \to \infty} \int_0^\infty \frac {e^{-a x} \paren {1 - \cos x} } {x^2} \rd x
      | r = \int_0^\infty \frac 0 {x^2} \rd x
}}
{{eqn | r = 0
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = \lim_{a \mathop \to \infty} \map I a
      | r = \lim_{a \mathop \to \infty} \map \ln {\frac {a^a} {\paren {\sqrt {a^2 + 1} }^a} } - \lim_{a \mathop \to \infty} \paren {\arctan a} + C_2
}}
{{eqn | r = \lim_{a \mathop \to \infty} \map \ln {\frac 1 {\paren {\sqrt {1 + \frac 1 {a^2} } }^a} } - \frac \pi 2 + C_2
      | c = Limit of Arctangent Function
}}
{{eqn | r = C_2 - \frac \pi 2
}}
{{end-eqn}}
We hence have: 
{{begin-eqn}}
{{eqn | l = \map I a
      | r = a \ln a - \frac 1 2 a \map \ln {a^2 + 1} + \paren {\frac \pi 2 - \arctan a}
}}
{{eqn | r = a \ln a - \frac 1 2 a \map \ln {a^2 + 1} + \arccot a
      | c = Arccotangent Function in terms of Arctangent
}}
{{end-eqn}}
{{qed}}