Proof of The Gaussian Weight Defines a Probability Distribution

We keep the notation of the statement, use the $[0,\infty]$-valued measurability and integral of Lebesgue Integral of a Nonnegative Measurable Function, and use the vocabulary jointly Borel of Joint Distribution, Expectations, and Block Independence for Independent Random Variables for maps on $\mathbb{R}^2$ measurable with respect to $\mathcal{B}(\mathbb{R})\otimes\mathcal{B}(\mathbb{R})$. From Basic Properties of the Exponential Function: $\exp$ is positive, strictly increasing, satisfies $\exp(s+t)=\exp(s)\exp(t)$ and $\exp'=\exp$, and from the defining series $\exp(t)\ge1+t\ge t$ for $t\ge0$; the natural logarithm $\ln$ is its inverse, so for $s>0$ and real $w$: $\exp(w)>s\iff w>\ln s$, and $\exp(-\ln s)=1/s$ by the product property. Note $g$ is continuous, hence Borel measurable, and $0<g\le1$.

Claim 1. $\nu(\emptyset)=0$. For pairwise disjoint Borel $B_j$: $\mathbf{1}_{\bigcup_jB_j}\,g=\sum_j\mathbf{1}_{B_j}g$ pointwise, the partial sums are nondecreasing, finite sums pull out of the integral by claim 1 of Linearity and Monotonicity of the Lebesgue Integral, and Monotone Convergence Theorem gives $\nu(\bigcup_jB_j)=\sum_j\nu(B_j)$. So $\nu$ is a measure.

Claim 2. For $|x|\ge2$ we have $x^{2}/2\ge|x|$, so $g(x)\le\exp(-|x|)$ by monotonicity of $\exp$. Moreover $\int_{\mathbb{R}}\exp(-|x|)\,d\lambda\le4$: by monotonicity of the integral on each interval $[k,k+1)$ (where $\exp(-x)\le\exp(-k)$, a constant on an interval of Lebesgue measure one), the simple-function bounds and Monotone Convergence Theorem along $\mathbf{1}_{[0,L)}\exp(-x)\uparrow\mathbf{1}_{[0,\infty)}\exp(-x)$ give $\int_{[0,\infty)}\exp(-x)\,d\lambda\le\sum_{k\ge0}\exp(-1)^{k}\le2$ (geometric series; $\exp(1)\ge2$ from the series, so $\exp(-1)\le1/2$), and the negative half-line contributes the same by the reflection instance of Preliminary (P2) of the proof of Moments and Stability of the Standard Normal Distribution. Hence, splitting $\mathbb{R}$ into $[-2,2]$ and its complement and using $g\le1$,

Also $c>0$: $g$ is nonincreasing in $|x|$, so $g\ge g(1)=\exp(-1/2)>0$ on $[-1,1]$, whence $c\ge\exp(-1/2)\,\lambda([-1,1])=2\exp(-1/2)>0$ by monotonicity. Finally $N=\nu/c$ is a measure (additivity is preserved under multiplication by the constant $1/c$) with $N(\mathbb{R})=c/c=1$, a probability measure.

Claim 3. For $s<t$, additivity gives $\nu((-\infty,t])-\nu((-\infty,s])=\nu((s,t])=\int\mathbf{1}_{(s,t]}\,g\,d\lambda\le\int\mathbf{1}_{(s,t]}\,d\lambda=t-s$, using $g\le1$, monotonicity, and interval lengths. So $t\mapsto\nu((-\infty,t])$ satisfies $|\nu((-\infty,t])-\nu((-\infty,s])|\le|t-s|$ and is continuous at every point of the real line $(\mathbb{R},d_{\mathbb{R}})$, whose metric is $d_{\mathbb{R}}(s,t)=|s-t|$ (take $\delta=\varepsilon$); dividing by $c$, $\Phi$ is continuous on $\mathbb{R}$.

Claim 4. Write $g_2(x,y)=g(x)g(y)$, jointly Borel: coordinate projections are jointly Borel and compositions with Borel maps remain jointly Borel (claim 4 of Joint Distribution, Expectations, and Block Independence for Independent Random Variables), and products of jointly Borel functions are jointly Borel since $uv=((u+v)^{2}-u^{2}-v^{2})/2$.

(i) $c^{2}$ as a plane integral. $\lambda$ is $\sigma$-finite ($\mathbb{R}=\bigcup_L[-L,L]$), so Tonelli and Fubini Theorems applies to $g_2\ge0$: for fixed $y$, $\int g(x)g(y)\,d\lambda(x)=g(y)\,c$ (nonnegative scalars pull out, claim 1 of Linearity and Monotonicity of the Lebesgue Integral), hence

(ii) Layer-cake identity. Let $(W,\mathcal{A},m)$ be a $\sigma$-finite measure space and $h:W\to[0,\infty]$ an $\mathcal{A}$-measurable function. Then

Indeed, by density of the rationals the set $E_h=\{(w,s):0<s<h(w)\}$ satisfies $E_h=\bigcup_{q\in\mathbb{Q},q>0}\bigl(\{h>q\}\times(0,q)\bigr)$, a countable union of measurable rectangles, so $E_h\in\mathcal{A}\otimes\mathcal{B}(\mathbb{R})$ (Product Sigma-Algebra). Applying Tonelli and Fubini Theorems to $\mathbf{1}_{E_h}$ over $m\otimes\lambda$: the $w$-indexed sections are $(E_h)_w=(0,h(w))$ with $\lambda((0,h(w)))=h(w)$ (interval lengths, including the value $\infty$ for $h(w)=\infty$, since $\lambda((0,\infty))=\infty$ by continuity from below), while the $s$-indexed sections are $\{h>s\}$ for $s>0$ and $\emptyset$ otherwise; the two iterated integrals give the two sides.

