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

Covariance-refined preparation uncertainty without operator products

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space with inner product linear in the first argument (Real and complex inner product spaces, with the inner product linear in the first argument, Hilbert space), let $A, B$ be symmetric densely defined operators on $H$ (Symmetric, self-adjoint and essentially self-adjoint operators, Adjoint of a densely defined operator), and let $u \in D (A) \cap D (B)$ satisfy $∥ u ∥ = 1$ . Put $a : = ⟨ A u, u ⟩, b : = ⟨ B u, u ⟩, x : = (A - a) u, y : = (B - b) u, Δ A : = ∥ x ∥, Δ B : = ∥ y ∥,$ and define the covariance of the pair $(A, B)$ in the preparation $u$ by ${Cov}_{u} (A, B) : = Re ⟨ x, y ⟩$ . Then:

(a) $a, b \in R$ ; $x, y \in H$ ; and ${Cov}_{u} (A, B) \in R$ is symmetric in its two arguments: ${Cov}_{u} (A, B) = {Cov}_{u} (B, A)$ ;

(b) covariance-refined bound: $(Δ A)^{2} (Δ B)^{2} \geq [{Cov}_{u} (A, B)]^{2} + [Im ⟨ x, y ⟩]^{2} \geq [{Cov}_{u} (A, B)]^{2},$ so in particular $Δ A Δ B \geq ∣ {Cov}_{u} (A, B) ∣$ ;

(c) equality holds in (b)'s first inequality if and only if $x$ and $y$ are linearly dependent (in the convention that $x = 0$ or $y = 0$ counts as dependence);

(d) if in addition $u \in D (A B) \cap D (B A)$ — that is $B u \in D (A)$ and $A u \in D (B)$ — then the pairing $⟨ [A, B] u, u ⟩ : = ⟨ A B u, u ⟩ - ⟨ B A u, u ⟩$ is defined and $⟨ [A, B] u, u ⟩ = - 2 i Im ⟨ x, y ⟩,$ in particular it is purely imaginary, and consequently $(Δ A)^{2} (Δ B)^{2} \geq [{Cov}_{u} (A, B)]^{2} + \frac{1}{4} ∣ ⟨ [A, B] u, u ⟩ ∣^{2}, Δ A Δ B \geq \frac{1}{2} ∣ ⟨ [A, B] u, u ⟩ ∣ .$

Clauses (a)-(c) use no product $A B$ or $B A$ and no assumption on the domains of such products. The quantities are preparation quantities of the vector $u$ ; no measurement model, apparatus error or energy-time interpretation is asserted.

Facts & Assumptions

Given: symmetric densely defined $A, B$ on a complex Hilbert space $H$ , a unit vector $u \in D (A) \cap D (B)$ , the numbers $a, b$ , vectors $x, y$ and $Δ A, Δ B$ .

[F1]

$(T - λ) v \in H$ for $T$ symmetric, $v \in D (T)$ , $λ \in R$ ; and $⟨ T v, v ⟩ = \overline{⟨ T v, v ⟩}$ , so the mean of a symmetric operator in any vector of its domain is real (Symmetric, self-adjoint and essentially self-adjoint operators, Adjoint of a densely defined operator).

[F2]

Cauchy–Schwarz in a complex inner product space: $∣ ⟨ v, w ⟩ ∣ \leq ∥ v ∥ ∥ w ∥$ , with equality if and only if $v, w$ are linearly dependent; 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).

[F3]

The weak-form Robertson lemma of Weak-form Robertson uncertainty on a common domain states in clause (b) exactly the inequality $(Δ A)^{2} (Δ B)^{2} \geq [Re ⟨ x, y ⟩]^{2} + [Im ⟨ x, y ⟩]^{2}$ for the present data; it is recorded here for comparison, and is derived below from [F2] without operator products.

[F4]

If $v, w \in H$ then $⟨ w, v ⟩ = \overline{⟨ v, w ⟩}$ , hence $Re ⟨ w, v ⟩ = Re ⟨ v, w ⟩$ .

Proof

1.1givenF1F4

[Means, centered vectors and covariance] By [F1], $a$ and $b$ are real, so $x = (A - a) u$ and $y = (B - b) u$ are well-defined vectors of $H$ (the sums $(A - a) u = A u - a u$ lie in $H$ because $A u, B u \in H$ and $a, b$ are scalars). By [F4], ${Cov}_{u} (B, A) = Re ⟨ y, x ⟩ = Re ⟨ x, y ⟩ = {Cov}_{u} (A, B)$ , which is real by definition. This is (a).

1.2givenF2F3algebra

[The refined bound] Apply [F2] to $x, y$ : $Δ A Δ B = ∥ x ∥ ∥ y ∥ \geq ∣ ⟨ x, y ⟩ ∣$ , and [F2] again gives $∣ ⟨ x, y ⟩ ∣^{2} = (Re ⟨ x, y ⟩)^{2} + (Im ⟨ x, y ⟩)^{2} = {Cov}_{u} (A, B)^{2} + (Im ⟨ x, y ⟩)^{2}$ . Squaring the first inequality and substituting the second gives $(Δ A)^{2} (Δ B)^{2} \geq ∣ ⟨ x, y ⟩ ∣^{2} \geq {Cov}_{u} (A, B)^{2}$ , which is (b) and reproduces [F3] without any operator product.

2.1givenF2step 1.2algebra

[Equality case] Equality holds in $(Δ A)^{2} (Δ B)^{2} \geq [{Cov}_{u} (A, B)]^{2} + [Im ⟨ x, y ⟩]^{2}$ exactly when equality holds in $∥ x ∥ ∥ y ∥ \geq ∣ ⟨ x, y ⟩ ∣$ , since the second step $∣ ⟨ x, y ⟩ ∣^{2} \geq (Re ⟨ x, y ⟩)^{2}$ is an identity with $[Im ⟨ x, y ⟩]^{2}$ added, i.e. it is always an equality. By [F2] that holds exactly for linearly dependent $x, y$ . This is (c).

3.1givenstep 1.2F1F4algebra∎

[Commutator pairing] Assume $u \in D (A B) \cap D (B A)$ . Then $B u \in D (A)$ and $A u \in D (B)$ , so both $⟨ A B u, u ⟩ = ⟨ B u, A u ⟩$ (symmetry of $A$ applied to $B u \in D (A)$ and $u$ ) and $⟨ B A u, u ⟩ = ⟨ A u, B u ⟩$ (symmetry of $B$ ) are defined. Writing $z : = ⟨ x, y ⟩$ , the computation $z = ⟨ A u, B u ⟩ - a b - a b + a b = ⟨ A u, B u ⟩ - a b$ with real $a, b$ gives $\overline{z} = ⟨ B u, A u ⟩ - a b$ by [F4]. Hence $⟨ [A, B] u, u ⟩ = (\overline{z} + a b) - (z + a b) = \overline{z} - z = - 2 i Im z = - 2 i Im ⟨ x, y ⟩$ , which is purely imaginary. Substituting into (b) gives $(Δ A)^{2} (Δ B)^{2} \geq {Cov}_{u} (A, B)^{2} + \frac{1}{4} ∣ ⟨ [A, B] u, u ⟩ ∣^{2}$ and, taking square roots, $Δ A Δ B \geq \frac{1}{2} ∣ ⟨ [A, B] u, u ⟩ ∣$ . This is (d).

Covariance-refined preparation uncertainty without operator products

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources