The Cohn–Elkies exponent and sign uncertainty

6.1. Proposition A.1: the tail-integration operator🔗

The tail-integration operator T_d and the comparison \mathsf{A}_+(d) < \mathsf{A}_-(d) (Proposition A.1 of the report). For an anti-self-Fourier radial function g, the central Mellin moment M_g(d/2) vanishes. Integrating the radial tail of g therefore produces a self-Fourier function with a strictly smaller last-sign radius; applied to a radial extremizer for \mathsf{A}_-(d), whose existence is proved in the next section, this gives the strict inequality. Throughout, d \ge 1, \lambda = d/2, and g denotes the continuous Fourier-inversion representative, as in Definition 1.2.1.

Definition6.1.1
Group: Comparison of the constants (20)
Group member previews
Preview
Lemma 6.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 6
Reverse dependency previews
Preview
Lemma 6.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g \in \mathcal{E}_-(d) (Definition 1.2.1) be radial, i.e. 0 \ne g \in L^1_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) with \widehat g = -g and g(0) = 0. Define T_dg(0) = 0 and, for x \ne 0 (equation (87)), (T_dg)(x) = \dfrac{\lambda}{2}\int_1^\infty t^{\lambda-1}g(tx)\,dt. In terms of the radial profile, (T_dg)(r) = \dfrac{\lambda}{2}r^{-\lambda}\int_r^\infty s^{\lambda-1}g(s)\,ds for r > 0 (large-scale representation).

Lean code for Definition6.1.1●2 declarations
  • defdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    def CohnElkies.tailIntegral (d : ℕ) (g : CohnElkies.Euclidean d → ℝ)
  (x : CohnElkies.Euclidean d) : ℝ
    def CohnElkies.tailIntegral (d : ℕ)
  (g : CohnElkies.Euclidean d → ℝ)
  (x : CohnElkies.Euclidean d) : ℝ
    The tail-integration operator `T_d g (x) = (λ/2) ∫_1^∞ t^{λ-1} g(t x) dt` of report (87),
`λ = d/2`, with `T_d g (0) = 0`.
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.tailIntegral_of_ne_zero {d : ℕ}
  (g : CohnElkies.Euclidean d → ℝ) {x : CohnElkies.Euclidean d}
  (hx : x ≠ 0) :
  CohnElkies.tailIntegral d g x =
    ↑d / 2 / 2 * ∫ (t : ℝ) in Set.Ioi 1, t ^ (↑d / 2 - 1) * g (t • x)
    theorem CohnElkies.tailIntegral_of_ne_zero {d : ℕ}
  (g : CohnElkies.Euclidean d → ℝ)
  {x : CohnElkies.Euclidean d}
  (hx : x ≠ 0) :
  CohnElkies.tailIntegral d g x =
    ↑d / 2 / 2 *
      ∫ (t : ℝ) in Set.Ioi 1,
        t ^ (↑d / 2 - 1) * g (t • x)
Lemma6.1.2
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 6.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g be as in Definition 6.1.1. Then g is bounded and continuous, and \int_{\mathbb{R}^d}|g(x)||x|^{-\lambda}\,dx < \infty.