(iii) Dilations of the plane. For $r>0$ and $E\in\mathcal{B}(\mathbb{R})\otimes\mathcal{B}(\mathbb{R})$, write $rE=\{(rx,ry):(x,y)\in E\}$. The map $S_r(x,y)=(x/r,y/r)$ satisfies $S_r^{-1}(A\times B)=(rA)\times(rB)$, with $rA$ Borel (it is the preimage of $A$ under the continuous map $x\mapsto x/r$), so $S_r$ is measurable and $rE=S_r^{-1}(E)$ is again in the product $\sigma$-algebra. The set function $E\mapsto(\lambda\otimes\lambda)(rE)$ is a measure (preimages preserve disjoint unions) assigning to a rectangle the value $\lambda(rA)\lambda(rB)=r^{2}\lambda(A)\lambda(B)$, by the scaling instance of Preliminary (P2) of the proof of Moments and Stability of the Standard Normal Distribution (interval covers scale by $r$ in the Lebesgue outer measure). The set function $E\mapsto r^{2}(\lambda\otimes\lambda)(E)$ is a measure with the same rectangle values, namely those of the product of the $\sigma$-finite measure $r\lambda$ with itself; by the uniqueness clause of Existence and Uniqueness of the Product Measure both equal $(r\lambda)\otimes(r\lambda)$, so

(iv) Disks. Let $D^{\circ}=\{(x,y):x^{2}+y^{2}<1\}$, which is in the product $\sigma$-algebra since $(x,y)\mapsto x^{2}+y^{2}$ is jointly Borel; similarly $D$ (use $\le$). For $0<s<1$, $sD\subseteq D^{\circ}\subseteq D$, so by monotonicity and (iii), $s^{2}\pi\le(\lambda\otimes\lambda)(D^{\circ})\le\pi$; letting $s\to1$ gives $(\lambda\otimes\lambda)(D^{\circ})=\pi$. Hence for $R>0$, $(\lambda\otimes\lambda)(R\,D^{\circ})=\pi R^{2}$.

(v) Conclusion. For $0<s<1$: $g_2(x,y)>s\iff\exp(-(x^{2}+y^{2})/2)>s\iff-(x^{2}+y^{2})/2>\ln s\iff x^{2}+y^{2}<2\ln(1/s)$, using the inverse relation between $\exp$ and $\ln$ and $-\ln s=\ln(1/s)$; thus $\{g_2>s\}=R_s\,D^{\circ}$ with $R_s=\sqrt{2\ln(1/s)}$ (positive square root), of measure $\pi R_s^{2}=2\pi\ln(1/s)$ by (iv). For $s\ge1$, $\{g_2>s\}=\emptyset$ since $g_2\le1$. By (i) and (ii) applied on $(\mathbb{R}^2,\lambda\otimes\lambda)$ ($\sigma$-finite by Existence and Uniqueness of the Product Measure),

Finally $\int_{(0,1)}\ln(1/s)\,d\lambda(s)=1$: by (ii) applied on $(\mathbb{R},\lambda)$ to $h(s)=\ln(1/s)\mathbf{1}_{(0,1)}(s)$ (measurable: for $u>0$, $\{h>u\}=\{s\in(0,1):1/s>\exp(u)\}=(0,\exp(-u))$, an interval; for $u\le 0$, $\{h>u\}\in\mathcal{B}(\mathbb{R})$ similarly),

and the map $u\mapsto-\exp(-u)$ is an antiderivative of $u\mapsto\exp(-u)$ on every $[0,L]$ (claim 1 of Derivative and Continuity of the Scaled Exponential Function with $c=-1$ gives the derivative $-\exp(-u)$ of $u\mapsto\exp(-u)$, and claim 2 of Sum, Constant Multiple, and Product Rules for One-Dimensional Derivatives multiplies by the constant $-1$), and $F(u)=-\exp(-u)$ is continuous on $[0,L]$, since $u\mapsto\exp(-u)$ is continuous by claim 2 of Derivative and Continuity of the Scaled Exponential Function and $|F(s)-F(t)|=|\exp(-s)-\exp(-t)|$; that same continuity makes $u\mapsto\exp(-u)$ Riemann integrable on $[0,L]$ by Continuous Functions on Compact Intervals are Riemann Integrable, so Fundamental Theorem of Calculus, Part II, on a Closed Real Interval gives $\int_0^L\exp(-u)\,du=F(L)-F(0)=1-\exp(-L)$, and Agreement of the Riemann and Lebesgue Integrals for Continuous Functions on a Closed Interval, applied to the zero extension of $u\mapsto\exp(-u)$ from $[0,L]$, gives $\int\mathbf{1}_{[0,L]}\exp(-u)\,d\lambda=1-\exp(-L)$; by Monotone Convergence Theorem and $\exp(-L)\le1/L\to0$ (from $\exp(L)\ge L$), the integral equals $1$. Hence $c^{2}=2\pi$. $\blacksquare$