TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hardy's Gaussian uncertainty principle in $R^{n}$

Statement

Assume countable choice. Let $n \geq 1$ and $a, b, C > 0$ and let $f : R^{n} \to C$ be measurable with $∣ f (x) ∣ \leq C e^{- π a ∣ x ∣^{2}}$ for almost every $x$ ; then $f \in L^{1}$ and $\hat{f}$ is its continuous $L^{1}$ transform (Fourier transform on complex L1 classes). Suppose $∣ \hat{f} (ξ) ∣ \leq C e^{- π b ∣ ξ ∣^{2}}$ for every $ξ \in R^{n}$ . Then: (i) if $a b > 1$ , $f = 0$ almost everywhere; (ii) if $a b = 1$ , there is $c \in C$ with $f (x) = c e^{- π a ∣ x ∣^{2}}$ for almost every $x$ ; necessarily $c = \hat{f} (0) a^{n / 2}$ with $\hat{f} (0) = \int f$ . Equality in (ii) is asserted almost everywhere only; no continuity of $f$ is assumed.

Facts & Assumptions

Given: Countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), reals $a, b, C > 0$ , and a measurable $f : R^{n} \to C$ with $∣ f (x) ∣ \leq C e^{- π a ∣ x ∣^{2}}$ for almost every $x$ and $∣ \hat{f} (ξ) ∣ \leq C e^{- π b ∣ ξ ∣^{2}}$ for every $ξ \in R^{n}$ .

[F1]

Countable choice is assumed; it is the hypothesis carried by the entire continuation, the Gaussian transform and the uniqueness theorem below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

Gaussian decay gives an entire continuation: $f \in L^{1}$ , $F (z) : = \int_{R^{n}} f (x) e^{- 2 π i x \cdot z} d x$ converges absolutely for every $z \in C^{n}$ , has entire coordinate slices, satisfies $F (x) = \hat{f} (x)$ for real $x$ , and $∣ F (z) ∣ \leq C a^{- n / 2} e^{π ∣ Im z ∣^{2} / a}$ for every $z \in C^{n}$ (Gaussian decay gives an entire Fourier-Laplace transform and its growth bound).

[F3]

One-variable rigidity: if $a, b > 0$ , $C_{1}, C_{2} \geq 0$ and the entire $φ : C \to C$ satisfies $∣ φ (x + i y) ∣ \leq C_{1} e^{π y^{2} / a}$ and $∣ φ (x) ∣ \leq C_{2} e^{- π b x^{2}}$ for all real $x, y$ , then $φ \equiv 0$ when $a b > 1$ , and $φ (z) = φ (0) e^{- π z^{2} / a}$ for all $z \in C$ when $a b = 1$ (Entire rigidity under Gaussian growth and real-axis decay).

[F4]

A separately holomorphic $G : C^{n} \to C$ vanishing on a nondegenerate real box is identically zero (Separately holomorphic functions vanishing on a real box are zero).

[F5]

For every $t > 0$ the Gaussian $e^{- π t ∣ x ∣^{2}}$ is absolutely integrable with $L^{1}$ transform $t^{- n / 2} e^{- π ∣ ξ ∣^{2} / t}$ (Euclidean Gaussian transform with the 2π normalization).

[F6]

The $L^{1}$ transform is defined by $\hat{g} (ξ) = \int g (x) e^{- 2 π i x \cdot ξ} d x$ , so $\hat{g} (0) = \int g$ ; if $g, h \in L^{1}$ have equal transforms then $g = h$ almost everywhere; a scalar multiple has the correspondingly scaled transform (Fourier transform on complex L1 classes, Uniqueness of the L1 Fourier transform).

Proof

technique · apply one-variable rigidity on coordinate slices, then iterate the critical factors

1.1F1F2given

Entire continuation. By [F1, F2], $f \in L^{1}$ and its continuation $F$ has entire coordinate slices, $F (x) = \hat{f} (x)$ for real $x$ , and $∣ F (z) ∣ \leq C a^{- n / 2} e^{π ∣ Im z ∣^{2} / a}, ∣ F (x) ∣ \leq C e^{- π b ∣ x ∣^{2}} .$

2.1F3step 1.1

Coordinate rigidity. Fix $j$ and real coordinates $y_{k}$ for $k \neq j$ . The entire slice $φ (w) = F (y_{1}, \dots, y_{j - 1}, w, y_{j + 1}, \dots, y_{n})$ satisfies $∣ φ (u + i v) ∣ \leq C a^{- n / 2} e^{π v^{2} / a}, ∣ φ (u) ∣ \leq C e^{- π b \sum_{k \neq j} y_{k}^{2}} e^{- π b u^{2}} .$ Thus [F3] applies with $C_{1} = C a^{- n / 2}$ and $C_{2} = C e^{- π b \sum_{k \neq j} y_{k}^{2}}$ . If $a b > 1$ , every such slice is zero, so $F = 0$ on $R^{n}$ . If $a b = 1$ , every such slice satisfies $φ (w) = φ (0) e^{- π w^{2} / a}$ .

3.1F4step 2.1

Critical factorization. If $a b = 1$ , apply the slice identity in step 2.1 successively to coordinates $1, \dots, n$ of a real point $x$ , leaving the other coordinates real at each application. This gives $F (x) = F (0) \prod_{j = 1}^{n} e^{- π x_{j}^{2} / a} = F (0) e^{- π ∣ x ∣^{2} / a} .$ In fact the same formula holds for complex $z$ : the difference $F (z) - F (0) e^{- π \sum_{j} z_{j}^{2} / a}$ has entire coordinate slices and vanishes on $[0, 1]^{n}$ , so [F4] makes it identically zero. This includes $n = 1$ .

4.1F2F5F6step 2.1step 3.1∎

Fourier uniqueness and the constant. If $a b > 1$ , step 2.1 gives $\hat{f} = 0$ and [F6] yields $f = 0$ almost everywhere. If $a b = 1$ , [F5] says $g (x) = F (0) a^{n / 2} e^{- π a ∣ x ∣^{2}}$ is integrable with transform $F (0) e^{- π ∣ ξ ∣^{2} / a}$ , equal to $\hat{f}$ by step 3.1. By [F6], $f = g$ almost everywhere. Hence the scalar is $c = F (0) a^{n / 2} = \hat{f} (0) a^{n / 2}$ , and $\hat{f} (0) = \int f$ .

Depends on

Used by

Dependency tree · two levels

49 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Terence Tao, Hardy's uncertainty principle (blog post, 18 February 2009) (standard reference, not scraped)
Aingeru Fernández-Bertolín and Eugenia Malinnikova, Dynamical Versions of Hardy's Uncertainty Principle: A Survey (arXiv:2210.03369) (standard reference, not scraped)
Calder Sheagren, Uncertainty Principles with Fourier Analysis (University of Chicago REU 2017, author PDF) (standard reference, not scraped)

Hardy's Gaussian uncertainty principle in RnRn