The Fourier transform of e^{-b\pi|x|^2} is b^{-d/2}e^{-\pi|\xi|^2/b}, which gives the formula; taking logarithms, t^{-d/2}e^{-\pi|\xi|^2/t} < (2t)^{-d/2}e^{-\pi|\xi|^2/(2t)} if and only if \pi|\xi|^2/(2t) > (d/2)\log 2, i.e. |\xi|^2 > t\,d\log 2/\pi. Applying the transform formula twice gives \widehat{\widehat{\varphi_t}} = \varphi_t.

Immediate from Lemma 6.2.3: \widehat{\psi_t} = \widehat{\varphi_t} - \varphi_t = -\psi_t, \psi_t(0) = 0 - 1, and \psi_t = \varphi_t - \widehat{\varphi_t} > 0 where \widehat{\varphi_t} < 0.

By Lemma 6.2.4, \widehat h = -g + g(0)(-\psi_t) = -h, h(0) = g(0) + g(0)\psi_t(0) = 0, and for |x| \ge R one has |x|^2 \ge t\,d\log 2/\pi, so \psi_t(x) \ge 0 and h(x) \ge g(x) \ge 0. If g(0) > 0 then h(x) > g(x) \ge 0 for |x| > R, so h \ne 0; if g(0) = 0 then h = g \ne 0.

(Cohn–Gonçalves 2019, §3.1.) If g \in \mathcal{E}_\varsigma(d) with \|g\|_1 = 1 is nonnegative outside B_\rho, then \int g = \widehat g(0) = \varsigma g(0) = 0 gives \int g_- = \tfrac12, while g_- \le |g| \le \|\widehat g\|_1 = 1 vanishes outside B_\rho, so \tfrac12 \le \operatorname{vol}(B_\rho); choosing \rho with \operatorname{vol}(B_\rho) < \tfrac12 shows \mathsf{A}_\varsigma(d) \ge \rho > 0.

G satisfies \widehat G = -G and G(0) = -1 - (-1) = 0 (Lemma 6.2.4). Writing E_b(x) = e^{-\pi b|x|^2}, D = 2^d - 2^{d/2}, D' = 2^{d/2} - 1, \psi_{1/4} = (E_{1/4} - E_{1/2} - 2^dE_4 + 2^{d/2}E_2)/D and \psi_{1/2} = (E_{1/2} - 2^{d/2}E_2)/D', so that G \ge E_{1/4}\bigl(1 - e^{-\pi|x|^2/4}(1 + D/D' + 2^d)\bigr)/D > 0 once |x|^2 > (4/\pi)\log(1 + D/D' + 2^d); hence G \ne 0 and G \in \mathcal{E}_-(d).

\mathsf{A}_-(d) \le r(G) < \infty for the explicit G of Lemma 6.2.7.

By the Fréchet–Riesz theorem the functionals \langle x_n, \cdot\rangle lie in a closed ball of the dual E^*, which is weak-star sequentially compact for separable E (sequential Banach–Alaoglu, Mathlib's WeakDual.isSeqCompact_closedBall); transporting the limit functional back along the Riesz isometry gives y.

Suppose not: there are such f_n with \delta_n = \int_{B^c}|f_n| \to 0, B the closed ball of radius R. Each f_n = c^{-1}\widehat{f_n} is continuous with |f_n| \le |c|^{-1}. The truncations 1_Bf_n are bounded in L^2, so by Lemma 6.2.9 a subsequence converges weakly to some g \in L^2; testing against the kernels 1_B(x)e^{2\pi i\langle x,\xi\rangle} shows \widehat{1_Bf_n}(\xi) \to \widehat{1_Bg}(\xi) for every \xi, and |\widehat{f_n} - \widehat{1_Bf_n}| \le \delta_n, so f_n \to G := c^{-1}\widehat{1_Bg} pointwise, with G continuous. Bounded convergence on B gives \int_B|G| = \lim(1 - \delta_n) = 1; Fatou on B^c gives G = 0 a.e., hence everywhere, off B; and bounded convergence on B again gives \widehat G(\xi) = \lim\int_B e^{-2\pi i\langle x,\xi\rangle}f_n = \lim(\widehat{f_n}(\xi) + O(\delta_n)) = cG(\xi). Thus G and \widehat G are compactly supported and G \ne 0, contradicting Lemma 3.2.12.

By Lemma 6.2.6 and Lemma 6.2.8, 0 < a := \mathsf{A}_-(d) < \infty. Pick f_n \in \mathcal{E}_-(d) with r(f_n) \le a + 1/(n+1), normalized so that \|f_n\|_1 = 1; then |f_n| = |\widehat{f_n}| \le 1, \int f_n = 0, and f_n \ge 0 on \{|x| \ge a + 1/(n+1)\}. By Lemma 6.2.10 with R = a + 1 there is \kappa > 0 with \int_{|x| \le a+1} f_n = -\int_{|x| > a+1} f_n \le -\kappa for all n. Since \|f_n\|_2^2 \le \|f_n\|_\infty\|f_n\|_1 \le 1, Lemma 6.2.9 gives a subsequence converging weakly in L^2 to some g. Testing the weak convergence against bounded compactly supported functions shows: g \in L^1 with \int_K|g| \le 1 for every compact K (test with 1_K\operatorname{sign} g); \int_{|x| \le a+1} g \le -\kappa, so g \ne 0; \int_K g \le 0 for all balls K \supseteq B_{a+1}, hence \int g \le 0; and g \ge 0 a.e. on \{|x| > a\} (test with indicators of \{a + 1/(m+1) \le |x| \le m+1\} \cap \{g < 0\}). Testing against Schwartz functions \Phi and using \int\widehat u\,\Phi = \int u\,\widehat\Phi for u \in L^1 yields \int(\widehat g + g)\Phi = 0 for all smooth compactly supported \Phi, so \widehat g = -g a.e. The continuous function G = -\widehat g therefore satisfies G = g a.e., \widehat G = -G pointwise, G \ne 0, G(0) = -\int g \ge 0, and G \ge 0 on \{|x| \ge a\} (a.e. on the open exterior, hence everywhere by continuity). Finally Lemma 6.2.5 with R = a produces h \in \mathcal{E}_-(d) with r(h) \le a, and r(h) \ge \mathsf{A}_-(d) = a by definition of the infimum.

This differs from the proof of Cohn–Gonçalves in three places: their uniform negative-mass bound \int_{B} f_n \le K < 0 is deduced from Nazarov's uncertainty principle in Jaming's form (or from the Amrein–Berthier inequality), here from the compactness lemma Lemma 6.2.10; they pass from weak to almost-everywhere and L^2 convergence by Mazur's lemma before applying Fatou's lemma, whereas here the weak limit is only tested against explicit L^2 and smooth compactly supported functions; and they normalize the minimizing sequence by their Lemma 3.1 and infer f(0) = 0 for the limit from minimality, whereas here every element of \mathcal{E}_-(d) already has \widehat g = -g and g(0) = 0, and the origin correction is applied once, to the limit.