4.2. The packing lower bound
For every 0 < c < 1/\pi there exists d_0(c) \in \mathbb{N} such that, for every
d \ge d_0(c) and \varsigma \in \{-1,+1\}, no g \in \mathcal{E}_\varsigma(d)
(Definition 1.2.1) satisfies g(x) \ge 0 for all |x| \ge c\sqrt d.
In words: no nonzero g \in L^1(\mathbb{R}^d;\mathbb{R}) with \widehat g = \varsigma g and
g(0) = 0 is nonnegative outside B(0,c\sqrt d), where g denotes its continuous
Fourier-inversion representative.
Lean code for Proposition4.2.1●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/SignUncertainty/LowerBound.leancomplete
theorem CohnElkies.eventually_not_nonneg_outside_signEigenfunction {c : ℝ} (hc : 0 < c) (hcπ : c < Real.pi⁻¹) : ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (ς : ℤˣ) (g : CohnElkies.SignEigenfunction d ς), ¬∀ (x : CohnElkies.Euclidean d), c * √↑d ≤ ‖x‖ → 0 ≤ g.toFun x
theorem CohnElkies.eventually_not_nonneg_outside_signEigenfunction {c : ℝ} (hc : 0 < c) (hcπ : c < Real.pi⁻¹) : ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (ς : ℤˣ) (g : CohnElkies.SignEigenfunction d ς), ¬∀ (x : CohnElkies.Euclidean d), c * √↑d ≤ ‖x‖ → 0 ≤ g.toFun x
Proposition 3.7 of the report, `L¹` case: for `0 < c < 1/π`, in all sufficiently large dimensions `d` no sign eigenfunction `g` (`0 ≠ g ∈ L¹(ℝ^d;ℝ)`, `𝓕 g = ς g`, `g(0) = 0`; report (6)) is nonnegative outside the ball of radius `c √d`. The proof follows the module docstring: radial reduction, Schwartz approximation, the negative-mass estimate for each `q_n`, and `n → ∞`.
Schwartz case. Suppose first that g is a radial Schwartz eigenfunction. Since
\int g = \widehat g(0) = \varsigma g(0) = 0, its negative part g_- = \max\{-g,0\} has
integral \|g\|_1/2. If g \ge 0 for |x| \ge c\sqrt d, then g_- vanishes outside
B(0,c\sqrt d), so
\|g\|_1/2 = \int g_- \le \int_{|x|<c\sqrt d}|g| \le C_ce^{-\gamma_c d}\|g\|_1
by Proposition 4.1.35, which is impossible once C_ce^{-\gamma_c d} < 1/2.
General case. Let g \in \mathcal{E}_\varsigma(d) be nonnegative outside B(0,R),
R = c\sqrt d. By Lemma 3.2.8 and
Lemma 3.2.6, h = \mathcal{R}g is a nonzero radial element of
\mathcal{E}_\varsigma(d) with the same eigenvalue, origin value and exterior sign. Let h_n
be the radial Schwartz eigenfunctions of Lemma 3.2.18, so
\widehat{h_n} = \varsigma h_n, h_n(0) = 0, h_n \to h in L^1. They need not be
nonnegative outside the ball, but there (h_n)_- \le |h_n - h| because h \ge 0; hence
\tfrac12\|h_n\|_1 = \int(h_n)_- \le \int_{|x|<R}|h_n| + \|h_n - h\|_1, which is at most
C_ce^{-\gamma_c d}\|h_n\|_1 + \|h_n - h\|_1 by Proposition 4.1.35. Letting n \to \infty
gives \|h\|_1/2 \le C_ce^{-\gamma_c d}\|h\|_1, contradicting h \ne 0 for all sufficiently
large d.
There is a sequence \epsilon_d \to 0, \epsilon_d \ge 0, such that for every d \ge 1 and
every F \in \mathcal{A}_d (Definition 1.1.4), (equation (28))
\dfrac{F(0)}{\widehat F(0)}
\ge \dfrac{2^d}{v_d}\Bigl(\sqrt{\dfrac{e}{2\pi}} - \epsilon_d\Bigr)^d,
with v_d from Definition 1.1.3.
Lean code for Theorem4.2.2●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/Asymptotics/Manuscript.leancomplete
theorem CohnElkies.exists_manuscriptUniversalPackingIsLittleO : ∃ δ, (δ =o[Filter.atTop] fun x ↦ 1) ∧ (∀ (d : ℕ), 0 ≤ δ d) ∧ ∀ (d : ℕ), 0 < d → ∀ (f : CohnElkies.Admissible d), 2 ^ d / CohnElkies.unitBallVolume d * (CohnElkies.criticalPackingBase - δ d) ^ d ≤ CohnElkies.quotient f
theorem CohnElkies.exists_manuscriptUniversalPackingIsLittleO : ∃ δ, (δ =o[Filter.atTop] fun x ↦ 1) ∧ (∀ (d : ℕ), 0 ≤ δ d) ∧ ∀ (d : ℕ), 0 < d → ∀ (f : CohnElkies.Admissible d), 2 ^ d / CohnElkies.unitBallVolume d * (CohnElkies.criticalPackingBase - δ d) ^ d ≤ CohnElkies.quotient f
By Lemma 3.2.7 we may replace F by its rotational average,
which preserves F(0), \widehat F(0) and admissibility; so assume F radial. Both
\widehat F(0) > 0 and F(0) > 0 (Lemma 1.1.5), so
a = (\widehat F(0)/F(0))^{1/d} > 0 is defined (CohnElkies.balancingScale). Put h(x) = F(ax)
(CohnElkies.balanced) and g = \widehat h - h (CohnElkies.antiFourierPart). Fourier scaling
(Definition 1.1.2) and admissibility give (29)–(30):
\widehat h(\xi) = a^{-d}\widehat F(\xi/a), h(0) = \widehat h(0) = F(0), \widehat g = -g
(as h is even, \widehat{\widehat h} = h), g(0) = 0, and
g(x) = a^{-d}\widehat F(x/a) - F(ax) \ge 0 for |x| \ge 1/a. Moreover g \ne 0: otherwise
h = \widehat h \ge 0 while h(x) = F(ax) \le 0 for |x| \ge 1/a, so h would vanish outside
a ball and be self-Fourier, hence h = 0 by
Lemma 3.2.12, contradicting h(0) = F(0) > 0
(CohnElkies.antiFourierPart_balanced_ne_zero). Thus g is a nonzero real radial Schwartz
anti-self-Fourier function with g(0) = 0, nonnegative outside B(0,1/a). Fix
0 < c < 1/\pi. If 1/a \le c\sqrt d then g \ge 0 outside B(0,c\sqrt d), which
Proposition 4.2.1 forbids for d \ge d_0(c). Hence
(F(0)/\widehat F(0))^{1/d} = 1/a > c\sqrt d
uniformly in F, so
\liminf_{d\to\infty}\frac{1}{\sqrt d}\inf_{F\in\mathcal{A}_d}(F(0)/\widehat F(0))^{1/d} \ge c for
every c < 1/\pi. Taking the supremum over c (a diagonal choice c_d \uparrow 1/\pi) yields
(31): \inf_{F\in\mathcal{A}_d}(F(0)/\widehat F(0))^{1/d} \ge (1/\pi - o(1))\sqrt d with the
o(1) independent of F. Combining (31) with v_d^{1/d} = (1+o(1))\sqrt{2\pi e/d} from
Lemma 3.1.8, and \sqrt{2\pi e}/(2\pi) = \sqrt{e/(2\pi)}, gives (28)
for a sequence \epsilon_d \to 0 independent of F.