Dirichlet Integral

From ProofWiki
Jump to navigation Jump to search

Theorem

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


Proof 1

By Fubini's Theorem:

$\ds \int_0^\infty \paren {\int_0^\infty e^{- x y} \sin x \rd y} \rd x = \int_0^\infty \paren {\int_0^\infty e^{- x y} \sin x \rd x} \rd y$


Then:

\(\ds \int_0^\infty e^{- x y} \sin x \rd y\) \(=\) \(\ds \intlimits {-e^{- x y} \frac {\sin x} x} 0 \infty\) Primitive of $e^{a x}$
\(\ds \) \(=\) \(\ds \frac {\sin x} x\)


and:

\(\ds \int_0^\infty e^{- x y} \sin x \rd x\) \(=\) \(\ds \intlimits {\frac {-e^{- x y} \paren {y \sin x + \cos x} } {y^2 + 1} } 0 \infty\) Primitive of $e^{a x} \sin b x$
\(\ds \) \(=\) \(\ds \frac 1 {y^2 + 1}\)


Hence:

\(\ds \int_0^\infty \frac {\sin x} x \rd x\) \(=\) \(\ds \int_0^\infty \frac 1 {y^2 + 1} \rd y\)
\(\ds \) \(=\) \(\ds \bigintlimits {\arctan y} 0 \infty\) Primitive of $\dfrac 1 {x^2 + a^2}$
\(\ds \) \(=\) \(\ds \frac \pi 2\) as $\ds \lim_{y \mathop \to \infty} \arctan y = \frac \pi 2$

$\blacksquare$


Proof 2

We have, by Modulus of Sine of x Less Than or Equal To Absolute Value of x:

$\ds \size {\frac {e^{-\alpha x} \sin x} x} \le e^{-\alpha x}$

We have, from Laplace Transform of Real Power:

$\ds \int_0^\infty e^{-\alpha x} \rd x = \frac 1 \alpha$

so, by Comparison Test for Improper Integral:

$\ds \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x$ converges.

So, we can define a real function $I : \hointr 0 \infty \to \R$ by:

$\ds \map I \alpha = \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x$

for each $\alpha \in \hointr 0 \infty$.


Using Definite Integral of Partial Derivative:

