LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Weak-form Robertson uncertainty on a common domain

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space (Hilbert space) and let $A, B$ be symmetric densely defined operators on $H$ (Symmetric, self-adjoint and essentially self-adjoint operators, Adjoint of a densely defined operator). Let $u \in D (A) \cap D (B)$ have $∥ u ∥ = 1$ , and put

$a : = ⟨ A u, u ⟩, b : = ⟨ B u, u ⟩, x : = (A - a) u, y : = (B - b) u, Δ A : = ∥ x ∥, Δ B : = ∥ y ∥ .$

Then:

(a) $a$ and $b$ are real, $x, y \in H$ , and $Δ A Δ B \geq ∣ ⟨ x, y ⟩ ∣ \geq ∣ Im ⟨ x, y ⟩ ∣$ ;

(b) (refined form) $(Δ A)^{2} (Δ B)^{2} \geq [Re ⟨ x, y ⟩]^{2} + [Im ⟨ x, y ⟩]^{2}$ ;

(c) if in addition $u \in D (A B) \cap D (B A)$ , then $([A, B] u, u) = ⟨ A B u, u ⟩ - ⟨ B A u, u ⟩ = - 2 i Im ⟨ A u, B u ⟩ = - 2 i Im ⟨ x, y ⟩$ , and consequently $Δ A Δ B \geq \frac{1}{2} ∣ ([A, B] u, u) ∣$ ;

