The Cohn–Elkies exponent and sign uncertainty

5. The admissible primal upper bound🔗

The previous chapter established \min\{\inf_{F\in\mathcal{A}_d}(F(0)/\widehat F(0))^{1/d},\ \mathsf{A}_-(d),\ \mathsf{A}_+(d)\} \ge (1/\pi - o(1))\sqrt d. We now explain how the upper bounds in the introduction reduce to constructing functions whose sign changes occur at the same radius. Throughout, \ll denotes an inequality up to an absolute constant, \ll_\epsilon up to a constant depending only on \epsilon, and \asymp means both \ll and \gg. The chapter corresponds to the modules CohnElkies/UpperBound/*.lean; the construction is generic in the polynomial factor (CohnElkies.IsSaddlePolynomial, CohnElkies.mellinProfile), the Fourier pair (f_-, f_+) being the case P = P_\pm and the self-Fourier function f_0 the case P = P_0 (module CohnElkies.UpperBound.SelfFourier, CohnElkies.fZero, CohnElkies.PZero).

Lemma5.1
Statement uses 3
Statement dependency previews
Preview
Definition 1.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let R > 0 and let f_-, f_+ be real radial Schwartz functions on \mathbb{R}^d with \widehat{f_-} = f_+ \ge 0 everywhere, f_-(0) = f_+(0) > 0, and f_-(x) \le 0 for |x| \ge R. Then F(x) = f_-(Rx) belongs to \mathcal{A}_d^{\mathrm{rad}} (Definition 1.1.4, Definition 3.2.2) with F(0)/\widehat F(0) = R^d, so \mathrm{LP}_d \le v_d(R/2)^d (Definition 1.1.6).

Lean code for Lemma5.1●2 declarations
  • defdefined in CohnElkies/UpperBound/FourierPair.lean
    complete
    def CohnElkies.saddleSourceAdmissible {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε) {R : ℝ}
  (hR : 0 < R) (fminus fplus : CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x = CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d), fplus x = CohnElkies.fPlusFun ε d x)
  (hplusnonneg :
    ∀ (x : CohnElkies.Euclidean d), 0 ≤ (CohnElkies.fPlusFun ε d x).re)
  (hminusoutside :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → (CohnElkies.fMinusFun ε d x).re ≤ 0) :
  CohnElkies.RadialAdmissible d
    def CohnElkies.saddleSourceAdmissible {ε : ℝ}
  (hε : 0 < ε) {d : ℕ} (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  {R : ℝ} (hR : 0 < R)
  (fminus fplus :
    CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x =
        CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d),
      fplus x = CohnElkies.fPlusFun ε d x)
  (hplusnonneg :
    ∀ (x : CohnElkies.Euclidean d),
      0 ≤ (CohnElkies.fPlusFun ε d x).re)
  (hminusoutside :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ →
        (CohnElkies.fMinusFun ε d x).re ≤
          0) :
  CohnElkies.RadialAdmissible d
    The radial admissible function `x ↦ f₋(Rx)` built from the saddle pair `(f₋, f₊)`.
  • theoremdefined in CohnElkies/UpperBound/FourierPair.lean
    complete
    theorem CohnElkies.saddleSourceAdmissible_normalizedCost {ε : ℝ} (hε : 0 < ε)
  {d : ℕ} (hd : 0 < d) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  {R : ℝ} (hR : 0 < R) (fminus fplus : CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x = CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d), fplus x = CohnElkies.fPlusFun ε d x)
  (hplusnonneg :
    ∀ (x : CohnElkies.Euclidean d), 0 ≤ (CohnElkies.fPlusFun ε d x).re)
  (hminusoutside :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → (CohnElkies.fMinusFun ε d x).re ≤ 0) :
  CohnElkies.normalizedCost
      (CohnElkies.saddleSourceAdmissible hε hd horder hR fminus fplus
          hminus hplus hplusnonneg hminusoutside).toAdmissible =
    R / √↑d
    theorem CohnElkies.saddleSourceAdmissible_normalizedCost
  {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  {R : ℝ} (hR : 0 < R)
  (fminus fplus :
    CohnElkies.TestFunction d)
  (hminus :
    ∀ (x : CohnElkies.Euclidean d),
      fminus x =
        CohnElkies.fMinusFun ε d x)
  (hplus :
    ∀ (x : CohnElkies.Euclidean d),
      fplus x = CohnElkies.fPlusFun ε d x)
  (hplusnonneg :
    ∀ (x : CohnElkies.Euclidean d),
      0 ≤ (CohnElkies.fPlusFun ε d x).re)
  (hminusoutside :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ →
        (CohnElkies.fMinusFun ε d x).re ≤
          0) :
  CohnElkies.normalizedCost
      (CohnElkies.saddleSourceAdmissible
          hε hd horder hR fminus fplus
          hminus hplus hplusnonneg
          hminusoutside).toAdmissible =
    R / √↑d
    Report (31): the normalized cost of the saddle source is `R/√d`.
Proof for Lemma 5.1
uses 1

Fourier scaling (Definition 1.1.2) gives \widehat F(\xi) = R^{-d}f_+(\xi/R) \ge 0, F(x) = f_-(Rx) \le 0 for |x| \ge 1, and F(0)/\widehat F(0) = R^df_-(0)/f_+(0) = R^d.

Lemma5.2
Statement uses 4
Statement dependency previews
Preview
Definition 1.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

If g is a real radial Schwartz function with \widehat g = \varsigma g, g(0) = 0, g \ne 0 and g(x) \ge 0 for |x| \ge R, then g \in \mathcal{E}_\varsigma(d) with r(g) \le R, so \mathsf{A}_\varsigma(d) \le R (see Definition 1.2.1, Definition 1.2.2, Definition 1.2.3). This applies to g_- = f_+ - f_- for a pair f_\pm as in Lemma 5.1 with f_+ > 0 on \{|x| \ge R\}, and to a self-Fourier f_0 with f_0(0) = 0 and f_0 > 0 on \{|x| \ge R\}.

Lean code for Lemma5.2●3 declarations
  • theoremdefined in CohnElkies/SignUncertainty/UpperBound.lean
    complete
    theorem CohnElkies.RadialEigenfunction.signUncertaintyConstant_le_of_nonneg_outside
  {d : ℕ} {ς : ℤˣ} (g : CohnElkies.RadialEigenfunction d ς) {R : ℝ}
  (hR : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ (g.toFun x).re) :
  CohnElkies.signUncertaintyConstant ς d ≤ ENNReal.ofReal R
    theorem CohnElkies.RadialEigenfunction.signUncertaintyConstant_le_of_nonneg_outside
  {d : ℕ} {ς : ℤˣ}
  (g : CohnElkies.RadialEigenfunction d ς)
  {R : ℝ}
  (hR :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ (g.toFun x).re) :
  CohnElkies.signUncertaintyConstant ς d ≤
    ENNReal.ofReal R
    `A_ς(d) ≤ R` as soon as some real radial Schwartz eigenfunction with eigenvalue `ς` is
nonnegative outside the ball of radius `R` (report (6)).
  • defdefined in CohnElkies/SignUncertainty/UpperBound.lean
    complete
    def CohnElkies.minusSaddleEigenfunction {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  (hne :
    CohnElkies.plusSaddleSchwartz hε hd horder -
        CohnElkies.minusSaddleSchwartz hε hd horder ≠
      0) :
  CohnElkies.RadialEigenfunction d (-1)
    def CohnElkies.minusSaddleEigenfunction
  {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  (hne :
    CohnElkies.plusSaddleSchwartz hε hd
          horder -
        CohnElkies.minusSaddleSchwartz hε
          hd horder ≠
      0) :
  CohnElkies.RadialEigenfunction d (-1)
    Report, proof of Theorem 1.2: `g_{ε,d,-} = f₊ - f₋` is a real radial test function with
`𝓕 g = -g` (by (40) and Fourier inversion) and `g(0) = f₊(0) - f₋(0) = 0` (by (83)); it is a
radial eigenfunction with eigenvalue `-1` once it is known to be nonzero.
  • defdefined in CohnElkies/UpperBound/SelfFourier.lean
    complete
    def CohnElkies.zeroSaddleEigenfunction {ε : ℝ} (hε : 0 < ε) {d : ℕ}
  (hd : 0 < d) (horder : CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  (hne : CohnElkies.zeroSaddleSchwartz hε hd horder ≠ 0) :
  CohnElkies.RadialEigenfunction d 1
    def CohnElkies.zeroSaddleEigenfunction {ε : ℝ}
  (hε : 0 < ε) {d : ℕ} (hd : 0 < d)
  (horder :
    CohnElkies.a₀ε ε ≤ CohnElkies.Aε ε)
  (hne :
    CohnElkies.zeroSaddleSchwartz hε hd
        horder ≠
      0) :
  CohnElkies.RadialEigenfunction d 1
    `f₀` as a real radial self-Fourier eigenfunction (`𝓕 g = g`, `g(0) = 0`), once it is known to
be nonzero.
Proof for Lemma 5.2
uses 0

Schwartz functions are continuous and integrable, so g lies in \mathcal{E}_\varsigma(d) and the infimum gives the bound. For g_- = f_+ - f_-: since f_- is even, \widehat{f_+} = \widehat{\widehat{f_-}} = f_-, so \widehat{g_-} = f_- - f_+ = -g_-; g_-(0) = 0; g_-(x) = f_+(x) - f_-(x) > 0 for |x| \ge R, so g_- \ne 0 and r(g_-) \le R.

Thus all the upper bounds reduce to producing one Fourier pair, one self-Fourier function, and a radius R = (1/\pi + o(1))\sqrt d.

Theorem5.3
Statement uses 2
Statement dependency previews
Preview
Lemma 5.5.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.5.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

There is \epsilon_0 > 0 such that, for every fixed 0 < \epsilon < \epsilon_0 and every sufficiently large dimension d, there exist real radial Schwartz functions f_-, f_+, f_0 on \mathbb{R}^d and a radius R_{\epsilon,d} > 0 such that f_+ \ge 0 everywhere, f_-(x) \le 0 < f_0(x) whenever |x| \ge R_{\epsilon,d}, and \widehat{f_-} = f_+, \widehat{f_0} = f_0, f_-(0) = f_+(0) > 0, f_0(0) = 0. Moreover R_{\epsilon,d}/\sqrt d \to \alpha_\epsilon as d \to \infty for each fixed \epsilon, and \alpha_\epsilon \to 1/\pi as \epsilon \downarrow 0 (Lemma 5.5.4, Lemma 5.5.5).

Lean code for Theorem5.3●2 theorems
  • theoremdefined in CohnElkies/UpperBound/Signs.lean
    complete
    theorem CohnElkies.saddleSourceEventualSigns :
  CohnElkies.SaddleSourceEventualSigns
    theorem CohnElkies.saddleSourceEventualSigns :
  CohnElkies.SaddleSourceEventualSigns
    Report §4: for small `ε` and large `d` the pair `f_ε^±` has the Cohn–Elkies sign pattern.
  • theoremdefined in CohnElkies/UpperBound/SelfFourier.lean
    complete
    theorem CohnElkies.eventually_exists_radialEigenfunction_fZero :
  ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
    ∀ᶠ (d : ℕ) in Filter.atTop,
      ∃ g,
        (∀ (x : CohnElkies.Euclidean d),
            g.toFun x = CohnElkies.fZeroFun ε d x) ∧
          ∀ (x : CohnElkies.Euclidean d),
            CohnElkies.R_ε ε d ≤ ‖x‖ → 0 < (g.toFun x).re
    theorem CohnElkies.eventually_exists_radialEigenfunction_fZero :
  ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),
    ∀ᶠ (d : ℕ) in Filter.atTop,
      ∃ g,
        (∀ (x : CohnElkies.Euclidean d),
            g.toFun x =
              CohnElkies.fZeroFun ε d x) ∧
          ∀ (x : CohnElkies.Euclidean d),
            CohnElkies.R_ε ε d ≤ ‖x‖ →
              0 < (g.toFun x).re
    Report §4 for `P₀`, packaged: for small `ε` and large `d` the function `f₀` is realized by a
real radial self-Fourier eigenfunction `g` (`𝓕 g = g`, `g(0) = 0`, `g ≠ 0`) which is positive
outside the ball of radius `R_{ε,d}`.
  1. 5.1. Outline of the construction
  2. 5.2. The Mellin ansatz
  3. 5.3. Saddle geometry
  4. 5.4. Global saddle asymptotics
  5. 5.5. Positivity and the sharp upper bound