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.

Centring by translation and modulation preserves the variance product

Statement

Assume countable choice. Let $f \in L^{2} (R^{n}; C)$ be nonzero with finite second moments, spatial mean $a$ , frequency mean $b$ , and variances $V_{x} (f), V_{ξ} (f)$ as in Spatial and frequency centres and variances of an $L^{2}$ function with finite second moments (Translation of a function on $R^{n}$ ). Define $g (x) : = e^{- 2 π i b \cdot x} f (x + a) .$ Then $g \in L^{2}$ is nonzero with finite second moments, its spatial mean is $0$ and its frequency mean is $0$ , and for every $j$ $∥ x_{j} g ∥_{2} = ∥ (x_{j} - a_{j}) f ∥_{2}, ∥ ξ_{j} \hat{g} ∥_{2} = ∥ (ξ_{j} - b_{j}) \hat{f} ∥_{2} .$ Consequently $V_{x} (g) = V_{x} (f)$ , $V_{ξ} (g) = V_{ξ} (f)$ , and $V_{x} (g) V_{ξ} (g) = V_{x} (f) V_{ξ} (f)$ .

Facts & Assumptions

Given: Countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), a nonzero $f \in L^{2} (R^{n}; C)$ with finite second moments and means and variances $a, b, V_{x} (f), V_{ξ} (f)$ as in Spatial and frequency centres and variances of an $L^{2}$ function with finite second moments, and $g (x) = e^{- 2 π i b \cdot x} f (x + a)$ .

[F1]

Countable choice is assumed; it is used by the change-of-variables interface and to select the $L^{2}$ -approximating sequence in step 2.2 (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

Complex $L^{1}$ change of variables: for a $C^{1}$ diffeomorphism $T$ with absolute Jacobian determinant $∣ \det D T ∣$ and $h \in L^{1}$ , $\int h (T x) ∣ \det D T (x) ∣ d x = \int h (y) d y$ ; the affine maps $x \mapsto x + a$ and $ξ \mapsto ξ + b$ have determinant $1$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions). Complex $L^{2}$ carries the norm $∥ \cdot ∥_{2}$ of Complex completeness, density, and inner product: the consumer interface.

[F3]

Translation and modulation: with $τ_{a} f (x) = f (x - a)$ and $M_{b} f (x) = e^{2 π i b \cdot x} f (x)$ , for $f \in S$ one has $\hat{τ_{a} f} (ξ) = e^{- 2 π i a \cdot ξ} \hat{f} (ξ)$ and $\hat{M_{b} f} (ξ) = \hat{f} (ξ - b)$ at every frequency (Translation, modulation, linear dilation and reflection laws, Translation of a function on $R^{n}$ ).

[F4]

Schwartz functions lie in $L^{1} \cap L^{2}$ ; Schwartz space is dense in $L^{2}$ , the integral Fourier transform of any $L^{1} \cap L^{2}$ function represents its Plancherel transform almost everywhere, and Plancherel is an isometry (Schwartz derivatives are integrable, Schwartz space is dense in L2, Agreement of the integral and L2 transforms, Plancherel theorem).

[F5]