(d) for $c > 0$ , $H = L^{2} (R)$ and the operators $Q f (x) = x f (x)$ , $P f (x) = - i c f^{'} (x)$ defined on the Schwartz space $S (R)$ : every unit $f \in S (R)$ satisfies $(Q P - P Q) f = i c f$ , the numbers $a_{Q} = \int_{R} x ∣ f (x) ∣^{2} d x$ and $b_{P} = ⟨ P f, f ⟩$ are real, and with $x_{Q} : = (Q - a_{Q}) f$ , $y_{P} : = (P - b_{P}) f$ one has $∣ Im ⟨ x_{Q}, y_{P} ⟩ ∣ = c / 2$ ; hence $Δ Q Δ P \geq c / 2$ in the sense of the centered norms.

No assertion is made about products $A B$ off $D (A B)$ and the statement produces no energy-time inequality.

Facts & Assumptions

Given: A complex Hilbert space $H$ with pairing linear in the first argument; symmetric densely defined $A, B$ ; a unit vector $u \in D (A) \cap D (B)$ ; in clause (d) the operators $Q, P$ on $S (R)$ .

[F1]

For a symmetric operator $T$ (so $T \subseteq T^{*}$ ) and $v \in D (T)$ , $⟨ T v, v ⟩ = ⟨ v, T v ⟩ = \overline{⟨ T v, v ⟩}$ , so the number is real (Symmetric, self-adjoint and essentially self-adjoint operators, Adjoint of a densely defined operator).

[F2]

If $T$ is symmetric and $v \in D (T)$ , then $(T - λ) v \in H$ for every real $λ$ ; and $∥ (T - λ) v ∥^{2} = ∥ T v ∥^{2} - 2 λ Re ⟨ T v, v ⟩ + λ^{2} ∥ v ∥^{2}$ , so centering by the real mean $λ = ⟨ T v, v ⟩$ is legitimate (Symmetric, self-adjoint and essentially self-adjoint operators).

[F3]

In a complex inner product space, $∣ ⟨ v, w ⟩ ∣ \leq ∥ v ∥ ∥ w ∥$ and $∣ ⟨ v, w ⟩ ∣^{2} = (Re ⟨ v, w ⟩)^{2} + (Im ⟨ v, w ⟩)^{2}$ (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

[F4]

$S (R)$ consists of $C^{\infty}$ complex functions all of whose polynomial-weighted derivatives are bounded; in particular $f, f^{'}, x f, x f^{'} \in L^{2} (R)$ and $x f (x) \overline{f (x)} \to 0$ as $x \to \pm \infty$ for every $f \in S (R)$ (Schwartz space and its seminorms).

[F5]

Sums, scalar multiples and products of differentiable real functions satisfy $(f g)^{'} = f^{'} g + f g^{'}$ , and the derivative of a complex-valued differentiable function is computed componentwise (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F6]

For differentiable real $u, v$ on $[a, b]$ with integrable derivatives, $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ); a continuous real function on an interval has a primitive and $\int_{a}^{b} G^{'} = G (b) - G (a)$ for it (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ); the improper integral over an unbounded interval is the limit of the compact-interval integrals (Improper integrals over unbounded intervals).

Proof

1.1givenF1F2algebra

[Reality of the means] By [F1] applied to $T = A$ and $T = B$ , $a = ⟨ A u, u ⟩$ and $b = ⟨ B u, u ⟩$ are real. Hence $x = A u - a u \in H$ and $y = B u - b u \in H$ , and $Δ A = ∥ x ∥$ , $Δ B = ∥ y ∥$ are the norms of the centered vectors; the centering by the real means is the construction recorded in [F2].

1.2givenF4F5F6algebra

[Boundary-vanishing pairing identity on the Schwartz space] Let $f, g \in S (R)$ . Applying [F6] on $[- R, R]$ to the real and imaginary parts of $f$ and $\overline{g}$ and summing the four identities gives $\int_{- R}^{R} f^{'} \overline{g} = [f \overline{g}]_{- R}^{R} - \int_{- R}^{R} f \overline{g^{'}}$ ; by [F4] the boundary term $f (R) \overline{g} (R) - f (- R) \overline{g} (- R)$ tends to $0$ as $R \to \infty$ , while both improper integrals converge absolutely because $f^{'} \overline{g}$ and $f \overline{g^{'}}$ are products of Schwartz functions; taking the limit in [F6]'s finite identity therefore gives $\int_{R} f^{'} \overline{g} = - \int_{R} f \overline{g^{'}}$ .

2.1step 1.1F3algebra

[Cauchy-Schwarz bounds] By [F3], $Δ A Δ B = ∥ x ∥ ∥ y ∥ \geq ∣ ⟨ x, y ⟩ ∣$ , and $∣ ⟨ x, y ⟩ ∣ \geq ∣ Im ⟨ x, y ⟩ ∣$ ; squaring the first identity of [F3] gives $(Δ A)^{2} (Δ B)^{2} \geq (Re ⟨ x, y ⟩)^{2} + (Im ⟨ x, y ⟩)^{2}$ . This is (a) and (b).

2.2step 1.2F4F5F6algebra

[The position-momentum commutator] For $f \in S (R)$ the product rule [F5] applied componentwise gives $(x f)^{'} (x) = f (x) + x f^{'} (x)$ and hence $(Q P - P Q) f (x) = x (- i c f^{'} (x)) - (- i c) (f (x) + x f^{'} (x)) = i c f (x)$ , so $Q P - P Q = i c I$ on $S (R)$ . Moreover $\int_{R} (x ∣ f ∣^{2})^{'} (x) d x = 0$ : on $[- R, R]$ the evaluation clause of [F6] gives $\int_{- R}^{R} (x ∣ f ∣^{2})^{'} d x = x ∣ f ∣^{2} ∣_{- R}^{R}$ , which tends to $0$ by [F4], and $(x ∣ f ∣^{2})^{'} = ∣ f ∣^{2} + 2 Re (x f^{'} \overline{f})$ is continuous and dominated by an integrable Schwartz bound, so its improper integral over $R$ exists by [F6] and equals this limit. Expanding and using $\int_{R} ∣ f ∣^{2} = 1$ yields $\int_{R} x f^{'} \overline{f} d x + \int_{R} x f \overline{f^{'}} d x = - 1$ ; the second integral equals $\overline{\int_{R} x f^{'} \overline{f} d x}$ by complex conjugation, so $2 Re \int_{R} x f^{'} \overline{f} d x = - 1$ .

3.1step 1.1step 2.1algebra

[Commutator pairing] Assume $u \in D (A B) \cap D (B A)$ . Using symmetry of $A$ with $B u \in D (A)$ and symmetry of $B$ with $A u \in D (B)$ , $⟨ A B u, u ⟩ = ⟨ B u, A u ⟩$ and $⟨ B A u, u ⟩ = ⟨ A u, B u ⟩$ , so $([A, B] u, u) = ⟨ B u, A u ⟩ - ⟨ A u, B u ⟩ = \overline{⟨ A u, B u ⟩} - ⟨ A u, B u ⟩ = - 2 i Im ⟨ A u, B u ⟩$ . Since $a, b \in R$ , expanding $⟨ x, y ⟩ = ⟨ (A - a) u, (B - b) u ⟩$ gives $⟨ x, y ⟩ = ⟨ A u, B u ⟩ - a b$ and therefore $Im ⟨ x, y ⟩ = Im ⟨ A u, B u ⟩$ ; combining with step 2.1 gives $Δ A Δ B \geq \frac{1}{2} ∣ ([A, B] u, u) ∣$ .

4.1step 2.1step 2.2F4algebra∎

[The uncertainty product for the Schwartz pair] Let $f \in S (R)$ have $∥ f ∥ = 1$ and put $a_{Q} = \int_{R} x ∣ f ∣^{2} d x \in R$ , $b_{P} = ⟨ P f, f ⟩ = - i c \int_{R} f^{'} \overline{f} d x$ ; step 1.2 with $g = f$ gives $\int_{R} f^{'} \overline{f} = - \overline{\int_{R} f^{'} \overline{f}}$ , so this number is purely imaginary and $b_{P}$ is real. With $x_{Q} = (Q - a_{Q}) f$ and $y_{P} = (P - b_{P}) f$ , both in $L^{2} (R)$ by [F4], one computes $⟨ x_{Q}, y_{P} ⟩ = ⟨ Q f, P f ⟩ - a_{Q} b_{P}$ , using $⟨ Q f, f ⟩ = a_{Q}$ , $⟨ f, P f ⟩ = \overline{⟨ P f, f ⟩} = b_{P}$ and $∥ f ∥ = 1$ . Now $Im ⟨ Q f, P f ⟩$ : writing $w = \int_{R} x f \overline{f^{'}} d x$ and using $⟨ Q f, P f ⟩ = \int_{R} x f \overline{(- i c f^{'})} = i c w$ , and $w + \overline{w} = \int_{R} x (∣ f ∣^{2})^{'} = - 1$ from step 2.2, so $Re w = - \frac{1}{2}$ and $Im ⟨ Q f, P f ⟩ = c Re w = - \frac{c}{2}$ . Hence $∣ Im ⟨ x_{Q}, y_{P} ⟩ ∣ = c / 2$ , and the Cauchy-Schwarz computation of step 2.1 applied to the explicitly centered vectors $x_{Q}, y_{P}$ gives $Δ Q Δ P \geq c / 2$ .

Weak-form Robertson uncertainty on a common domain

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources