Modulus of Complex Integral

From ProofWiki
Jump to navigation Jump to search


Let $\left[{a \,.\,.\, b}\right]$ be a closed real interval.

Let $f : \left[{a \,.\,.\, b}\right] \to \C$ be a continuous complex function.


$\displaystyle \left|{\int_a^b f \left({t}\right) \rd t}\right| \le \int_a^b \left|{f \left({t}\right)}\right| \rd t$

where the first integral is a complex Riemann integral, and the second integral is a definite real integral.


Define $z \in \C$ as the value of the complex Riemann integral:

$z = \displaystyle \int_a^b f \left({t}\right) \rd t$

Define $r \in \left[{0 \,.\,.\, \infty }\right)$ as the modulus of $z$, and $\theta \in \left[{0 \,.\,.\, 2 \pi}\right)$ as the argument of $z$.

From Modulus and Argument of Complex Exponential, we have $z = re^{i \theta}$.


\(\ds r\) \(=\) \(\ds ze^{-i \theta}\) Reciprocal of Complex Exponential
\(\ds \) \(=\) \(\ds \int_a^b e^{-i \theta} f \left({t}\right) \rd t\) Linear Combination of Complex Integrals
\(\ds \) \(=\) \(\ds \int_a^b \operatorname{Re} \left({e^{-i \theta} f \left({t}\right) }\right) \rd t + i \int_a^b \operatorname{Im} \left({e^{-i \theta} f \left({t}\right) }\right) \rd t\) Definition of Complex Riemann Integral

As $r$ is wholly real, we have:

$\displaystyle 0 = \operatorname{Im}\left({r}\right) = \int_a^b \operatorname{Im} \left({e^{-i \theta} f \left({t}\right) }\right) \rd t$


\(\ds r\) \(=\) \(\ds \int_a^b \operatorname{Re} \left({e^{-i \theta} f \left({t}\right) }\right) \rd t\)
\(\ds \) \(\le\) \(\ds \int_a^b \left\vert{\operatorname{Re} \left({e^{-i \theta} f \left({t}\right) }\right) }\right\vert \rd t\) Absolute Value of Definite Integral
\(\ds \) \(\le\) \(\ds \int_a^b \left\vert{e^{-i \theta} f \left({t}\right) }\right\vert \rd t\) Modulus Larger than Real Part
\(\ds \) \(=\) \(\ds \int_a^b \left\vert{e^{-i \theta} }\right\vert \left\vert{f \left({t}\right) }\right\vert \rd t\)
\(\ds \) \(=\) \(\ds \int_a^b \left\vert{f \left({t}\right) }\right\vert \rd t\) Modulus of Exponential of Imaginary Number

As $\displaystyle r = \left|{\int_a^b f \left({t}\right) \rd t}\right|$ by its definition, the result follows.