Integrable functions that agree almost everywhere have equal integrals (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

Proof

technique · direct

1.1F2given

The centred function is admissible on the spatial side. Translation preserves null equivalence and the $L^{2}$ norm by [F2], while modulation has unit modulus, so $g \in L^{2}$ and $∥ g ∥_{2} = ∥ f ∥_{2} > 0$ . Substituting $y = x + a$ gives $\int ∣ x ∣^{2} ∣ g (x) ∣^{2} d x = \int ∣ y - a ∣^{2} ∣ f (y) ∣^{2} d y \leq 2 \int ∣ y ∣^{2} ∣ f (y) ∣^{2} d y + 2 ∣ a ∣^{2} ∥ f ∥_{2}^{2} < \infty .$ Also $\int ∣ x_{j} ∣ ∣ g (x) ∣^{2} d x < \infty$ by Cauchy--Schwarz from $g, x_{j} g \in L^{2}$ . Thus the spatial mean and variance of $g$ are defined; frequency-side finiteness is established in the frequency computation below.

2.1F2givenstep 1.1

Spatial side. Substituting $y = x + a$ and using $∣ g (x) ∣^{2} = ∣ f (x + a) ∣^{2}$ [F2] gives, for each $j$ , $\int x_{j} ∣ g (x) ∣^{2} d x = \int y_{j} ∣ f (y) ∣^{2} d y - a_{j} \int ∣ f (y) ∣^{2} d y = ∥ f ∥_{2}^{2} a_{j} - ∥ f ∥_{2}^{2} a_{j} = 0, \int x_{j}^{2} ∣ g (x) ∣^{2} d x = \int (y_{j} - a_{j})^{2} ∣ f (y) ∣^{2} d y .$ Hence the spatial mean of $g$ is $0$ , $∥ x_{j} g ∥_{2} = ∥ (x_{j} - a_{j}) f ∥_{2}$ , and $V_{x} (g) = ∥ g ∥_{2}^{- 2} \int ∣ x ∣^{2} ∣ g ∣^{2} = ∥ f ∥_{2}^{- 2} \int ∣ y - a ∣^{2} ∣ f (y) ∣^{2} d y = V_{x} (f)$ .

2.2F1F2F3F4F5givenstep 1.1

Frequency side. Choose $f_{k} \in S$ with $f_{k} \to f$ in $L^{2}$ , using [F4] and countable choice [F1], and set $g_{k} = M_{- b} (τ_{- a} f_{k})$ . By [F4], $f_{k} \in L^{1} \cap L^{2}$ ; [F2] shows translation and modulation preserve both spaces and their norms, so $g_{k} \in L^{1} \cap L^{2}$ . Translation and modulation preserve $L^{2}$ distances, hence $g_{k} \to g$ in $L^{2}$ ; Plancherel gives $F_{2} f_{k} \to F_{2} f$ and $F_{2} g_{k} \to F_{2} g$ . By [F3], for each $k$ the integral transforms satisfy ${\hat{g}}_{k} (ξ) = e^{2 π i a \cdot (ξ + b)} {\hat{f}}_{k} (ξ + b)$ , and [F4] identifies these transforms with their Plancherel classes. Translation and multiplication by this unit-modulus phase are isometries on $L^{2}$ by [F2], so passing to the norm limits proves the Plancherel-class identity $\hat{g} (ξ) = e^{2 π i a \cdot (ξ + b)} \hat{f} (ξ + b)$ almost everywhere. First, the affine change of variables $η = ξ + b$ gives $\int ∣ ξ ∣^{2} ∣ \hat{g} (ξ) ∣^{2} d ξ = \int ∣ η - b ∣^{2} ∣ \hat{f} (η) ∣^{2} d η < \infty,$ so the first moments are absolutely integrable by Cauchy--Schwarz. Using [F5] for representatives, the same substitution now yields $\int ξ_{j} ∣ \hat{g} (ξ) ∣^{2} d ξ = \int (η_{j} - b_{j}) ∣ \hat{f} (η) ∣^{2} d η = ∥ f ∥_{2}^{2} b_{j} - ∥ f ∥_{2}^{2} b_{j} = 0, \int ξ_{j}^{2} ∣ \hat{g} (ξ) ∣^{2} d ξ = \int (η_{j} - b_{j})^{2} ∣ \hat{f} (η) ∣^{2} d η .$ Thus $g$ has finite frequency second moments and mean $0$ , $∥ ξ_{j} \hat{g} ∥_{2} = ∥ (ξ_{j} - b_{j}) \hat{f} ∥_{2}$ , and $V_{ξ} (g) = ∥ \hat{g} ∥_{2}^{- 2} \int ∣ ξ ∣^{2} ∣ \hat{g} ∣^{2} = ∥ \hat{f} ∥_{2}^{- 2} \int ∣ η - b ∣^{2} ∣ \hat{f} (η) ∣^{2} d η = V_{ξ} (f)$ ; Plancherel and the unitary covariance give $∥ \hat{g} ∥_{2} = ∥ g ∥_{2} = ∥ f ∥_{2} = ∥ \hat{f} ∥_{2}$ .

3.1step 2.1step 2.2∎

Conclusion. Steps 2.1 and 2.2 give $V_{x} (g) = V_{x} (f)$ , $V_{ξ} (g) = V_{ξ} (f)$ and hence $V_{x} (g) V_{ξ} (g) = V_{x} (f) V_{ξ} (f)$ , and both centred means vanish.

Depends on

Used by

The sharp Heisenberg theorem is owned by functional analysis Remark

Dependency tree · two levels

48 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)
Richard S. Laugesen, Harmonic Analysis Lecture Notes (arXiv:0903.3845) (standard reference, not scraped)