Theorem: Dirichlet Integral

:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$

Proof:
Let $M \in \R_{>0}$.
Define a real function $I_M : \R \to \R$ by:
:$\ds \map {I_M} \alpha := \int_0^M \dfrac {\sin x} x e^{-\alpha x} \rd x$
Then, for $\alpha > 0$:
{{begin-eqn}}
{{eqn | l = \size {\map {I_M} \alpha}
      | o = \le
      | r = \int_0^M \size {\dfrac {\sin x} x e^{-\alpha x} } \rd x
      | c = Absolute Value of Definite Integral
}}
{{eqn | o = \le
      | r = \int_0^M e^{-\alpha x} \rd x
      | c = Sine Inequality $\size {\sin x} \le \size x$
}}
{{eqn | r = \intlimits {\dfrac {e^{-\alpha x} } {-\alpha} } 0 M
      | c = Primitive of $e^{ax}$
}}
{{eqn | r = \dfrac 1 \alpha - \dfrac {e^{-\alpha M} } \alpha
}}
{{eqn | n = 1
      | o = \le
      | r = \dfrac 1 \alpha
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = \map {I'_M} \alpha
      | r = \int_0^M \dfrac \partial {\partial \alpha} \paren {\dfrac {\sin x} x e^{-\alpha x} } \rd x
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = \int_0^M - \sin x e^{-\alpha x} \rd x
      | c = Primitive of $e^{ax}$
}}
{{eqn | r = \intlimits {-\frac {e^{-\alpha x} \paren {-\alpha \sin x - \cos x} } {\paren {-\alpha}^2 + 1} } 0 M 
      | c = Primitive of $e^{\alpha x} \sin b x$
}}
{{eqn | n = 2
      | r = \dfrac {-1} {\alpha^2 + 1} + \cos M \dfrac {e^{-\alpha M} }{\alpha^2 + 1} + \sin M \dfrac {\alpha e^{-\alpha M} }{\alpha^2 + 1}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \map {I_M} A - \map {I_M} 0
      | r = \int_0^A \map {I'_M} \alpha \rd \alpha
      | c = Fundamental Theorem of Calculus
}}
{{eqn | r = - \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} + \cos M \int_0^A \dfrac {e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha + \sin M \int_0^A \dfrac {\alpha e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha
      | c = by $\paren 2$ and Linear Combination of Integrals
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \size {\map {I_M} A - \map {I_M} 0 + \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} }
      | r = \size {\cos M \int_0^A \dfrac {e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha + \sin M \int_0^A \dfrac {\alpha e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha}
}}
{{eqn | o = \le
      | r = \size {\cos M \int_0^A \dfrac {e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha} + \size {\sin M \int_0^A \dfrac {\alpha e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha }
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = \le
      | r = \int_0^A \dfrac {e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha + \int_0^A \dfrac {\alpha e^{-\alpha M} }{\alpha^2 + 1} \rd \alpha
}}
{{eqn | o = \le
      | r = 2 \int_0^A e^{-\alpha M} \rd \alpha
}}
{{eqn | n = 3
      | o = \le
      | r = \dfrac 2 M
      | c = similarly to $\paren 1$
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \size {\map {I_M} 0 - \dfrac \pi 2}
      | r = \size {\paren {\map {I_M} A - \map {I_M} A } + \map {I_M} 0 + \paren {-\int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} + \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} } -\dfrac \pi 2}
      | c = adding zero
}}
{{eqn | r = \size {\map {I_M} A - \paren {\map {I_M} A -\map {I_M} 0 + \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} } + \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} -\dfrac \pi 2}
      | c = rearranging
}}
{{eqn | o = \le
      | r = \size {\map {I_M} A} + \size {\map {I_M} A -\map {I_M} 0 + \int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} } + \size {\int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} - \dfrac \pi 2}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = \le
      | r = \dfrac 1 A + \dfrac 2 M + \size {\int_0^A \dfrac {\rd \alpha} {\alpha^2 + 1} - \dfrac \pi 2}
      | c = by $\paren 1$ and $\paren 3$
}}
{{eqn | o = \to
      | r = \dfrac 2 M
      | c = as $A \to +\infty$ by Definite Integral to Infinity of $\dfrac 1 {x^2 + a^2}$
}}
{{end-eqn}}
As:
:$\ds \map {I_M} 0 = \int_0^M \dfrac {\sin x} x \rd x$
we have shown:
:$\ds \forall  M \in \R_{>0} : \size {\int_0^M \dfrac {\sin x} x \rd x - \dfrac \pi 2} \le \dfrac 2 M$
In particular:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \dfrac {\sin x} x \rd x
      | r = \lim_{M \mathop \to +\infty} \int_0^M \dfrac {\sin x} x \rd x
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \dfrac \pi 2
}}
{{end-eqn}}
{{qed}}