Lean code for Lemma6.1.2●3 theorems
  • theoremdefined in CohnElkies/SignUncertainty/Basic.lean
    complete
    theorem CohnElkies.SignEigenfunction.continuous {d : ℕ} {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς) : Continuous g.toFun
    theorem CohnElkies.SignEigenfunction.continuous
  {d : ℕ} {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς) :
  Continuous g.toFun
    A sign eigenfunction is continuous (it is `ς` times the Fourier transform of an integrable
function).
  • theoremdefined in CohnElkies/SignUncertainty/Basic.lean
    complete
    theorem CohnElkies.SignEigenfunction.norm_apply_le {d : ℕ} {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς) (x : CohnElkies.Euclidean d) :
  ‖g.toFun x‖ ≤ ∫ (y : CohnElkies.Euclidean d), ‖g.toFun y‖
    theorem CohnElkies.SignEigenfunction.norm_apply_le
  {d : ℕ} {ς : ℤˣ}
  (g : CohnElkies.SignEigenfunction d ς)
  (x : CohnElkies.Euclidean d) :
  ‖g.toFun x‖ ≤
    ∫ (y : CohnElkies.Euclidean d),
      ‖g.toFun y‖
    A sign eigenfunction is bounded by its `L¹` norm: `|g(x)| = |𝓕 g (x)| ≤ ‖g‖₁`.
  • theoremdefined in CohnElkies/SignUncertainty/MellinCancellation.lean
    complete
    theorem CohnElkies.integrable_mul_norm_rpow_neg_half {d : ℕ} (hd : 0 < d)
  {g : CohnElkies.Euclidean d → ℝ}
  (hg : MeasureTheory.Integrable g MeasureTheory.volume) {C : ℝ}
  (hC : ∀ (x : CohnElkies.Euclidean d), ‖g x‖ ≤ C) :
  MeasureTheory.Integrable (fun x ↦ g x * ‖x‖ ^ (-(↑d / 2)))
    MeasureTheory.volume
    theorem CohnElkies.integrable_mul_norm_rpow_neg_half
  {d : ℕ} (hd : 0 < d)
  {g : CohnElkies.Euclidean d → ℝ}
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {C : ℝ}
  (hC :
    ∀ (x : CohnElkies.Euclidean d),
      ‖g x‖ ≤ C) :
  MeasureTheory.Integrable
    (fun x ↦ g x * ‖x‖ ^ (-(↑d / 2)))
    MeasureTheory.volume
    `∫ |g(x)| ‖x‖^{-λ} dx < ∞` for a bounded integrable `g` on `ℝ^d`, since `λ = d/2 < d`.
Proof for Lemma 6.1.2
uses 1

Since g = -\widehat g \in L^1, Fourier inversion makes g bounded and continuous (Definition 1.1.2); splitting at |x| = 1 and using \lambda < d gives the finiteness of \int|g||x|^{-\lambda}.

Lemma6.1.3
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 6.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Let g be as in Definition 6.1.1. Then the central Mellin moment vanishes (equation (88)): \int_{\mathbb{R}^d}g(x)|x|^{-\lambda}\,dx = 0, i.e. M_g(\lambda) = \int_0^\infty g(r)\,r^{\lambda-1}\,dr = 0, the integrals converging absolutely by Lemma 6.1.2.

Lean code for Lemma6.1.3●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/MellinCancellation.lean
    complete
    theorem CohnElkies.SignEigenfunction.integral_mul_norm_rpow_eq_zero {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1)) :
  ∫ (x : CohnElkies.Euclidean d), g.toFun x * ‖x‖ ^ (-(↑d / 2)) = 0
    theorem CohnElkies.SignEigenfunction.integral_mul_norm_rpow_eq_zero
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1)) :
  ∫ (x : CohnElkies.Euclidean d),
      g.toFun x * ‖x‖ ^ (-(↑d / 2)) =
    0
    The central Mellin cancellation for `g ∈ E₋(d)`: `∫ g(x) ‖x‖^{-λ} dx = 0`, `λ = d/2` (report,
proof of Proposition A.1: Gaussian duality makes `∫_0^∞ t^{λ/2-1} J(t) dt` its own negative).
Proof for Lemma 6.1.3
uses 1

The Mellin–Fourier identity (9) was established only for Schwartz functions, so we verify its central consequence directly. Set J(t) = \int_{\mathbb{R}^d}g(x)e^{-\pi t|x|^2}\,dx for t > 0. Gaussian duality e^{-\pi t|x|^2} = t^{-\lambda}\widehat{e^{-\pi|\cdot|^2/t}}(x), the pairing \int g\widehat\phi = \int\widehat g\phi, and \widehat g = -g give J(t) = -t^{-\lambda}J(1/t). Tonelli's theorem gives \int_0^\infty t^{\lambda/2-1}|J(t)|\,dt \le \dfrac{\Gamma(\lambda/2)}{\pi^{\lambda/2}}\int_{\mathbb{R}^d}|g(x)||x|^{-\lambda}\,dx < \infty. Hence the substitution t \mapsto 1/t makes \int_0^\infty t^{\lambda/2-1}J(t)\,dt equal to its own negative, so it vanishes. On the other hand, Fubini and Gaussian integration express the same quantity as \dfrac{\Gamma(\lambda/2)}{\pi^{\lambda/2}}\int_{\mathbb{R}^d}g(x)|x|^{-\lambda}\,dx, which in polar coordinates (Lemma 3.3.2) equals \dfrac{\Gamma(\lambda/2)}{\pi^{\lambda/2}}S_d\int_0^\infty g(r)r^{\lambda-1}\,dr. This proves (88).

Lemma6.1.4
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 6.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g be as in Definition 6.1.1. The integral defining T_dg(x) converges absolutely for x \ne 0, and T_dg is integrable with \|T_dg\|_1 \le \tfrac12\|g\|_1.

Lean code for Lemma6.1.4●3 theorems
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.integrable_tailIntegral_kernel {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1)) :
  MeasureTheory.Integrable
    (fun p ↦ p.2 ^ (↑d / 2 - 1) * g.toFun (p.2 • p.1))
    (MeasureTheory.volume.prod
      (MeasureTheory.volume.restrict (Set.Ioi 1)))
    theorem CohnElkies.SignEigenfunction.integrable_tailIntegral_kernel
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1)) :
  MeasureTheory.Integrable
    (fun p ↦
      p.2 ^ (↑d / 2 - 1) *
        g.toFun (p.2 • p.1))
    (MeasureTheory.volume.prod
      (MeasureTheory.volume.restrict
        (Set.Ioi 1)))
    The integrand `(x, t) ↦ t^{λ-1} g(t x)` of (87) is absolutely integrable on `ℝ^d × (1, ∞)`
(Tonelli: `∫ |g(t x)| dx = t^{-d} ‖g‖₁` and `∫_1^∞ t^{λ-1-d} dt < ∞`).
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.integrable_tailIntegral {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  MeasureTheory.Integrable (CohnElkies.tailIntegral d g.toFun)
    MeasureTheory.volume
    theorem CohnElkies.SignEigenfunction.integrable_tailIntegral
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  MeasureTheory.Integrable
    (CohnElkies.tailIntegral d g.toFun)
    MeasureTheory.volume
    `T_d g` is integrable.
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.integral_norm_tailIntegral_le {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  ∫ (x : CohnElkies.Euclidean d),
      ‖CohnElkies.tailIntegral d g.toFun x‖ ≤
    1 / 2 * ∫ (x : CohnElkies.Euclidean d), ‖g.toFun x‖
    theorem CohnElkies.SignEigenfunction.integral_norm_tailIntegral_le
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  ∫ (x : CohnElkies.Euclidean d),
      ‖CohnElkies.tailIntegral d g.toFun
          x‖ ≤
    1 / 2 *
      ∫ (x : CohnElkies.Euclidean d),
        ‖g.toFun x‖
    `‖T_d g‖₁ ≤ ½ ‖g‖₁` (report, proof of Proposition A.1).
Proof for Lemma 6.1.4
uses 0

For x \ne 0, in the radial profile \int_1^\infty t^{\lambda-1}|g(tx)|\,dt = |x|^{-\lambda}\int_{|x|}^\infty s^{\lambda-1}|g(s)|\,ds, and s^{\lambda-1} \le |x|^{-\lambda}s^{d-1} for s \ge |x|, so the integral is at most |x|^{-d}\|g\|_1/S_d: absolute convergence. Tonelli and d = 2\lambda give \|T_dg\|_1 \le \tfrac\lambda2\|g\|_1\int_1^\infty t^{-\lambda-1}\,dt = \tfrac12\|g\|_1.

Lemma6.1.5
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 6.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let g be as in Definition 6.1.1. For every x, T_dg(x) = -\dfrac{\lambda}{2}\int_0^1s^{\lambda-1}g(sx)\,ds (small-scale representation, equation (89)); this representation is continuous on all of \mathbb{R}^d and equals -g(0)/2 = 0 at x = 0. Hence T_dg is continuous and radial with T_dg(0) = 0.

Lean code for Lemma6.1.5●2 theorems
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.tailIntegral_eq_neg_integral_Ioo {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) (x : CohnElkies.Euclidean d) :
  CohnElkies.tailIntegral d g.toFun x =
    -(↑d / 2 / 2) *
      ∫ (s : ℝ) in Set.Ioo 0 1, s ^ (↑d / 2 - 1) * g.toFun (s • x)
    theorem CohnElkies.SignEigenfunction.tailIntegral_eq_neg_integral_Ioo
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun)
  (x : CohnElkies.Euclidean d) :
  CohnElkies.tailIntegral d g.toFun x =
    -(↑d / 2 / 2) *
      ∫ (s : ℝ) in Set.Ioo 0 1,
        s ^ (↑d / 2 - 1) * g.toFun (s • x)
    The small-scale representation of report (89): `T_d g (x) = -(λ/2) ∫_0^1 s^{λ-1} g(s x) ds`,
for every `x` (both sides vanish at `x = 0`); from the central Mellin cancellation along the ray
through `x`.
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.continuous_tailIntegral {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  Continuous (CohnElkies.tailIntegral d g.toFun)
    theorem CohnElkies.SignEigenfunction.continuous_tailIntegral
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  Continuous
    (CohnElkies.tailIntegral d g.toFun)
    `T_d g` is continuous (dominated convergence on the small-scale representation, `g` being
bounded and continuous and `s^{λ-1}` integrable on `(0, 1)`).
Proof for Lemma 6.1.5
Proof uses 2
Proof dependency previews
Preview
Lemma 6.1.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By Lemma 6.1.3, for x \ne 0, \int_0^\infty s^{\lambda-1}g(sx)\,ds = |x|^{-\lambda}M_g(\lambda) = 0, so -\int_0^1 = \int_1^\infty; at x = 0 both sides vanish. Continuity of the small-scale representation follows from dominated convergence, g being bounded and continuous (Lemma 6.1.2), and its value at 0 is -\tfrac\lambda2g(0)\int_0^1s^{\lambda-1}ds = -g(0)/2 = 0.

Lemma6.1.6
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

Let g be as in Definition 6.1.1. Then (equation (89)) \widehat{T_dg}(\xi) = \dfrac{\lambda}{2}\int_1^\infty t^{\lambda-d-1}\widehat g(\xi/t)\,dt = -\dfrac{\lambda}{2}\int_0^1s^{\lambda-1}g(s\xi)\,ds = T_dg(\xi) for every \xi: \widehat{T_dg} = T_dg.

Lean code for Lemma6.1.6●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/TailIntegral.lean
    complete
    theorem CohnElkies.SignEigenfunction.fourier_tailIntegral {d : ℕ} (hd : 0 < d)
  (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) (ξ : CohnElkies.Euclidean d) :
  FourierTransform.fourier
      (fun x ↦ ↑(CohnElkies.tailIntegral d g.toFun x)) ξ =
    ↑(CohnElkies.tailIntegral d g.toFun ξ)
    theorem CohnElkies.SignEigenfunction.fourier_tailIntegral
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun)
  (ξ : CohnElkies.Euclidean d) :
  FourierTransform.fourier
      (fun x ↦
        ↑(CohnElkies.tailIntegral d
            g.toFun x))
      ξ =
    ↑(CohnElkies.tailIntegral d g.toFun ξ)
    The self-Fourier property `𝓕 (T_d g) = T_d g` of report (89): Fubini on the large-scale
representation, Fourier scaling `𝓕(g(t ·))(ξ) = t^{-d} 𝓕 g (ξ/t) = -t^{-d} g(ξ/t)`, the
substitution `s = 1/t`, and the small-scale representation.
Proof for Lemma 6.1.6
Proof uses 2
Proof dependency previews
Preview
Lemma 6.1.4
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

The absolute convergence of Lemma 6.1.4 justifies Fourier transformation under the integral. Fourier scaling \widehat{g(t\,\cdot)}(\xi) = t^{-d}\widehat g(\xi/t) and \widehat g = -g give the first two expressions after the substitution s = 1/t, and Lemma 6.1.5 identifies the last one with T_dg(\xi).

Proposition6.1.7
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Proposition 6.1.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let d \ge 1, \lambda = d/2, and let 0 \ne g \in L^1_{\mathrm{rad}}(\mathbb{R}^d;\mathbb{R}) satisfy \widehat g = -g and g(0) = 0, with T_dg as in Definition 6.1.1. Then T_dg is nonzero, continuous, radial and integrable, with \widehat{T_dg} = T_dg, T_dg(0) = 0, \|T_dg\|_1 \le \tfrac12\|g\|_1; in particular T_dg \in \mathcal{E}_+(d).

Lean code for Proposition6.1.7●2 declarations
  • defdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    def CohnElkies.SignEigenfunction.tailIntegral {d : ℕ} (hd : 0 < d)
  (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) : CohnElkies.SignEigenfunction d 1
    def CohnElkies.SignEigenfunction.tailIntegral
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  CohnElkies.SignEigenfunction d 1
    Proposition A.1 of the report (Appendix A): for a radial `g ∈ E₋(d)`, `d ≥ 1`, the tail
integral `T_d g` of (87) is a self-Fourier sign eigenfunction, `T_d g ∈ E₊(d)`: it is continuous
and integrable, `𝓕 (T_d g) = T_d g`, `T_d g (0) = 0` and `T_d g ≠ 0`. Moreover `‖T_d g‖₁ ≤ ½ ‖g‖₁`
(`SignEigenfunction.integral_norm_tailIntegral_le`), `r(T_d g) ≤ r(g)`
(`SignEigenfunction.signRadius_tailIntegral_le`) and `r(T_d g) < r(g)` when `r(g) < ∞`
(`SignEigenfunction.signRadius_tailIntegral_lt`).
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.SignEigenfunction.tailIntegral_ne_zero {d : ℕ} (hd : 0 < d)
  (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  CohnElkies.tailIntegral d g.toFun ≠ 0
    theorem CohnElkies.SignEigenfunction.tailIntegral_ne_zero
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  CohnElkies.tailIntegral d g.toFun ≠ 0
    `T_d g ≠ 0` (Proposition A.1).
Proof for Proposition 6.1.7
Proof uses 4
Proof dependency previews
Preview
Definition 6.1.1
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Continuity and vanishing at the origin are Lemma 6.1.5, integrability and the norm bound Lemma 6.1.4, and the self-Fourier property Lemma 6.1.6. Differentiating the large-scale representation of Definition 6.1.1 in r gives (r\tfrac{d}{dr} + \lambda)T_dg = -\tfrac\lambda2g, i.e. (x\cdot\nabla + \lambda)T_dg = -\lambda g/2; since g \ne 0, also T_dg \ne 0. If g is Schwartz, differentiating the small-scale representation gives smoothness at the origin, and differentiating the large-scale representation gives rapid decay at infinity; thus T_dg is Schwartz.

Proposition6.1.8
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

In the situation of Proposition 6.1.7, r(T_dg) \le r(g), and if r(g) < \infty then T_dg > 0 on \{|x| \ge r(g)\} and r(T_dg) < r(g) (Definition 1.2.2).

Lean code for Proposition6.1.8●3 theorems
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.SignEigenfunction.tailIntegral_pos {d : ℕ} (hd : 0 < d)
  (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) {R : ℝ}
  (hR : ∀ (x : CohnElkies.Euclidean d), R ≤ ‖x‖ → 0 ≤ g.toFun x)
  {x : CohnElkies.Euclidean d} (hx : R ≤ ‖x‖) :
  0 < CohnElkies.tailIntegral d g.toFun x
    theorem CohnElkies.SignEigenfunction.tailIntegral_pos
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun)
  {R : ℝ}
  (hR :
    ∀ (x : CohnElkies.Euclidean d),
      R ≤ ‖x‖ → 0 ≤ g.toFun x)
  {x : CohnElkies.Euclidean d}
  (hx : R ≤ ‖x‖) :
  0 < CohnElkies.tailIntegral d g.toFun x
    Report, proof of Proposition A.1: if `g ≥ 0` outside the ball of radius `R`, then `T_d g > 0`
outside that ball. Nonnegativity is (87); if `T_d g (x) = 0`, then `g` vanishes on the ray beyond
`x`, hence (radiality) outside the ball of radius `‖x‖`, and so does `𝓕 g = -g`, which forces
`g = 0` by Fourier analyticity.
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.SignEigenfunction.signRadius_tailIntegral_le {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  CohnElkies.signRadius (CohnElkies.tailIntegral d g.toFun) ≤
    CohnElkies.signRadius g.toFun
    theorem CohnElkies.SignEigenfunction.signRadius_tailIntegral_le
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun) :
  CohnElkies.signRadius
      (CohnElkies.tailIntegral d
        g.toFun) ≤
    CohnElkies.signRadius g.toFun
    `r(T_d g) ≤ r(g)`: `T_d g ≥ 0` outside every ball outside which `g ≥ 0`.
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.SignEigenfunction.signRadius_tailIntegral_lt {d : ℕ}
  (hd : 0 < d) (g : CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun)
  (hfin : CohnElkies.signRadius g.toFun < ⊤) :
  CohnElkies.signRadius (CohnElkies.tailIntegral d g.toFun) <
    CohnElkies.signRadius g.toFun
    theorem CohnElkies.SignEigenfunction.signRadius_tailIntegral_lt
  {d : ℕ} (hd : 0 < d)
  (g :
    CohnElkies.SignEigenfunction d (-1))
  (hg : CohnElkies.IsRadial g.toFun)
  (hfin :
    CohnElkies.signRadius g.toFun < ⊤) :
  CohnElkies.signRadius
      (CohnElkies.tailIntegral d
        g.toFun) <
    CohnElkies.signRadius g.toFun
    Proposition A.1: if `r(g) < ∞` then `r(T_d g) < r(g)`. Indeed `r(g) > 0`, `T_d g > 0` on the
sphere of radius `r(g)`, and the (radial, continuous) function `T_d g` stays positive on a slightly
smaller sphere.
Proof for Proposition 6.1.8
uses 1

Let R = r(g) < \infty. Then R > 0: otherwise g \ge 0 everywhere and \int g = \widehat g(0) = -g(0) = 0 would force the continuous nonnegative g to vanish. For r \ge R we have g(s) \ge 0 for all s \ge r, so by (87) (T_dg)(r) = \tfrac\lambda2r^{-\lambda}\int_r^\infty s^{\lambda-1}g(s)\,ds \ge 0, and in fact > 0: equality would force g = 0 on [r,\infty), making both g and \widehat g = -g compactly supported, which Lemma 3.2.12 forbids. In particular T_dg(R) > 0, so by continuity T_dg > 0 on some [R - \delta, R] with \delta > 0, hence T_dg \ge 0 on \{|x| \ge R - \delta\} and r(T_dg) \le R - \delta < R.

Theorem6.1.9
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

For every d \ge 1, \mathsf{A}_+(d) < \mathsf{A}_-(d) (Definition 1.2.3).

Lean code for Theorem6.1.9●1 theorem
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.signUncertaintyConstant_one_lt_neg_one {d : ℕ} (hd : 0 < d) :
  CohnElkies.signUncertaintyConstant 1 d <
    CohnElkies.signUncertaintyConstant (-1) d
    theorem CohnElkies.signUncertaintyConstant_one_lt_neg_one
  {d : ℕ} (hd : 0 < d) :
  CohnElkies.signUncertaintyConstant 1 d <
    CohnElkies.signUncertaintyConstant
      (-1) d
    Appendix A of the report: `A₊(d) < A₋(d)` for every `d ≥ 1`. Let `g ∈ 𝓔₋(d)` attain
`A₋(d) < ∞` and let `h = ℛg` be its rotational average, a radial element of `𝓔₋(d)` with
`r(h) = A₋(d)`; then `T_d h ∈ 𝓔₊(d)` (Proposition A.1) has `r(T_d h) < r(h)`, so
`A₊(d) ≤ r(T_d h) < A₋(d)`.
Proof for Theorem 6.1.9
Proof uses 6
Proof dependency previews
Preview
Lemma 3.2.6
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By Theorem 6.2.11 there is an extremizer g \in \mathcal{E}_-(d), r(g) = \mathsf{A}_-(d) < \infty (Lemma 6.2.8). Put h = \mathcal{R}g, a nonzero radial element of \mathcal{E}_-(d) with r(h) \le r(g) (Lemma 3.2.8, Lemma 3.2.6). By Proposition 6.1.7 and Proposition 6.1.8, \mathsf{A}_+(d) \le r(T_dh) < r(h) \le r(g) = \mathsf{A}_-(d).

Theorem6.1.10
Group: Comparison of the constants (20)
Group member previews
Preview
Definition 6.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

For every d \ge 1 and \varsigma = \pm 1, \mathsf{A}_\varsigma(d) < \infty (Definition 1.2.3); together with Lemma 6.2.6, 0 < \mathsf{A}_\varsigma(d) < \infty.

Lean code for Theorem6.1.10●2 theorems
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.signUncertaintyConstant_lt_top {d : ℕ} (hd : 0 < d)
  (ς : ℤˣ) : CohnElkies.signUncertaintyConstant ς d < ⊤
    theorem CohnElkies.signUncertaintyConstant_lt_top
  {d : ℕ} (hd : 0 < d) (ς : ℤˣ) :
  CohnElkies.signUncertaintyConstant ς d <
    ⊤
    `A_ς(d) < ∞` for `d ≥ 1` and both signs: `A₊(d) < A₋(d) < ∞`.
  • theoremdefined in CohnElkies/SignUncertainty/AppendixA.lean
    complete
    theorem CohnElkies.signUncertaintyConstant_pos_lt_top {d : ℕ} (hd : 0 < d)
  (ς : ℤˣ) :
  0 < CohnElkies.signUncertaintyConstant ς d ∧
    CohnElkies.signUncertaintyConstant ς d < ⊤
    theorem CohnElkies.signUncertaintyConstant_pos_lt_top
  {d : ℕ} (hd : 0 < d) (ς : ℤˣ) :
  0 <
      CohnElkies.signUncertaintyConstant ς
        d ∧
    CohnElkies.signUncertaintyConstant ς
        d <
      ⊤
    `0 < A_ς(d) < ∞` for `d ≥ 1` and both signs.
Proof for Theorem 6.1.10
Proof uses 2
Proof dependency previews
Preview
Theorem 6.1.9
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

\mathsf{A}_+(d) < \mathsf{A}_-(d) < \infty by Theorem 6.1.9 and Lemma 6.2.8.