LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.

The momentum representation of the componentwise kinematics

Statement

Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice). Fix $d \geq 1$ , $r \geq 1$ and $ℏ > 0$ , let $H^{(r)} = L^{2} (R^{d}; C^{r})$ with the componentwise operators $Q_{j}, P_{k}$ of Componentwise position and momentum operators on the component-valued wave-function space, let $U$ be the unitary of Momentum Fourier Jacobian: the unitary momentum representation clause (c), which on Schwartz classes acts by $(U ψ) (p) = (2 π ℏ)^{- d / 2} \int_{R^{d}} e^{- i p \cdot x / ℏ} ψ (x) d x,$ and put $U^{(r)} : = Ψ_{0} (⨁_{l} U) Ψ_{0}^{- 1}$ with $Ψ_{0}$ as in Unitary identifications of the component-valued wave-function space. Then:

(a) $U^{(r)} : L^{2} (R^{d}, d x; C^{r}) \to L^{2} (R^{d}, d p; C^{r})$ is unitary; for $f = (f_{l}) \in S (R^{d}; C^{r})$ , $(U^{(r)} f)_{l} (p) = (2 π ℏ)^{- d / 2} \int_{R^{d}} e^{- i p \cdot x / ℏ} f_{l} (x) d x (l = 1, \dots, r),$ $U^{(r)} f \in S (R^{d}; C^{r})$ , and $\int_{R^{d}} ∥ U^{(r)} f (p) ∥_{C^{r}}^{2} d p = \int_{R^{d}} ∥ f (x) ∥_{C^{r}}^{2} d x$ ;

(b) $U^{(r)} D (P_{k}) = D (M_{p_{k}})$ , where $M_{p_{k}} g (p) : = p_{k} g (p)$ on $D (M_{p_{k}}) = {g \in L^{2} (d p; C^{r}) : p_{k} g \in L^{2}}$ , and $U^{(r)} P_{k} = M_{p_{k}} U^{(r)};$ equivalently $(U^{(r)} P_{k} f) (p) = p_{k} (U^{(r)} f) (p)$ for every $f \in D (P_{k})$ and almost every $p$ ;

(c) for every $f \in S (R^{d}; C^{r})$ and every $j$ , $U^{(r)} (Q_{j} f) (p) = i ℏ \frac{\partial}{\partial p_{j}} (U^{(r)} f) (p) (p \in R^{d}),$ and both sides are Schwartz classes; no identity of unbounded operators on the full domain of $Q_{j}$ is asserted;

(d) for every $a \in R^{d}$ , with $T_{a}^{(r)}$ the componentwise translation of Componentwise position and momentum operators on the component-valued wave-function space clause (c), $U^{(r)} T_{a}^{(r)} U^{(r) - 1} = M_{e^{- i a \cdot p / ℏ}},$ the bounded multiplication operator by the unimodular function $p \mapsto e^{- i a \cdot p / ℏ}$ ;

(e) under $Ψ_{0}$ the operator $U^{(r)}$ is the orthogonal sum $⨁_{l} U$ ; no physical identification of $U^{(r)} f$ with a measured momentum distribution is made by this lemma.

Facts & Assumptions

Given: The Axiom of Countable Choice and the Axiom of Choice; integers $d, r \geq 1$ ; $ℏ > 0$ ; the scalar unitary $U$ and its componentwise version $U^{(r)}$ ; the operators $Q_{j}, P_{k}$ and their scalar counterparts; a class $f = (f_{l})$ ; a vector $a \in R^{d}$ ; indices $j, k$ .

[F1]

The scalar momentum representation. $U$ is a unitary $L^{2} (R^{d}, d x) \to L^{2} (R^{d}, d p)$ with the displayed Schwartz formula; $U = D_{ℏ} F_{2}$ on Schwartz classes, where $D_{ℏ} g (p) = (2 π ℏ)^{- d / 2} g (p / (2 π ℏ))$ is a surjective isometry of $L^{2} (R^{d}; C)$ and $F_{2}$ is the unitary Plancherel transform of Plancherel theorem; and on Schwartz classes $U$ acts as the topological automorphism $D_{ℏ} F_{2}$ (Momentum Fourier Jacobian: the unitary momentum representation clauses (a)-(c), Fourier transform is a topological automorphism of Schwartz space).

[F2]

Scalar domains, Fourier representation and translations. $D (P_{k}^{(1)}) = {f : ξ_{k} F_{2} f \in L^{2}}$ and $F_{2} (P_{k}^{(1)} f) (ξ) = 2 π ℏ ξ_{k} F_{2} f (ξ)$ ; the scalar translations are unitary and satisfy $F_{2} (T_{a} f) (ξ) = e^{- 2 π i a \cdot ξ} F_{2} f (ξ)$ on $L^{1} \cap L^{2}$ , hence on $L^{2}$ by density and continuity (Self-adjointness, Fourier representation and translation identities of position and momentum clauses (b),(c), Fourier transform on complex L1 classes).

[F3]

Componentwise operators and identifications. $Ψ_{0}$ is unitary and $Q_{j}, P_{k}$ are its conjugates of the corresponding orthogonal sums; $F_{2}^{(r)}$ is unitary with the componentwise multiplication representation of $P_{k}$ ; the componentwise translations are the conjugates of $⨁_{l} T_{a}$ (Componentwise position and momentum operators on the component-valued wave-function space clauses (a)-(c), Unitary identifications of the component-valued wave-function space clauses (a),(c)).

[F4]

Differentiation under the integral. If for a parameter $p$ the integrand is differentiable with derivative dominated by an integrable function independent of the parameter, the derivative may be taken under the integral sign (Differentiation under the integral sign). Change of variables under a translation holds for integrable functions (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not). Tonelli's theorem for nonnegative measurable integrands (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F5]

