7.12. Existence of extremizers: deviations from Cohn–Gonçalves🔗

The existence part of Theorem 1.4 of Cohn–Gonçalves (2019) is proved along the lines of their §3.2, with three changes.

• Uniform negative-mass bound. Cohn–Gonçalves obtain \int_{B_{r(f_n)}} f_n \le K < 0 for the normalized minimizing sequence from Nazarov's uncertainty principle in Jaming's higher-dimensional form (alternatively from the Amrein–Berthier inequality), a quantitative statement with explicit constants. The formalization uses the qualitative lemma Lemma 6.2.10: L^1-normalized eigenfunctions of the Fourier transform have L^1 mass at least \kappa(c,R) > 0 outside any fixed ball, proved by contradiction from weak L^2 compactness (Lemma 6.2.9) and the compact-support theorem (Lemma 3.2.12).

• No Mazur's lemma. Cohn–Gonçalves upgrade the weak L^2 convergence of the minimizing sequence to convergence almost everywhere and in L^2 (Mazur's lemma, using the convexity of the class) and then apply Fatou's lemma. The formalization keeps the weak limit and reads off its properties by testing against explicit L^2 functions (indicators, 1_K\operatorname{sign} g) and smooth compactly supported functions (for the Fourier eigen-equation, through \int\widehat u\,\Phi = \int u\,\widehat\Phi).

• Origin correction. Cohn–Gonçalves normalize the minimizing sequence with their Lemma 3.1 (\widehat{f_n} = -f_n, f_n(0) = 0) and deduce f(0) = 0 for the limit from minimality. In the report's class \mathcal{E}_-(d) both conditions are part of the definition, and the origin correction (Lemma 6.2.5) is applied once, to the continuous representative of the weak limit, which a priori only satisfies f(0) \ge 0.

The infinitely-many-roots part of Theorem 1.4 is not formalized.