1.2. Fourier sign uncertainty
The packing sign conditions are related to the Bourgain–Clozel–Kahane uncertainty principle for
eventually nonnegative Fourier eigenfunctions, and to its anti-self-Fourier counterpart introduced
by Cohn and Gonçalves. The report works with the class of nonzero
g \in L^1(\mathbb{R}^d;\mathbb{R}) satisfying \widehat g = \varsigma g and g(0) = 0, where
pointwise values refer to the continuous Fourier-inversion representative. We use the following
equivalent formulation.
Let \varsigma \in \{-1,+1\}. A sign eigenfunction of eigenvalue \varsigma is a function
g : \mathbb{R}^d \to \mathbb{R} that is continuous, integrable, not identically zero, satisfies
\widehat g(\xi) = \varsigma\, g(\xi) for every \xi \in \mathbb{R}^d (with the convention of
Definition 1.1.2), and g(0) = 0. Write \mathcal{E}_\varsigma(d) for the set
of such functions.
This is equivalent to the report's formulation. If an L^1 class g satisfies
\widehat g = \varsigma g almost everywhere, then \widehat g \in L^1, and Fourier inversion
gives g = \varsigma\,\widehat{g} almost everywhere; the right-hand side is continuous and
bounded, so g has a continuous representative, which is unique because two continuous
functions that agree almost everywhere agree everywhere, and this representative satisfies
\widehat g = \varsigma g pointwise. Conversely, a continuous integrable g with
\widehat g = \varsigma g pointwise defines such an L^1 class. All pointwise values and sign
conditions below refer to this representative.
Lean code for Definition1.2.1●1 definition
Associated Lean declarations
-
CohnElkies.SignEigenfunction[complete]
-
CohnElkies.SignEigenfunction[complete]
-
structuredefined in CohnElkies/Basic.leancomplete
structure CohnElkies.SignEigenfunction (d : ℕ) (ς : ℤˣ) : Type
structure CohnElkies.SignEigenfunction (d : ℕ) (ς : ℤˣ) : Type
The class of (5)–(6) of the report: `0 ≠ g ∈ L¹(ℝ^d;ℝ)` with `𝓕 g = ς g` and `g(0) = 0`, where `ς = ±1`. Pointwise values refer to the continuous Fourier-inversion representative: requiring `𝓕 g = ς g` *everywhere* (not only almost everywhere) forces `g` to be that representative, since the Fourier transform of an integrable function is continuous.
Fields
toFun : CohnElkies.Euclidean d → ℝ
The function `g : ℝ^d → ℝ`.
integrable : MeasureTheory.Integrable self.toFun MeasureTheory.volume
`g` is integrable.
fourier_eq : ∀ (ξ : CohnElkies.Euclidean d), FourierTransform.fourier (fun x ↦ ↑(self.toFun x)) ξ = ↑↑ς * ↑(self.toFun ξ)
`𝓕 g = ς g` everywhere.
ne_zero : self.toFun ≠ 0
`g` is not the zero function.
zero : self.toFun 0 = 0
`g(0) = 0`.
For g : \mathbb{R}^d \to \mathbb{R} define the last-sign radius (equation (5))
r(g) = \inf\{ R \ge 0 : g(x) \ge 0 \text{ for all } |x| \ge R \} \in [0,\infty],
with r(g) = \infty when no such radius exists.
Lean code for Definition1.2.2●1 definition
Associated Lean declarations
-
CohnElkies.signRadius[complete]
-
CohnElkies.signRadius[complete]
-
defdefined in CohnElkies/Basic.leancomplete
def CohnElkies.signRadius {d : ℕ} (g : CohnElkies.Euclidean d → ℝ) : ENNReal
def CohnElkies.signRadius {d : ℕ} (g : CohnElkies.Euclidean d → ℝ) : ENNReal
The last-sign radius `r(g) = inf {R ≥ 0 : g(x) ≥ 0 for ‖x‖ ≥ R}` of (5), with `r(g) = ⊤` when no such radius exists.
For \varsigma \in \{-1,+1\} and d \ge 1 define (equation (6))
\mathsf{A}_\varsigma(d) = \inf\{ r(g) : g \in \mathcal{E}_\varsigma(d) \} \in [0,\infty],
with r(g) from Definition 1.2.2 and \mathcal{E}_\varsigma(d) from
Definition 1.2.1. The signs +1 and -1 give the original
(Bourgain–Clozel–Kahane) and the complementary (Cohn–Gonçalves) uncertainty problems.
Lean code for Definition1.2.3●1 definition
Associated Lean declarations
-
CohnElkies.signUncertaintyConstant[complete]
-
CohnElkies.signUncertaintyConstant[complete]
-
defdefined in CohnElkies/Basic.leancomplete
def CohnElkies.signUncertaintyConstant (ς : ℤˣ) (d : ℕ) : ENNReal
def CohnElkies.signUncertaintyConstant (ς : ℤˣ) (d : ℕ) : ENNReal
The sign-uncertainty constants `A_ς(d) = inf r(g)` of (6).
The sign-uncertainty constants of Definition 1.2.3 satisfy
\lim_{d\to\infty} \mathsf{A}_+(d)/\sqrt d = \lim_{d\to\infty} \mathsf{A}_-(d)/\sqrt d = 1/\pi.
In particular \mathsf{A}_\pm(d) < \infty for all sufficiently large d.
Lean code for Theorem1.2.4●3 theorems
Associated Lean declarations
-
theoremdefined in CohnElkies/SignUncertainty/Main.leancomplete
theorem CohnElkies.signUncertaintyConstant_div_sqrt_tendsto (ς : ℤˣ) : Filter.Tendsto (fun d ↦ CohnElkies.signUncertaintyConstant ς d / ENNReal.ofReal √↑d) Filter.atTop (nhds (ENNReal.ofReal Real.pi⁻¹))
theorem CohnElkies.signUncertaintyConstant_div_sqrt_tendsto (ς : ℤˣ) : Filter.Tendsto (fun d ↦ CohnElkies.signUncertaintyConstant ς d / ENNReal.ofReal √↑d) Filter.atTop (nhds (ENNReal.ofReal Real.pi⁻¹))
Theorem 1.2 of the report: `A_±(d)/√d → 1/π`.
-
theoremdefined in CohnElkies/SignUncertainty/Main.leancomplete
theorem CohnElkies.tendsto_toReal_signUncertaintyConstant_div_sqrt (ς : ℤˣ) : Filter.Tendsto (fun d ↦ (CohnElkies.signUncertaintyConstant ς d).toReal / √↑d) Filter.atTop (nhds Real.pi⁻¹)
theorem CohnElkies.tendsto_toReal_signUncertaintyConstant_div_sqrt (ς : ℤˣ) : Filter.Tendsto (fun d ↦ (CohnElkies.signUncertaintyConstant ς d).toReal / √↑d) Filter.atTop (nhds Real.pi⁻¹)
Theorem 1.2 of the report in real form: `A_±(d)/√d → 1/π`, with `A_ς(d)` read as a real number (`⊤.toReal = 0`, which only happens for finitely many `d`).
-
theoremdefined in CohnElkies/SignUncertainty/Main.leancomplete
theorem CohnElkies.eventually_signUncertaintyConstant_lt_top (ς : ℤˣ) : ∀ᶠ (d : ℕ) in Filter.atTop, CohnElkies.signUncertaintyConstant ς d < ⊤
theorem CohnElkies.eventually_signUncertaintyConstant_lt_top (ς : ℤˣ) : ∀ᶠ (d : ℕ) in Filter.atTop, CohnElkies.signUncertaintyConstant ς d < ⊤
The infimum `A_ς(d)` of report (6) is finite for all large `d` (report, proof of Theorem 1.2: `A_ς(d) ≤ R_{ε,d}`).
Lower bound. Fix 0 < c < 1/\pi and \varsigma \in \{-1,+1\}. By Proposition 4.2.1 there is
d_0(c) such that for d \ge d_0(c) no g \in \mathcal{E}_\varsigma(d) is nonnegative on
\{|x| \ge c\sqrt d\}. If some g \in \mathcal{E}_\varsigma(d) had r(g) < c\sqrt d, the
definition Definition 1.2.2 would give a radius R < c\sqrt d with g \ge 0 on
\{|x| \ge R\} \supseteq \{|x| \ge c\sqrt d\}, a contradiction. Hence
\mathsf{A}_\varsigma(d) \ge c\sqrt d for d \ge d_0(c), and
\liminf_{d\to\infty} \mathsf{A}_\varsigma(d)/\sqrt d \ge 1/\pi after letting
c \uparrow 1/\pi.
Upper bound. By Theorem 5.5.7, \mathsf{A}_\varsigma(d) is finite for large d and
\limsup_{d\to\infty} \mathsf{A}_\varsigma(d)/\sqrt d \le 1/\pi.
Although the two asymptotics coincide, the appendix of the report shows that
\mathsf{A}_+(d) < \mathsf{A}_-(d) for every d \ge 1 (Theorem 6.1.9,
through the existence of extremizers, Theorem 6.2.11).