Is this distribution already known and has a name?

Question

My question is whether the distribution on $\Bbb R$ with probability density $$ f(x) := \frac 2 {\sqrt{2\pi}} e^{-\frac{x^2}{2}} - 2 \vert x\vert \int_{\vert x \vert}^\infty \frac 1{\sqrt{2\pi}} e^{-\frac{y^2} 2} \text d y$$ is already appearing in some context or even has a name or is part of a wider class of distributions.

Here it is. I discovered the following. Let $U_n$ be uniformly distributed on $\{1, \ldots , n \}$ and $X_{n,k}$ normal distributed with mean $0$ and variance $k/n$, independent. Then $$X_{n, U_n} \to Z$$ where $Z$ has the density above. Proof: The characteristic function of $X_{n, U_n}$ converges pointwise to $$t \mapsto \frac{1 - e^{- \frac 1 2 t^2 }}{\frac 1 2 t^2 }$$ By Levy's continuity theorem the laws of $X_{n, U_n}$ have a weak limit. By Fourier inversion one can derive the density of $Z$.

Answer 1

Unfortunately, this turns out to be less interesting than I thought. After a short comment of a collegue I found out that this convergence phenomenon is just a special case of the following easy statement:

Let $V_n$ and $V$ be random variables with $V_n \to V$ in distribution. Let $K$ be a stochastic kernel with the $C_b$-Feller property (i.e. $ v \mapsto Kf(v) := \int f(x)K(v, \text d x)$ is continuous for every continuous and bounded function $f$.). Given $V_n = v_n$ let $X_n \sim K(v_n, \cdot )$ and given $V = v$ let $X\sim K(v, \cdot)$. Then $X_n \to X$ in distribution. Proof: Let $f$ be continuous and bounded. Since $Kf$ is continous and bounded and $V_n \to V$ in distribution we have $$\Bbb E [f(X_n)] = \Bbb E[Kf(V_n)] \to \Bbb E[Kf(V)] = \Bbb E[f(X)] \tag*{$\blacksquare$}$$

In this case:

$V_n := U_n /n$, $V$ uniform distributed on $(0,1)$. It is easy to check that $V_n \to V$ in distribution.

$K(v, A) := \int_A \frac{1}{\sqrt{2\pi v}} e^{-{\frac{x^2}{2v}}} \text d x$ (has Feller property by dominated convergence theorem)

Therefore $Z\sim X$ with $X \sim\mathcal N (0, v)$ given $V=v$, which can be also seen by computing the characteristic function of $\mathcal N (0, V)$ (one can compute the density easily, too):

$$\Bbb E[e^{it X}] = \int_0^1 \Bbb E [e^{itX} \vert V=v] \text d v = \int_0^1 e^{-\frac 1 2 t^2 v} \text d v = \frac{1-e^{-\frac 1 2 t^2}}{\frac 1 2 t^2}$$

In retrospect this distribution makes intuitivly and perfectly sense of course.