The Cohn–Elkies exponent and sign uncertainty

3.2. Radial reduction🔗

Rotational averaging, the compact-support obstruction, and Schwartz approximation of integrable radial eigenfunctions (Section 2.1 of the report).

Definition3.2.1
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 4
Reverse dependency previews
Preview
Lemma 3.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

With normalized Haar measure on the orthogonal group O(d), the rotational average of a function f on \mathbb{R}^d is \mathcal{R}f(x) = \int_{O(d)} f(Ux)\,dU.

Lean code for Definition3.2.1●1 definition
  • defdefined in CohnElkies/Radialization.lean
    complete
    def CohnElkies.rotationalAverage.{u_1} {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (g : CohnElkies.Euclidean d → E) (x : CohnElkies.Euclidean d) : E
    def CohnElkies.rotationalAverage.{u_1} {d : ℕ}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  (g : CohnElkies.Euclidean d → E)
  (x : CohnElkies.Euclidean d) : E
    The rotational average `ℛg(x) = ∫_{O(d)} g(Ux) dU` of a function on `ℝ^d` (report §2.1),
with respect to the Haar probability measure of `O(d)`.
Definition3.2.2
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A function on \mathbb{R}^d is radial if it depends only on |x|. Write \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) for the real radial Schwartz functions, L^1_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) for the radial real integrable functions, and \mathcal{A}_d^{\mathrm{rad}} = \mathcal{A}_d \cap \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) for the radial admissible class (see Definition 1.1.4).

Lean code for Definition3.2.2●2 definitions
  • defdefined in CohnElkies/Basic.lean
    complete
    def CohnElkies.IsRadial.{u_1} {d : ℕ} {E : Type u_1}
  (f : CohnElkies.Euclidean d → E) : Prop
    def CohnElkies.IsRadial.{u_1} {d : ℕ}
  {E : Type u_1}
  (f : CohnElkies.Euclidean d → E) : Prop
    A function on `ℝ^d` is radial if it only depends on the norm of its argument.
  • structure(extends 1, 7 fields)defined in CohnElkies/Basic.lean
    complete
    structure CohnElkies.RadialAdmissible (d : ℕ) : Type
    structure CohnElkies.RadialAdmissible (d : ℕ) : Type
    The radial admissible class `𝒜_d^rad = 𝒜_d ∩ 𝒮_rad(ℝ^d; ℝ)` of the report, §2.1: admissible
functions depending only on the norm of their argument.

    Extends

    • PackingBounds.FullAdmissible d

    Fields

    function : CohnElkies.TestFunction d
    Inherited from
    1. PackingBounds.FullAdmissible
    real : ∀ (x : CohnElkies.Euclidean d), (self.function x).im = 0
    Inherited from
    1. PackingBounds.FullAdmissible
    fourier_real : ∀ (x : CohnElkies.Euclidean d), ((FourierTransform.fourier self.function) x).im = 0
    Inherited from
    1. PackingBounds.FullAdmissible
    fourier_nonneg : ∀ (x : CohnElkies.Euclidean d), 0 ≤ ((FourierTransform.fourier self.function) x).re
    Inherited from
    1. PackingBounds.FullAdmissible
    fourier_zero_pos : 0 < ((FourierTransform.fourier self.function) 0).re
    Inherited from
    1. PackingBounds.FullAdmissible
    outside_nonpos : ∀ (x : CohnElkies.Euclidean d), 1 ≤ ‖x‖ → (self.function x).re ≤ 0
    Inherited from
    1. PackingBounds.FullAdmissible
    radial : CohnElkies.IsRadial ⇑self.function
    The function is radial.
Lemma3.2.3
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let f be continuous and integrable on \mathbb{R}^d. Then \mathcal{R}f (Definition 3.2.1) is continuous, integrable and radial (Definition 3.2.2), with \|\mathcal{R}f\|_1 \le \|f\|_1 and (\mathcal{R}f)(0) = f(0); if f is real, so is \mathcal{R}f.

