LemmaStatement: 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.

Subcritical Gaussians show the Hardy threshold $a b = 1$ is sharp

Statement

Assume countable choice. Let $n \geq 1$ and let $a, b > 0$ with $a b < 1$ . Then $(a, 1 / b)$ is a nonempty open interval, and for every $c$ with $a < c < 1 / b$ the Gaussian $f_{c} (x) : = e^{- π c ∣ x ∣^{2}}$ satisfies $∣ f_{c} (x) ∣ \leq e^{- π a ∣ x ∣^{2}}, ∣ \hat{f_{c}} (ξ) ∣ \leq c^{- n / 2} e^{- π b ∣ ξ ∣^{2}} (x, ξ \in R^{n}) .$ In particular Hardy's two Gaussian bounds hold at every subcritical pair $a b < 1$ with a nonzero function, so the vanishing and classification conclusions genuinely require $a b \geq 1$ .

Facts & Assumptions

Given: Countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), an integer $n \geq 1$ , reals $a, b > 0$ with $a b < 1$ , and a real $c$ with $a < c < 1 / b$ .

[F1]

Countable choice is assumed; it is the hypothesis carried by the Gaussian transform identity used below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

For every $t > 0$ , the Gaussians $e^{- π t ∣ x ∣^{2}}$ are absolutely integrable and have $L^{1}$ Fourier transform $t^{- n / 2} e^{- π ∣ ξ ∣^{2} / t}$ at every frequency; every polynomial times a positive real Gaussian is absolutely integrable (Euclidean Gaussian transform with the 2π normalization).

[F3]

The real exponential is strictly increasing on $R$ (The exponential function is strictly increasing); the real power $c^{s}$ of a positive base is a positive real number, and $s \mapsto c^{s}$ , $t \mapsto t^{s}$ are continuous on their domains (Real powers for positive bases, with the zero-base positive-exponent convention, Continuity and derivatives of positive-base real powers).

Proof

technique · direct

1.1F3given

The interval and the first bound. Since $b > 0$ , the inequality $a b < 1$ is equivalent to $a < 1 / b$ , so $(a, 1 / b)$ is a nonempty open interval and the given $c$ satisfies $c > a > 0$ . The function $f_{c}$ is continuous and hence measurable, with $f_{c} > 0$ and $f_{c} (0) = 1$ . For every $x \in R^{n}$ one has $- π c ∣ x ∣^{2} \leq - π a ∣ x ∣^{2}$ because $c \geq a$ , and the real exponential is strictly increasing [F3], so $0 < f_{c} (x) = e^{- π c ∣ x ∣^{2}} \leq e^{- π a ∣ x ∣^{2}}$ . Hence $∣ f_{c} (x) ∣ \leq e^{- π a ∣ x ∣^{2}}$ for every $x$ , and $f_{c} \neq 0$ .

2.1F1F2F3step 1.1

The transform and the second bound. By [F2] the Gaussian $f_{c}$ is absolutely integrable and its $L^{1}$ Fourier transform is $\hat{f_{c}} (ξ) = c^{- n / 2} e^{- π ∣ ξ ∣^{2} / c}$ for every $ξ \in R^{n}$ ; this is a positive real number. Since $c < 1 / b$ gives $b < 1 / c$ , one has $- π ∣ ξ ∣^{2} / c \leq - π b ∣ ξ ∣^{2}$ , and strict increase of the exponential [F3] gives $e^{- π ∣ ξ ∣^{2} / c} \leq e^{- π b ∣ ξ ∣^{2}}$ . The factor $c^{- n / 2}$ is positive by [F3]. Therefore $∣ \hat{f_{c}} (ξ) ∣ = c^{- n / 2} e^{- π ∣ ξ ∣^{2} / c} \leq c^{- n / 2} e^{- π b ∣ ξ ∣^{2}}$ for every $ξ$ .

3.1givenstep 1.1step 2.1∎

Conclusion. By steps 1.1 and 2.1 the nonzero Gaussian $f_{c}$ satisfies both Gaussian bounds of the subcritical pair $(a, b)$ whenever $a < c < 1 / b$ , and such $c$ exists at every pair with $a b < 1$ . Hence at every subcritical pair the two Gaussian hypotheses admit a nonzero solution, so the vanishing conclusion cannot hold below that threshold. Nor can the critical classification with rate $a$ hold: $f_{c} (x) / e^{- π a ∣ x ∣^{2}} = e^{- π (c - a) ∣ x ∣^{2}}$ equals $1$ at $0$ and is smaller at $x = (1, 0, \dots, 0)$ , so is nonconstant. By continuity it cannot be constant almost everywhere either.

Depends on

Used by

Critical, subcritical and supercritical Gaussian regimes for Hardy's theorem Example

Dependency tree · two levels

33 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

Calder Sheagren, Uncertainty Principles with Fourier Analysis (University of Chicago REU 2017, author PDF) (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)

Subcritical Gaussians show the Hardy threshold ab=1ab=1 is sharp