\(\ds \map {I'} \alpha\) \(=\) \(\ds \frac \partial {\partial \alpha} \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x\)
\(\ds \) \(=\) \(\ds \int_0^\infty \frac \partial {\partial \alpha} \frac {e^{-\alpha x} \sin x} x \rd x\) Leibniz's Integral Rule
\(\ds \) \(=\) \(\ds -\int_0^\infty e^{-\alpha x} \sin x \rd x\) Derivative of Exponential Function
\(\ds \) \(=\) \(\ds \intlimits {-\frac {e^{-\alpha x} \paren {-\alpha \sin x + \cos x} } {\paren {-\alpha}^2 + 1} } 0 \infty\) Primitive of $e^{\alpha x} \sin b x$
\(\ds \) \(=\) \(\ds -\frac 1 {\alpha^2 + 1}\)

We also have:

\(\ds \size {\map I \alpha}\) \(=\) \(\ds \size {\int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x}\)
\(\ds \) \(\le\) \(\ds \int_0^\infty \size {\frac {e^{-\alpha x} \sin x} x} \rd x\) Triangle Inequality for Definite Integrals
\(\ds \) \(\le\) \(\ds \frac 1 \alpha\)

so:

$\ds \lim_{\alpha \to \infty} \size {\map I \alpha} = 0$

That is:

$\ds \lim_{\alpha \to \infty} \map I \alpha = 0$


Note that we have:

$\ds \map I 0 = \int_0^\infty \frac {\sin x} x \rd x$

So we have:

\(\ds \int_0^\infty \frac {\sin x} x \rd x\) \(=\) \(\ds -\paren {\lim_{\alpha \to \infty} \map I \alpha - \map I 0}\)
\(\ds \) \(=\) \(\ds -\lim_{\alpha \to \infty} \paren {\map I \alpha - \map I 0}\)
\(\ds \) \(=\) \(\ds -\lim_{\alpha \to \infty} \int_0^\alpha \map {I'} \alpha \rd \alpha\) Fundamental Theorem of Calculus
\(\ds \) \(=\) \(\ds \int_0^\infty \frac 1 {\alpha^2 + 1} \rd \alpha\) Definition of Improper Integral on Closed Interval Unbounded Above
\(\ds \) \(=\) \(\ds \frac \pi 2\) Definite Integral to Infinity of $\dfrac 1 {x^2 + a^2}$

$\blacksquare$


Proof 3

Let:

$\ds \map f z = \begin{cases} \frac {e^{i z} - 1} z & z \ne 0 \\ i & z = 0\end{cases}$

We have, by Euler's Formula, for $z \in \R$:

$\ds \map \Im {\map f z} = \begin{cases}\frac {\sin z} z & z \ne 0 \\ 1 & z = 0\end{cases}$

So:

$\ds \map \Im {\int_0^\infty \dfrac {e^{i x} - 1} x \rd x} = \int_0^\infty \dfrac {\sin x} x \rd x$

Let $C_R$ be the semicircular contour of radius $R$ situated on the upper half plane, centred at the origin, traversed anti-clockwise.

Let $\Gamma_R = C_R \cup \closedint {-R} R$.

Then, by Contour Integral of Concatenation of Contours:

$\ds \oint_{\Gamma_R} \frac {e^{i z} - 1} z \rd z = \int_{C_R} \frac {e^{i z} - 1} z \rd z + \int_{-R}^R \frac {e^{i x} - 1} x \rd x$

From Linear Combination of Contour Integrals, we write:

$\ds \oint_{\Gamma_R} \frac {e^{i z} - 1} z \rd z = \int_{C_R} \frac {e^{i z} } z \rd z - \int_{C_R} \frac {\rd z} z + \int_{-R}^R \frac {e^{i x} - 1} x \rd x$

Note that $f$ is holomorphic inside our contour.

It then follows from the Cauchy-Goursat Theorem, that:

$\ds \oint_{\Gamma_R} \frac {e^{i z} - 1} z \rd z = 0$

We also have:

\(\ds \size {\int_{C_R} \frac { e^{i z} } z \rd z}\) \(\le\) \(\ds \pi \max_{0 \mathop \le \theta \mathop \le \pi} \size {\frac 1 {R e^{i \theta} } }\) Jordan's Lemma
\(\ds \) \(=\) \(\ds \frac \pi R\)
\(\ds \) \(\to\) \(\ds 0\) as $R \to \infty$

Therefore:

$\ds \lim_{R \mathop \to \infty} \int_{C_R} \frac {\rd z} z = \lim_{R \mathop \to \infty} \int_{-R}^R \frac {e^{i x} - 1} x \rd x = \int_{-\infty}^\infty \frac {e^{i x} - 1} x \rd x$

Evaluating the integral on the left hand side:

\(\ds \int_{C_R} \frac {\rd z} z\) \(=\) \(\ds \int_0^\pi \frac {i R e^{i \theta} } {R e^{i \theta} } \rd \theta\) Definition of Complex Contour Integral
\(\ds \) \(=\) \(\ds i \int_0^\pi \rd \theta\)
\(\ds \) \(=\) \(\ds \pi i\)

So:

$\ds \int_{-\infty}^\infty \frac {e^{i x} - 1} x \rd x = \pi i$

Taking the imaginary part:

$\ds \int_{-\infty}^\infty \frac {\sin x} x \rd x = \pi$

From Definite Integral of Even Function:

$\ds \int_{-\infty}^\infty \frac {\sin x} x \rd x = 2 \int_0^\infty \frac {\sin x} x \rd x$

Hence:

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

$\blacksquare$


Proof 4

From Integral to Infinity of Function over Argument:

$\ds \int_0^\infty {\dfrac {\map f x} x} = \int_0^{\to \infty} \map F u \rd u$

for a real function $f$ and its Laplace transform $\laptrans f = F$, provided they exist.

Let $\map f x := \sin x$.

Then from Laplace Transform of Sine:

$\laptrans {\map f x} = \dfrac 1 {s^2 + 1}$


Hence:

\(\ds \int_0^\infty \frac {\sin x} x \rd x\) \(=\) \(\ds \int_0^{\to \infty} \dfrac {\d u} {u^2 + 1}\)
\(\ds \) \(=\) \(\ds \bigintlimits {\arctan u} 0 \infty\) Primitive of $\dfrac 1 {x^2 + a^2}$
\(\ds \) \(=\) \(\ds \dfrac \pi 2\)

$\blacksquare$


Source of Name

This entry was named for Johann Peter Gustav Lejeune Dirichlet.