Lean code for Lemma3.2.3●6 theorems
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.continuous_rotationalAverage.{u_1} {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E]
  {g : CohnElkies.Euclidean d → E} (hg : Continuous g) :
  Continuous (CohnElkies.rotationalAverage g)
    theorem CohnElkies.continuous_rotationalAverage.{u_1}
  {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [SecondCountableTopology E]
  {g : CohnElkies.Euclidean d → E}
  (hg : Continuous g) :
  Continuous
    (CohnElkies.rotationalAverage g)
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.integrable_rotationalAverage.{u_1} {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E]
  {g : CohnElkies.Euclidean d → E} (hg : Continuous g)
  (hi : MeasureTheory.Integrable g MeasureTheory.volume) :
  MeasureTheory.Integrable (CohnElkies.rotationalAverage g)
    MeasureTheory.volume
    theorem CohnElkies.integrable_rotationalAverage.{u_1}
  {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [SecondCountableTopology E]
  {g : CohnElkies.Euclidean d → E}
  (hg : Continuous g)
  (hi :
    MeasureTheory.Integrable g
      MeasureTheory.volume) :
  MeasureTheory.Integrable
    (CohnElkies.rotationalAverage g)
    MeasureTheory.volume
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.rotationalAverage_eq_of_norm_eq.{u_1} {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (g : CohnElkies.Euclidean d → E) :
  CohnElkies.IsRadial (CohnElkies.rotationalAverage g)
    theorem CohnElkies.rotationalAverage_eq_of_norm_eq.{u_1}
  {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (g : CohnElkies.Euclidean d → E) :
  CohnElkies.IsRadial
    (CohnElkies.rotationalAverage g)
    The rotational average is radial.
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.integral_norm_rotationalAverage_le.{u_1} {d : ℕ}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [SecondCountableTopology E] {g : CohnElkies.Euclidean d → E}
  (hg : Continuous g)
  (hi : MeasureTheory.Integrable g MeasureTheory.volume) :
  ∫ (x : CohnElkies.Euclidean d), ‖CohnElkies.rotationalAverage g x‖ ≤
    ∫ (x : CohnElkies.Euclidean d), ‖g x‖
    theorem CohnElkies.integral_norm_rotationalAverage_le.{u_1}
  {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [SecondCountableTopology E]
  {g : CohnElkies.Euclidean d → E}
  (hg : Continuous g)
  (hi :
    MeasureTheory.Integrable g
      MeasureTheory.volume) :
  ∫ (x : CohnElkies.Euclidean d),
      ‖CohnElkies.rotationalAverage g x‖ ≤
    ∫ (x : CohnElkies.Euclidean d), ‖g x‖
    `‖ℛg‖₁ ≤ ‖g‖₁`.
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.rotationalAverage_zero.{u_1} {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (g : CohnElkies.Euclidean d → E) :
  CohnElkies.rotationalAverage g 0 = g 0
    theorem CohnElkies.rotationalAverage_zero.{u_1}
  {d : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E]
  (g : CohnElkies.Euclidean d → E) :
  CohnElkies.rotationalAverage g 0 = g 0
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.rotationalAverage_im_eq_zero {d : ℕ}
  {g : CohnElkies.Euclidean d → ℂ} (hg : CohnElkies.IsRealValued g) :
  CohnElkies.IsRealValued (CohnElkies.rotationalAverage g)
    theorem CohnElkies.rotationalAverage_im_eq_zero
  {d : ℕ} {g : CohnElkies.Euclidean d → ℂ}
  (hg : CohnElkies.IsRealValued g) :
  CohnElkies.IsRealValued
    (CohnElkies.rotationalAverage g)
    Rotational averaging preserves real values.
Proof for Lemma 3.2.3
uses 0

Continuity and integrability follow from Fubini–Tonelli for the probability measure dU, as does \|\mathcal{R}f\|_1 \le \int_{O(d)}\|f \circ U\|_1\,dU = \|f\|_1; U0 = 0 gives the value at the origin, and the average of a real function is real. Radiality uses that O(d) acts transitively on spheres (CohnElkies.orthogonal_transitive) and that dU is right invariant, so \mathcal{R}f(Ax) = \mathcal{R}f(x) for A \in O(d).

Lemma3.2.4
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let f be continuous and integrable on \mathbb{R}^d. Then \widehat{\mathcal{R}f} = \mathcal{R}\widehat f (Definition 3.2.1); in particular \widehat{\mathcal{R}f}(0) = \widehat f(0) by Lemma 3.2.3.

Lean code for Lemma3.2.4●1 theorem
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.fourier_rotationalAverage {d : ℕ}
  {g : CohnElkies.Euclidean d → ℂ} (hg : Continuous g)
  (hi : MeasureTheory.Integrable g MeasureTheory.volume)
  (ξ : CohnElkies.Euclidean d) :
  FourierTransform.fourier (CohnElkies.rotationalAverage g) ξ =
    CohnElkies.rotationalAverage (FourierTransform.fourier g) ξ
    theorem CohnElkies.fourier_rotationalAverage
  {d : ℕ} {g : CohnElkies.Euclidean d → ℂ}
  (hg : Continuous g)
  (hi :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (ξ : CohnElkies.Euclidean d) :
  FourierTransform.fourier
      (CohnElkies.rotationalAverage g) ξ =
    CohnElkies.rotationalAverage
      (FourierTransform.fourier g) ξ
    The Fourier transform commutes with rotational averaging: `𝓕(ℛg) = ℛ(𝓕g)` (report §2.1).
Proof for Lemma 3.2.4
uses 1

Fubini and the invariance \widehat{f \circ U} = \widehat f \circ U for orthogonal U (change of variables in Definition 1.1.2; CohnElkies.integral_fourierCharacter_mul).

Lemma3.2.5
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

If f is Schwartz, so is \mathcal{R}f (Definition 3.2.1), and \widehat{\mathcal{R}f} = \mathcal{R}\widehat f as Schwartz functions.

Lean code for Lemma3.2.5●2 declarations
  • defdefined in CohnElkies/Radialization.lean
    complete
    def CohnElkies.rotationalAverageSchwartz {d : ℕ}
  (f : CohnElkies.TestFunction d) : CohnElkies.TestFunction d
    def CohnElkies.rotationalAverageSchwartz
  {d : ℕ}
  (f : CohnElkies.TestFunction d) :
  CohnElkies.TestFunction d
    The rotational average of a test function, as a test function (report §2.1).
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.fourier_rotationalAverageSchwartz {d : ℕ}
  (f : CohnElkies.TestFunction d) :
  FourierTransform.fourier (CohnElkies.rotationalAverageSchwartz f) =
    CohnElkies.rotationalAverageSchwartz (FourierTransform.fourier f)
    theorem CohnElkies.fourier_rotationalAverageSchwartz
  {d : ℕ}
  (f : CohnElkies.TestFunction d) :
  FourierTransform.fourier
      (CohnElkies.rotationalAverageSchwartz
        f) =
    CohnElkies.rotationalAverageSchwartz
      (FourierTransform.fourier f)
    `𝓕(ℛf) = ℛ(𝓕f)` for a test function `f` (report §2.1).
Proof for Lemma 3.2.5
uses 1

Derivatives of \mathcal{R}f are averages of derivatives of f (differentiation under the integral sign, CohnElkies.iteratedFDeriv_integral), and the Schwartz seminorms of f \circ U equal those of f (CohnElkies.seminorm_compIsometry), whence the Schwartz property (CohnElkies.schwartzAverage); the Fourier identity is Lemma 3.2.4.

Lemma3.2.6
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 4
Reverse dependency previews
Preview
Lemma 3.2.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

If f \ge 0 (resp. f \le 0) on \{|x| \ge R\} then so is \mathcal{R}f (Definition 3.2.1).

Lean code for Lemma3.2.6●2 theorems
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.rotationalAverage_nonneg_of_norm_le {d : ℕ}
  {g : CohnElkies.Euclidean d → ℝ} {R : ℝ}
  (hg : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ g x)
  {x : CohnElkies.Euclidean d} (hx : R ≤ ‖x‖) :
  0 ≤ CohnElkies.rotationalAverage g x
    theorem CohnElkies.rotationalAverage_nonneg_of_norm_le
  {d : ℕ} {g : CohnElkies.Euclidean d → ℝ}
  {R : ℝ}
  (hg :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ g x)
  {x : CohnElkies.Euclidean d}
  (hx : R ≤ ‖x‖) :
  0 ≤ CohnElkies.rotationalAverage g x
    Rotational averaging preserves nonnegativity outside a ball (report §2.1: `r(ℛg) ≤ r(g)`).
  • theoremdefined in CohnElkies/Radialization.lean
    complete
    theorem CohnElkies.rotationalAverage_nonpos_of_le_norm {d : ℕ}
  {g : CohnElkies.Euclidean d → ℂ} (hg : Continuous g) {R : ℝ}
  (h : ∀ (y : CohnElkies.Euclidean d), R ≤ ‖y‖ → (g y).re ≤ 0)
  {x : CohnElkies.Euclidean d} (hx : R ≤ ‖x‖) :
  (CohnElkies.rotationalAverage g x).re ≤ 0
    theorem CohnElkies.rotationalAverage_nonpos_of_le_norm
  {d : ℕ} {g : CohnElkies.Euclidean d → ℂ}
  (hg : Continuous g) {R : ℝ}
  (h :
    ∀ (y : CohnElkies.Euclidean d),
      R ≤ ‖y‖ → (g y).re ≤ 0)
  {x : CohnElkies.Euclidean d}
  (hx : R ≤ ‖x‖) :
  (CohnElkies.rotationalAverage g x).re ≤
    0
    Nonpositivity outside the ball of any radius `R` is preserved by rotational averaging.
Proof for Lemma 3.2.6
uses 0

Exterior regions \{|x| \ge R\} are rotation-invariant, so pointwise sign conditions there are preserved by averaging.

Lemma3.2.7
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

If f \in \mathcal{A}_d then \mathcal{R}f \in \mathcal{A}_d^{\mathrm{rad}} (Definition 3.2.2) with the same values f(0) and \widehat f(0).

Lean code for Lemma3.2.7●3 declarations
  • defdefined in CohnElkies/Admissible/Radialization.lean
    complete
    def CohnElkies.Admissible.radialize {d : ℕ} (f : CohnElkies.Admissible d) :
  CohnElkies.RadialAdmissible d
    def CohnElkies.Admissible.radialize {d : ℕ}
  (f : CohnElkies.Admissible d) :
  CohnElkies.RadialAdmissible d
    The rotational average `ℛf = ∫_{O(d)} f(U ·) dU` of an admissible function, as a radial
admissible function (report §2.1): rotational averaging preserves every sign condition of (2).
  • theoremdefined in CohnElkies/Admissible/Radialization.lean
    complete
    theorem CohnElkies.Admissible.radialize_apply_zero {d : ℕ}
  (f : CohnElkies.Admissible d) : f.radialize.function 0 = f.function 0
    theorem CohnElkies.Admissible.radialize_apply_zero
  {d : ℕ} (f : CohnElkies.Admissible d) :
  f.radialize.function 0 = f.function 0
    `ℛf(0) = f(0)`.
  • theoremdefined in CohnElkies/Admissible/Radialization.lean
    complete
    theorem CohnElkies.Admissible.fourier_radialize_apply_zero {d : ℕ}
  (f : CohnElkies.Admissible d) :
  (FourierTransform.fourier f.radialize.function) 0 =
    (FourierTransform.fourier f.function) 0
    theorem CohnElkies.Admissible.fourier_radialize_apply_zero
  {d : ℕ} (f : CohnElkies.Admissible d) :
  (FourierTransform.fourier
        f.radialize.function)
      0 =
    (FourierTransform.fourier f.function)
      0
    `𝓕(ℛf)(0) = 𝓕f(0)`.
Proof for Lemma 3.2.7
Proof uses 4
Proof dependency previews
Preview
Lemma 3.2.3
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By Lemma 3.2.5, Lemma 3.2.3, Lemma 3.2.4 and Lemma 3.2.6 (applied to f with R = 1 and to \widehat f with R = 0).

Lemma3.2.8
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

If g \in \mathcal{E}_\varsigma(d) (Definition 1.2.1) is nonnegative outside some ball, then \mathcal{R}g is a radial element of \mathcal{E}_\varsigma(d): \widehat{\mathcal{R}g} = \varsigma\mathcal{R}g, \mathcal{R}g(0) = 0, \mathcal{R}g \ne 0; and r(\mathcal{R}g) \le r(g) for r as in Definition 1.2.2.

Lean code for Lemma3.2.8●2 declarations
  • defdefined in CohnElkies/SignUncertainty/Radialization.lean
    complete
    def CohnElkies.SignEigenfunction.radialize {d : ℕ} (hd : 0 < d) {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς) {R : ℝ}
  (hR : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.SignEigenfunction d ς
    def CohnElkies.SignEigenfunction.radialize
  {d : ℕ} (hd : 0 < d) {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς)
  {R : ℝ}
  (hR :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.SignEigenfunction d ς
    The rotational average `ℛg` of a sign eigenfunction `g` nonnegative outside a ball, as a sign
eigenfunction (report §2.1: `𝓕(ℛg) = ς ℛg`, `ℛg(0) = g(0) = 0`, `ℛg ≠ 0`).
  • theoremdefined in CohnElkies/SignUncertainty/Radialization.lean
    complete
    theorem CohnElkies.SignEigenfunction.signRadius_radialize_le {d : ℕ}
  (hd : 0 < d) {ς : ℤˣ} (g : CohnElkies.SignEigenfunction d ς) {R : ℝ}
  (hR : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.signRadius
      (CohnElkies.SignEigenfunction.radialize hd g hR).toFun ≤
    CohnElkies.signRadius g.toFun
    theorem CohnElkies.SignEigenfunction.signRadius_radialize_le
  {d : ℕ} (hd : 0 < d) {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς)
  {R : ℝ}
  (hR :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.signRadius
      (CohnElkies.SignEigenfunction.radialize
          hd g hR).toFun ≤
    CohnElkies.signRadius g.toFun
    `r(ℛg) ≤ r(g)`.
Proof for Lemma 3.2.8
Proof uses 4
Proof dependency previews
Preview
Lemma 3.2.3
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Lemma 3.2.3, Lemma 3.2.4 and Lemma 3.2.6 give the eigenfunction identity, the value at the origin and r(\mathcal{R}g) \le r(g); \mathcal{R}g \ne 0 is Lemma 3.2.13.

Lemma3.2.9
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

\inf_{f \in \mathcal{A}_d} f(0)/\widehat f(0) = \inf_{f \in \mathcal{A}_d^{\mathrm{rad}}} f(0)/\widehat f(0). Hence \mathrm{LP}_d in Definition 1.1.6 is unchanged when \mathcal{A}_d is replaced by \mathcal{A}_d^{\mathrm{rad}}, as in the radial formulation of Cohn and Miller.

Lean code for Lemma3.2.9●1 theorem
  • theoremdefined in CohnElkies/Admissible/Radialization.lean
    complete
    theorem CohnElkies.LP_eq_radial (d : ℕ) :
  CohnElkies.LP d =
    CohnElkies.unitBallVolume d / 2 ^ d *
      sInf (Set.range fun f ↦ CohnElkies.quotient f.toAdmissible)
    theorem CohnElkies.LP_eq_radial (d : ℕ) :
  CohnElkies.LP d =
    CohnElkies.unitBallVolume d / 2 ^ d *
      sInf
        (Set.range fun f ↦
          CohnElkies.quotient
            f.toAdmissible)
    Radial reduction of the Cohn–Elkies program (report §2.1): the infimum in (3) is unchanged
when `𝒜_d` is replaced by `𝒜_d^rad`.
Proof for Lemma 3.2.9
uses 1

The inequality \le holds since \mathcal{A}_d^{\mathrm{rad}} \subseteq \mathcal{A}_d. For \ge, given f \in \mathcal{A}_d, Lemma 3.2.7 gives \mathcal{R}f \in \mathcal{A}_d^{\mathrm{rad}} with the same quotient f(0)/\widehat f(0).

Lemma3.2.10
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

The constants \mathsf{A}_\varsigma(d) of Definition 1.2.3 are unchanged when the infimum is restricted to radial eigenfunctions: \mathsf{A}_\varsigma(d) = \inf\{r(g) : g \in \mathcal{E}_\varsigma(d) \text{ radial}\}.

Lean code for Lemma3.2.10●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/Radialization.lean
    complete
    theorem CohnElkies.signUncertaintyConstant_eq_radial {d : ℕ} (hd : 0 < d)
  (ς : ℤˣ) :
  CohnElkies.signUncertaintyConstant ς d =
    ⨅ g,
      ⨅ (_ : CohnElkies.IsRadial g.toFun), CohnElkies.signRadius g.toFun
    theorem CohnElkies.signUncertaintyConstant_eq_radial
  {d : ℕ} (hd : 0 < d) (ς : ℤˣ) :
  CohnElkies.signUncertaintyConstant ς d =
    ⨅ g,
      ⨅ (_ : CohnElkies.IsRadial g.toFun),
        CohnElkies.signRadius g.toFun
    Report §2.1: the infimum defining `A_ς(d)` may be taken over radial eigenfunctions only.
Proof for Lemma 3.2.10
uses 1

The inequality \le is immediate, the radial eigenfunctions being a subfamily. For \ge, let g \in \mathcal{E}_\varsigma(d). If r(g) = \infty there is nothing to prove; otherwise g is nonnegative outside some ball, so Lemma 3.2.8 makes \mathcal{R}g a radial member of \mathcal{E}_\varsigma(d) with r(\mathcal{R}g) \le r(g).

Lemma3.2.11
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

An integrable function on a nontrivial finite-dimensional real inner product space which vanishes outside a ball and whose Fourier transform vanishes outside a ball has identically vanishing Fourier transform, hence is zero almost everywhere.

Lean code for Lemma3.2.11●2 theorems
  • theoremdefined in CohnElkiesForMathlib/Analysis/Fourier/CompactSupport.lean
    complete
    theorem Real.fourierIntegral_eq_zero_of_eq_zero_outside_ball.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  [Nontrivial V] {f : V → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) {R : ℝ}
  (hsupp : ∀ (x : V), R < ‖x‖ → f x = 0)
  (hfourier : ∀ (x : V), R < ‖x‖ → FourierTransform.fourier f x = 0) :
  FourierTransform.fourier f = 0
    theorem Real.fourierIntegral_eq_zero_of_eq_zero_outside_ball.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  [Nontrivial V] {f : V → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  {R : ℝ}
  (hsupp : ∀ (x : V), R < ‖x‖ → f x = 0)
  (hfourier :
    ∀ (x : V),
      R < ‖x‖ →
        FourierTransform.fourier f x =
          0) :
  FourierTransform.fourier f = 0
    An integrable function vanishing outside a ball whose Fourier transform also vanishes outside
a ball has identically vanishing Fourier transform, since `𝓕 f` is entire along every ray through
the origin.
  • theoremdefined in CohnElkiesForMathlib/Analysis/Fourier/CompactSupport.lean
    complete
    theorem Real.ae_eq_zero_of_hasCompactSupport_fourierIntegral.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  [Nontrivial V] {f : V → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hsupp : HasCompactSupport f)
  (hfourier : HasCompactSupport (FourierTransform.fourier f)) :
  f =ᵐ[MeasureTheory.volume] 0
    theorem Real.ae_eq_zero_of_hasCompactSupport_fourierIntegral.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  [Nontrivial V] {f : V → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hsupp : HasCompactSupport f)
  (hfourier :
    HasCompactSupport
      (FourierTransform.fourier f)) :
  f =ᵐ[MeasureTheory.volume] 0
    An integrable function with compact support whose Fourier transform has compact support
vanishes almost everywhere.
Proof for Lemma 3.2.11
uses 1

Because g is integrable with bounded support, the integral \widehat g(\zeta) = \int g(x)e^{-2\pi i x\cdot\zeta}\,dx converges for every \zeta \in \mathbb{C}^d and defines an entire function (differentiation under the integral sign). Its restriction to \mathbb{R}^d is therefore real-analytic. By hypothesis \widehat g vanishes outside a ball, and it is continuous, so it vanishes on a nonempty open set; the identity theorem on the connected set \mathbb{R}^d gives \widehat g \equiv 0. Injectivity of the Fourier transform on L^1 (Definition 1.1.2) yields g = 0.

Lemma3.2.12
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 4
Reverse dependency previews
Preview
Lemma 3.2.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g \in L^1(\mathbb{R}^d) satisfy \widehat g = \varsigma g almost everywhere for some \varsigma \in \{-1,+1\}, and suppose g vanishes almost everywhere outside some ball. Then g = 0.

Lean code for Lemma3.2.12●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/Radialization.lean
    complete
    theorem CohnElkies.fourier_eq_zero_of_eq_zero_outside {d : ℕ} (hd : 0 < d)
  {f : CohnElkies.Euclidean d → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) {R : ℝ}
  (hsupp : ∀ (x : CohnElkies.Euclidean d), R < ‖x‖ → f x = 0)
  (hfourier :
    ∀ (x : CohnElkies.Euclidean d),
      R < ‖x‖ → FourierTransform.fourier f x = 0) :
  FourierTransform.fourier f = 0
    theorem CohnElkies.fourier_eq_zero_of_eq_zero_outside
  {d : ℕ} (hd : 0 < d)
  {f : CohnElkies.Euclidean d → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  {R : ℝ}
  (hsupp :
    ∀ (x : CohnElkies.Euclidean d),
      R < ‖x‖ → f x = 0)
  (hfourier :
    ∀ (x : CohnElkies.Euclidean d),
      R < ‖x‖ →
        FourierTransform.fourier f x =
          0) :
  FourierTransform.fourier f = 0
    Report §2.1: an integrable function vanishing outside a ball whose Fourier transform also
vanishes outside a ball has identically vanishing Fourier transform (`d ≥ 1`), since `𝓕 f` is
entire along every ray through the origin: the specialization to `ℝ^d` of
`Real.fourierIntegral_eq_zero_of_eq_zero_outside_ball`.
Proof for Lemma 3.2.12
uses 1

This is a special case of Lemma 3.2.11; the formal proof runs as follows. The finite measure g\,dx has an entire moment generating function z \mapsto \int e^{\langle z, x\rangle}g(x)\,dx (CohnElkies.analyticOnNhd_complexMGF_nnMeasure) whose values on the imaginary axis are the Fourier transform (CohnElkies.complexMGF_nnMeasure). Since \widehat g = g has compact support, this entire function vanishes on the tail of every imaginary ray, hence identically (CohnElkies.eq_zero_of_forall_imaginary_ray); so \widehat g = 0 and g = 0.

Lemma3.2.13
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

Let g be continuous, integrable and real on \mathbb{R}^d with \widehat g = \varsigma g, g \ne 0, and g(x) \ge 0 for all |x| \ge R, for some R \ge 0. Then \mathcal{R}g \ne 0.

Lean code for Lemma3.2.13●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/Radialization.lean
    complete
    theorem CohnElkies.SignEigenfunction.rotationalAverage_ne_zero {d : ℕ}
  (hd : 0 < d) {ς : ℤˣ} (g : CohnElkies.SignEigenfunction d ς) {R : ℝ}
  (hR : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.rotationalAverage g.toFun ≠ 0
    theorem CohnElkies.SignEigenfunction.rotationalAverage_ne_zero
  {d : ℕ} (hd : 0 < d) {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς)
  {R : ℝ}
  (hR :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ g.toFun x) :
  CohnElkies.rotationalAverage g.toFun ≠ 0
    Report §2.1: the rotational average of a sign eigenfunction that is nonnegative outside a
ball does not vanish.
Proof for Lemma 3.2.13
uses 1

Suppose \mathcal{R}g = 0. For |x| \ge R, (\mathcal{R}g)(x) is the average of g over the sphere of radius |x| (the image of Haar measure under U \mapsto Ux is the normalized surface measure). The integrand is continuous and nonnegative there and the average vanishes, so g vanishes on every sphere of radius at least R, i.e. outside B(0,R). Then Lemma 3.2.12 forces g = 0, a contradiction.

Definition3.2.14
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 5
Reverse dependency previews
Preview
Lemma 3.2.15
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g \in L^1_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) (continuous representative) satisfy \widehat g = \varsigma g and g(0) = 0, \varsigma \in \{-1,+1\}. Let \varphi be the normalized flat bump, \varphi(x) = c\,e^{-1/(1-4|x|^2)} for |x| < 1/2 and \varphi(x) = 0 otherwise, with \int\varphi = 1. For n \ge 1 set \varphi_n(x) = n^d\varphi(nx), \eta_n(x) = e^{-\pi|x|^2/n^2}, q_n = (\eta_n g) * \varphi_n, p_n = \tfrac12(q_n + \varsigma\widehat{q_n}). (The report convolves with the Gaussians \kappa_n(x) = n^de^{-\pi n^2|x|^2} instead of \varphi_n; see the final chapter.)

Lean code for Definition3.2.14●2 definitions
  • defdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    def CohnElkies.approximant {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς) (n : ℕ) :
  CohnElkies.TestFunction d
    def CohnElkies.approximant {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (n : ℕ) : CohnElkies.TestFunction d
    `q_n = (η_n h) ⋆ φ_n` (report §2.1, with the bump mollifier `φ_n`), as a test function.
  • defdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    def CohnElkies.projected {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς) (n : ℕ) :
  CohnElkies.TestFunction d
    def CohnElkies.projected {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (n : ℕ) : CohnElkies.TestFunction d
    `p_n = (q_n + ς 𝓕 q_n)/2` (report §2.1).
Lemma3.2.15
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.16
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

In the situation of Definition 3.2.14, q_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 as n \to \infty.

Lean code for Lemma3.2.15●5 theorems
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.approximant_real {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς) (n : ℕ) :
  CohnElkies.IsRealValued ⇑(CohnElkies.approximant h n)
    theorem CohnElkies.approximant_real {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (n : ℕ) :
  CohnElkies.IsRealValued
    ⇑(CohnElkies.approximant h n)
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.approximant_radial {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) (n : ℕ) :
  CohnElkies.IsRadial ⇑(CohnElkies.approximant h n)
    theorem CohnElkies.approximant_radial {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun)
  (n : ℕ) :
  CohnElkies.IsRadial
    ⇑(CohnElkies.approximant h n)
  • 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.tendsto_approximant {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(CohnElkies.approximant h n) x - ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    theorem CohnElkies.tendsto_approximant {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(CohnElkies.approximant h n) x -
            ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    `q_n → h` in `L¹` (report §2.1).
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.tendsto_fourier_approximant {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(FourierTransform.fourier (CohnElkies.approximant h n)) x -
            ↑↑ς * ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    theorem CohnElkies.tendsto_fourier_approximant
  {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(FourierTransform.fourier
                (CohnElkies.approximant h
                  n))
              x -
            ↑↑ς * ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    `𝓕 q_n → ς h` in `L¹` (report §2.1).
Proof for Lemma 3.2.15
uses 1

Mollification of the integrable function \eta_ng by the smooth compactly supported \varphi_n is smooth with all derivatives bounded, and \eta_n decays like a Gaussian, so q_n is Schwartz; it is radial and real because g, \varphi_n, \eta_n are. Since (\varphi_n) is an approximate identity, (\eta_ng)*\varphi_n \to g in L^1 (as \eta_n \to 1 boundedly). Using \widehat{\eta_n} = \kappa_n (Definition 1.1.2), \widehat{q_n} = \widehat{\eta_ng}\,\widehat{\varphi_n} = (\kappa_n * \widehat g)\widehat{\varphi_n} = \varsigma(g*\kappa_n)\widehat{\varphi_n}, and since g*\kappa_n \to g in L^1 and \widehat{\varphi_n} \to 1 boundedly, \widehat{q_n} \to \varsigma g in L^1.

Lemma3.2.16
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

In the situation of Definition 3.2.14, p_n is a real radial Schwartz function with \widehat{p_n} = \varsigma p_n, p_n \to g in L^1 and p_n(0) \to 0.

Lean code for Lemma3.2.16●5 theorems
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.projected_real {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) (n : ℕ) :
  CohnElkies.IsRealValued ⇑(CohnElkies.projected h n)
    theorem CohnElkies.projected_real {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun)
  (n : ℕ) :
  CohnElkies.IsRealValued
    ⇑(CohnElkies.projected h n)
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.projected_radial {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) (n : ℕ) :
  CohnElkies.IsRadial ⇑(CohnElkies.projected h n)
    theorem CohnElkies.projected_radial {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun)
  (n : ℕ) :
  CohnElkies.IsRadial
    ⇑(CohnElkies.projected h n)
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.fourier_projected {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) (n : ℕ) :
  FourierTransform.fourier (CohnElkies.projected h n) =
    ↑↑ς • CohnElkies.projected h n
    theorem CohnElkies.fourier_projected {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun)
  (n : ℕ) :
  FourierTransform.fourier
      (CohnElkies.projected h n) =
    ↑↑ς • CohnElkies.projected h n
    `𝓕 p_n = ς p_n` (report §2.1).
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.tendsto_projected {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(CohnElkies.projected h n) x - ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    theorem CohnElkies.tendsto_projected {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto
    (fun n ↦
      ∫ (x : CohnElkies.Euclidean d),
        ‖(CohnElkies.projected h n) x -
            ↑(h.toFun x)‖)
    Filter.atTop (nhds 0)
    `p_n → h` in `L¹` (report §2.1).
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.tendsto_projected_zero {d : ℕ} {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto (fun n ↦ (CohnElkies.projected h n) 0) Filter.atTop
    (nhds 0)
    theorem CohnElkies.tendsto_projected_zero {d : ℕ}
  {ς : ℤˣ}
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  Filter.Tendsto
    (fun n ↦ (CohnElkies.projected h n) 0)
    Filter.atTop (nhds 0)
    `p_n(0) → 0`: `q_n(0) = ∫ 𝓕 q_n → ∫ ς h = 0` and `𝓕 q_n(0) = ∫ q_n → ∫ h = 0`.
Proof for Lemma 3.2.16
uses 1

Since q_n is radial, hence even, \widehat{\widehat{q_n}} = q_n, so \widehat{p_n} = \tfrac12(\widehat{q_n} + \varsigma q_n) = \varsigma p_n; p_n is real radial Schwartz by Lemma 3.2.15, and p_n \to \tfrac12(g + \varsigma\widehat g) = g in L^1. Moreover q_n(0) = ((\eta_ng)*\varphi_n)(0) \to g(0) = 0 by continuity of g, and \widehat{q_n}(0) = \int q_n \to \int g = \widehat g(0) = \varsigma g(0) = 0, so p_n(0) \to 0.

Lemma3.2.17
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.18
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For \varsigma \in \{-1,+1\} there is \psi_\varsigma \in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) with \widehat{\psi_\varsigma} = \varsigma\psi_\varsigma and \psi_\varsigma(0) \ne 0: one of \varphi + \varsigma\widehat\varphi and x \mapsto \varphi(2x) + \varsigma\widehat{\varphi(2\cdot)}(x), for the bump \varphi of Definition 3.2.14, does not vanish at the origin.

Lean code for Lemma3.2.17●2 declarations
  • 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`.
  • defdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    def CohnElkies.eigenProjection {d : ℕ} (ς : ℤˣ)
  (φ : CohnElkies.TestFunction d) : CohnElkies.TestFunction d
    def CohnElkies.eigenProjection {d : ℕ}
  (ς : ℤˣ)
  (φ : CohnElkies.TestFunction d) :
  CohnElkies.TestFunction d
    `P_ς φ = φ + ς 𝓕 φ`: for radial `φ` this is (twice) the projection onto the
`ς`-eigenspace of `𝓕`.
Proof for Lemma 3.2.17
uses 0

Both are real radial Schwartz \varsigma-eigenfunctions (the bump is even). Their values at the origin are \varphi(0) + \varsigma\int\varphi and \varphi(0) + \varsigma2^{-d}\int\varphi, which cannot both vanish since \int\varphi = 1 > 0 and 2^{-d} \ne 1. (The report uses the Gaussian \psi_+ = e^{-\pi|x|^2} and the Hermite function \psi_- = (|x|^2 - \tfrac{d}{4\pi})e^{-\pi|x|^2} instead.)

Lemma3.2.18
Group: Radial reduction (17)
Group member previews
Preview
Definition 3.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 3.2.14
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Proposition 4.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

In the situation of Definition 3.2.14, with \psi_\varsigma from Lemma 3.2.17, the corrected approximants g_n = p_n - \dfrac{p_n(0)}{\psi_\varsigma(0)}\,\psi_\varsigma lie in \mathcal{S}_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}), satisfy \widehat{g_n} = \varsigma g_n and g_n(0) = 0, and g_n \to g in L^1(\mathbb{R}^d) as n \to \infty.

Lean code for Lemma3.2.18●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/SchwartzApproximation.lean
    complete
    theorem CohnElkies.exists_schwartz_approximation {d : ℕ} {ς : ℤˣ} (hd : 0 < d)
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  ∃ q,
    (∀ (n : ℕ),
        CohnElkies.IsRealValued ⇑(q n) ∧
          CohnElkies.IsRadial ⇑(q n) ∧
            FourierTransform.fourier (q n) = ↑↑ς • q n ∧ (q n) 0 = 0) ∧
      Filter.Tendsto
        (fun n ↦
          ∫ (x : CohnElkies.Euclidean d), ‖(q n) x - ↑(h.toFun x)‖)
        Filter.atTop (nhds 0)
    theorem CohnElkies.exists_schwartz_approximation
  {d : ℕ} {ς : ℤˣ} (hd : 0 < d)
  (h : CohnElkies.SignEigenfunction d ς)
  (hrad : CohnElkies.IsRadial h.toFun) :
  ∃ q,
    (∀ (n : ℕ),
        CohnElkies.IsRealValued ⇑(q n) ∧
          CohnElkies.IsRadial ⇑(q n) ∧
            FourierTransform.fourier
                  (q n) =
                ↑↑ς • q n ∧
              (q n) 0 = 0) ∧
      Filter.Tendsto
        (fun n ↦
          ∫ (x : CohnElkies.Euclidean d),
            ‖(q n) x - ↑(h.toFun x)‖)
        Filter.atTop (nhds 0)
    Report §2.1: a radial sign eigenfunction `h` (`𝓕 h = ς h`, `h(0) = 0`) is the `L¹` limit of
real radial test functions `g_n` with `𝓕 g_n = ς g_n` and `g_n(0) = 0`.
Proof for Lemma 3.2.18
Proof uses 2
Proof dependency previews
Preview
Lemma 3.2.16
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By Lemma 3.2.16 and Lemma 3.2.17, g_n is real radial Schwartz, \widehat{g_n} = \varsigma g_n, g_n(0) = p_n(0) - p_n(0) = 0, and \|g_n - g\|_1 \le \|p_n - g\|_1 + |p_n(0)|\,\|\psi_\varsigma\|_1/|\psi_\varsigma(0)| \to 0.