Dense extension of bounded identities. If two bounded operators agree on a dense subspace, they agree everywhere (A bounded linear map from a dense normed subspace into a Banach space extends uniquely with the same norm).

Proof

technique · direct; reduce unitarity and the Schwartz formula to the scalar supplier through the orthogonal-sum identification, transport the momentum representation and its domain, differentiate the Schwartz transform under the integral for the core identity of position, and extend the translation conjugation by density

Given: The data of the statement and [F1]-[F5].

1.1F1F3algebra

[Unitarity, Schwartz formula and Plancherel identity] By [F3] and Finite orthogonal sums of self-adjoint operators and of bounded operators clause (c) the orthogonal sum $⨁_{l} U$ is unitary, hence so is its conjugate $U^{(r)}$ by the unitary $Ψ_{0}$ . On a Schwartz class $f = (f_{l})$ each component is a scalar Schwartz class, so [F1] gives $(U^{(r)} f)_{l} = U f_{l}$ with the displayed integral formula and $U f_{l} \in S (R^{d}; C)$ ; hence $U^{(r)} f \in S (R^{d}; C^{r})$ . The Plancherel identity is the componentwise scalar identity of [F1], summed over $l$ (finite sum) and read with the componentwise norms. This proves (a) and (e).

2.1step 1.1F1F2F3algebra

[Momentum domain and action] Let $f = (f_{l}) \in H^{(r)}$ . By [F2], for each $l$ one has $f_{l} \in D (P_{k}^{(1)})$ exactly when $ξ_{k} F_{2} f_{l} \in L^{2}$ , and then $F_{2} (P_{k}^{(1)} f_{l}) = 2 π ℏ ξ_{k} F_{2} f_{l}$ . Since $U = D_{ℏ} F_{2}$ and $p_{k} D_{ℏ} h = D_{ℏ} (2 π ℏ ξ_{k} h)$ pointwise for every $h \in L^{2}$ with $ξ_{k} h \in L^{2}$ , one gets $p_{k} U f_{l} = U (P_{k}^{(1)} f_{l})$ and, conversely, $p_{k} U f_{l} \in L^{2}$ exactly when $ξ_{k} F_{2} f_{l} \in L^{2}$ because $D_{ℏ}$ is an isometry; thus $U D (P_{k}^{(1)}) = D (M_{p_{k}})$ and $U P_{k}^{(1)} = M_{p_{k}} U$ . Assembling components through $Ψ_{0}$ [F3] gives $U^{(r)} D (P_{k}) = D (M_{p_{k}})$ and $U^{(r)} P_{k} = M_{p_{k}} U^{(r)}$ , which is (b).

2.2step 1.1F1F3F4algebra

[Position in the momentum representation] Let $f \in S (R^{d}; C^{r})$ and consider one component $f_{l} \in S (R^{d}; C)$ . For fixed $x$ , the $p_{j}$ -derivative of $e^{- i p \cdot x / ℏ} f_{l} (x)$ is $(- i / ℏ) x_{j} e^{- i p \cdot x / ℏ} f_{l} (x)$ . Its modulus is $∣ x_{j} f_{l} (x) ∣ / ℏ$ , an integrable bound independent of $p$ because $f_{l}$ is Schwartz; [F4] therefore permits differentiation under the integral, giving $\frac{\partial}{\partial p_{j}} (U f_{l}) (p) = (2 π ℏ)^{- d / 2} \int e^{- i p \cdot x / ℏ} (- \frac{i}{ℏ} x_{j}) f_{l} (x) d x = (- \frac{i}{ℏ}) (U (Q_{j}^{(1)} f_{l})) (p),$ that is $U (Q_{j}^{(1)} f_{l}) = i ℏ \partial_{p_{j}} (U f_{l})$ . Since $U f_{l} \in S$ by [F1], its partial derivative is again Schwartz (Schwartz space and its seminorms), and assembling components through [F3] proves (c).

3.1step 1.1F1F3F4F5algebra∎

[Translations] Let $f = (f_{l})$ be a Schwartz class and fix $a$ . For each component, the substitution $y = x - a$ and [F4] give $(U T_{a} f_{l}) (p) = (2 π ℏ)^{- d / 2} \int e^{- i p \cdot (x + a) / ℏ} f_{l} (x) d x = e^{- i a \cdot p / ℏ} (U f_{l}) (p)$ , so $U^{(r)} T_{a}^{(r)} = M_{e^{- i a \cdot p / ℏ}} U^{(r)}$ on the dense Schwartz subspace of $H^{(r)}$ ; both sides are bounded operators (products of unitaries, a translation and a unimodular multiplier), so [F5] extends the identity to all of $H^{(r)}$ and $U^{(r)} T_{a}^{(r)} U^{(r) - 1} = M_{e^{- i a \cdot p / ℏ}}$ , which is (d).

Remarks

What the momentum representative is. $U^{(r)} f$ is a class in $L^{2} (R^{d}, d p; C^{r})$ obtained from $f$ by the unitary transform of clause (a); the lemma makes no statement about measuring it, and the physical reading of $∥ U^{(r)} f (p) ∥^{2} d p$ as an outcome density is a separate consequence of the observable postulate, proved with the physics items of this page.
Core only for position. Clause (c) is asserted on Schwartz classes, where both sides are ordinary functions; no claim is made that the mapping $g \mapsto i ℏ \partial_{p_{j}} g$ with its maximal $L^{2}$ domain is the unitary conjugate of the full position operator.

The momentum representation of the componentwise kinematics

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources