The Cohn–Elkies exponent and sign uncertainty

7.13. Schwartz approximation with a bump mollifier🔗

The report approximates a radial L^1 eigenfunction g by q_n = \eta_n\,(g * \kappa_n) with the Gaussians \kappa_n(x) = n^de^{-\pi n^2|x|^2}, \eta_n(x) = e^{-\pi|x|^2/n^2} (Definition 3.2.14). The formalization convolves with a compactly supported normalized flat bump instead, which makes the smoothness and the Schwartz decay of the approximant elementary, and keeps the Gaussians only on the Fourier side.

Lemma7.13.1
Statement uses 2
Statement dependency previews
Preview
Lemma 3.2.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Let \varphi be a smooth nonnegative radial function with compact support and \int\varphi = 1, \varphi_n(x) = n^d\varphi(nx), and let g \in L^1_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) be continuous with \widehat g = \varsigma g. Then q_n = (\eta_n g) * \varphi_n is a real radial Schwartz function with \widehat{q_n} = \varsigma\,(g * \kappa_n)\,\widehat{\varphi_n}, and q_n \to g, \widehat{q_n} \to \varsigma g in L^1 (Lemma 3.2.15). Moreover, for a bump \varphi as above, one of \varphi + \varsigma\widehat\varphi and \varphi(2\cdot) + \varsigma\widehat{\varphi(2\cdot)} is a real radial Schwartz function \psi_\varsigma with \widehat{\psi_\varsigma} = \varsigma\psi_\varsigma and \psi_\varsigma(0) \ne 0 (Lemma 3.2.17), the corrector of Lemma 3.2.18, in place of the Gaussian and Hermite functions \psi_\pm of the report.

Lean code for Lemma7.13.1●3 declarations
  • defdefined in CohnElkies/SignUncertainty/Mollifiers.lean
    complete
    def CohnElkies.bumpKernel {d : ℕ} (n : ℕ) : CohnElkies.TestFunction d
    def CohnElkies.bumpKernel {d : ℕ} (n : ℕ) :
  CohnElkies.TestFunction d
    `φ_n(x) = (n+1)^d φ((n+1) x)`, the bump mollifier, as a test function.
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.fourier_approximant_apply {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) (n : ℕ)
  (ξ : CohnElkies.Euclidean d) :
  (FourierTransform.fourier (CohnElkies.approximant h n)) ξ =
    ↑↑ς *
      (CohnElkies.gaussianSmoothing h n ξ *
        (FourierTransform.fourier (CohnElkies.bumpKernel n)) ξ)
    theorem CohnElkies.fourier_approximant_apply
  {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun)
  (n : ℕ) (ξ : CohnElkies.Euclidean d) :
  (FourierTransform.fourier
        (CohnElkies.approximant h n))
      ξ =
    ↑↑ς *
      (CohnElkies.gaussianSmoothing h n
          ξ *
        (FourierTransform.fourier
            (CohnElkies.bumpKernel n))
          ξ)
    `𝓕 q_n = ς (h ⋆ κ_n) 𝓕 φ_n` (report §2.1).
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.exists_eigenTest {d : ℕ} (hd : 0 < d) (ς : ℤˣ) :
  ∃ ψ,
    CohnElkies.IsRealValued ⇑ψ ∧
      CohnElkies.IsRadial ⇑ψ ∧
        FourierTransform.fourier ψ = ↑↑ς • ψ ∧ ψ 0 ≠ 0
    theorem CohnElkies.exists_eigenTest {d : ℕ}
  (hd : 0 < d) (ς : ℤˣ) :
  ∃ ψ,
    CohnElkies.IsRealValued ⇑ψ ∧
      CohnElkies.IsRadial ⇑ψ ∧
        FourierTransform.fourier ψ =
            ↑↑ς • ψ ∧
          ψ 0 ≠ 0
    A real radial test function `ψ` with `𝓕 ψ = ς ψ` and `ψ(0) ≠ 0` (the corrector `ψ_ς` of
report §2.1): `P_ς(bump)` or `P_ς(bump(2·))`, at least one of which does not vanish at `0`
since `𝓕 bump (0) = ∫ bump > 0` and `2^{-d} ≠ 1`.
Proof for Lemma 7.13.1
Proof uses 3
Proof dependency previews
Preview
Definition 1.1.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Convolution with a compactly supported smooth function of an integrable function is smooth with all derivatives bounded; multiplied by the Gaussian factor inside \eta_n g the result is a Schwartz function (Definition 3.2.14). The Fourier identity is the convolution theorem \widehat{u * v} = \widehat u\,\widehat v together with \widehat{\eta_n g} = \kappa_n * \widehat g = \varsigma\,(\kappa_n * g) (Definition 1.1.2). Convergence: (\varphi_n) and (\kappa_n) are approximate identities and \eta_n \to 1 boundedly, so both q_n \to g and \widehat{q_n} \to \varsigma g in L^1 by continuity of translation in L^1 and dominated convergence. The remaining steps are those of Lemma 3.2.18.