Is the distribution of the real part of product of two independent complex variates exponential? Trying to find the pdf of the real part x of the product $z_1z_2$ of two uncorrelated complex random Gaussian variates  .  The pdf of the modulus $r \equiv  |z_1z_2|$ is known 
$ f_r(r)=rK_0(r)$ from Wells, Anderson and Cell 1962: "The Distribution of the Product...",  $\theta $ is uniform on $[0,2\pi]$. So the marginal pdf on x is found by integrating on the y-axis:
$$
f_x(x)= \frac{1}{2\pi}\int _{- \infty} ^\infty  rK_0(r)dy
$$
By a change of variable $y=\sqrt{r^2 - x^2}$ I get 
$$
f_x(x)= \frac{1}{\pi}\int _{|x|} ^\infty  rK_0(r)\frac{dy}{dr}dr=
\frac{1}{\pi}\int _{|x|} ^\infty \frac{ r}{\sqrt{r^2-x^2}} K_0(r) dr
$$
Remarkably this definite integral evaluates numerically to a simple double-sided exponential. To computer precision $f_x(x)=0.5e^{-|x|} \pm 10^{-8}$.
Is this a known result, can it be proved or is it trivial? I searched through the Bessel section in Gradshteyn and Ryzhik to no avail.
 A: $\newcommand{\ep}{\epsilon}
\newcommand{\ga}{\gamma}
\newcommand{\Ga}{\Gamma}
\newcommand{\la}{\lambda}
\newcommand{\Si}{\Sigma}
\newcommand{\thh}{\theta}
\newcommand{\R}{\mathbb{R}}
\newcommand{\E}{\operatorname{\mathsf E}} 
\newcommand{\PP}{\operatorname{\mathsf P}}$ 
Here is a rather elementary derivation of the double-sided exponential distribution for the real part (say $R$) of the product of two standard independent complex random variables (r.v.'s). We have $R=U-V$, where $U$ and $V$ are iid r.v.'s such that $U=XY$, where $X$ and $Y$ are iid standard normal (real-valued) r.v.'s. Since the r.v. $V$ is symmetrically distributed, we can write 
\begin{equation}
 f=g^2,
\end{equation}
where $f$ and $g$ are the characteristic functions (c.f.'s) of $R$ and $U$, respectively. Next, using the polar coordinates, for real $t$ we have
\begin{multline*}
 g(t)=\E e^{itXY}=\int_{-\infty}^\infty\int_{-\infty}^\infty e^{itxy}\frac1{2\pi}\,e^{-(x^2+y^2)/2}dx\,dy \\ 
 =\frac1{2\pi}\,\int_0^{2\pi}d\thh\int_0^\infty r\,dr\, e^{-r^2(1-it\sin2\thh)/2}
 =\frac1{2\pi}\,\int_0^{2\pi}\frac{d\thh}{1-it\sin2\thh}
 =\frac1{\sqrt{1+t^2}}
\end{multline*}
(to evaluate the latter integral, use the standard substitution $u=\tan\thh$, $d\thh=\frac{du}{1+u^2}$, $\sin2\thh=\frac{2u}{1+u^2}$ to reduce it to the integral of a rational function.) 
So, for all real $t$ 
\begin{equation}
 f(t)=\frac1{1+t^2}, 
\end{equation}
which is easily seen to be the expression of the c.f. of the double-sided exponential distribution, as desired.
