Empirical/QM: Robertson uncertainty relation

Category: 3-Local (promotion-ready to 2-Framework on demand). QM-generic: no CSD ontology, pure inner-product geometry.

The Robertson uncertainty relation (Robertson 1929): for self-adjoint observables A, B and a state ψ,

Var_ψ(A) · Var_ψ(B) ≥ ¼ |⟨ψ, [A,B] ψ⟩|²,

where [A,B] = AB − BA is the commutator and Var_ψ(A) = ‖(A − ⟨A⟩)ψ‖² is the variance of the centered observable. The bound is the squared Cauchy–Schwarz inequality applied to the centered vectors (A−⟨A⟩)ψ, (B−⟨B⟩)ψ, retaining only the imaginary part of their inner product, which equals ½⟨ψ,[A,B]ψ⟩.

Operators are Module.End ℂ H = H →ₗ[ℂ] H; self-adjointness is LinearMap.IsSymmetric (the inner-product form ⟪T x, y⟫ = ⟪x, T y⟫), which sidesteps the Star synthesis issues noted in LF3. The proof needs no finite-dimensionality.

Source

Robertson 1929, Phys. Rev. 34, 163; Schrödinger 1930 (the stronger form with the anticommutator term, not formalised here).

noncomputable def CSD.Empirical.Uncertainty.expectation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : ℂ

Expectation value ⟨A⟩_ψ = ⟪ψ, A ψ⟫.

Equations

• CSD.Empirical.Uncertainty.expectation A ψ = inner ℂ ψ (A ψ)

noncomputable def CSD.Empirical.Uncertainty.variance {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : ℝ

Variance Var_ψ(A) = ‖(A − ⟨A⟩) ψ‖², the squared norm of the centered observable applied to ψ (the standard quantum variance for a unit ψ).

Equations

• CSD.Empirical.Uncertainty.variance A ψ = ‖A ψ - CSD.Empirical.Uncertainty.expectation A ψ • ψ‖ ^ 2

noncomputable def CSD.Empirical.Uncertainty.stdDev {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : ℝ

Standard deviation σ_ψ(A) = ‖(A − ⟨A⟩) ψ‖, the unsquared spread. variance is its square (variance_eq_stdDev_sq); the error–disturbance relation of Ozawa.lean is stated in unsquared quantities, which is why this lives beside variance rather than in that file.

Equations

• CSD.Empirical.Uncertainty.stdDev A ψ = ‖A ψ - CSD.Empirical.Uncertainty.expectation A ψ • ψ‖

theorem CSD.Empirical.Uncertainty.stdDev_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : 0 ≤ stdDev A ψ

theorem CSD.Empirical.Uncertainty.variance_eq_stdDev_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : variance A ψ = stdDev A ψ ^ 2

theorem CSD.Empirical.Uncertainty.expectation_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (hA : LinearMap.IsSymmetric A) (ψ : H) : (starRingEnd ℂ) (expectation A ψ) = expectation A ψ

For a symmetric operator the expectation value is real.

theorem CSD.Empirical.Uncertainty.isSymmetric_sub_smul_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {A : Module.End ℂ H} (hA : LinearMap.IsSymmetric A) {a : ℂ} (ha : (starRingEnd ℂ) a = a) : LinearMap.IsSymmetric (A - a • 1)

Subtracting a real scalar multiple of the identity preserves symmetry.

theorem CSD.Empirical.Uncertainty.commutator_shift {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A B : Module.End ℂ H) (a b : ℂ) : (A - a • 1) * (B - b • 1) - (B - b • 1) * (A - a • 1) = A * B - B * A

The commutator is invariant under shifting each operator by a scalar multiple of the identity: [A − a, B − b] = [A, B].

theorem CSD.Empirical.Uncertainty.variance_centered {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : Module.End ℂ H) (ψ : H) : variance A ψ = ‖(A - expectation A ψ • 1) ψ‖ ^ 2

Var_ψ(A) = ‖(A − ⟨A⟩•1) ψ‖² (variance via the centered operator).

theorem CSD.Empirical.Uncertainty.commutator_le_two_mul_norm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A B : Module.End ℂ H) (hA : LinearMap.IsSymmetric A) (hB : LinearMap.IsSymmetric B) (ψ : H) : ‖inner ℂ ψ ((A * B - B * A) ψ)‖ ≤ 2 * (‖A ψ‖ * ‖B ψ‖)

★ The commutator bound, unsquared. For symmetric A, B, ‖⟪ψ, [A,B] ψ⟫‖ ≤ 2 ‖A ψ‖ ‖B ψ‖.

Both robertson_core (by squaring) and Ozawa's error–disturbance relation (by summing three instances) are this inequality; the squared form cannot be summed, which is why the unsquared one is the primitive. The content is that ⟪ψ,[A,B]ψ⟫ = z − conj z = 2i·Im z for z = ⟪A ψ, B ψ⟫, so the commutator sees only the imaginary part, and |Im z| ≤ ‖z‖.

theorem CSD.Empirical.Uncertainty.robertson_core {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A B : Module.End ℂ H) (hA : LinearMap.IsSymmetric A) (hB : LinearMap.IsSymmetric B) (ψ : H) : ‖A ψ‖ ^ 2 * ‖B ψ‖ ^ 2 ≥ 1 / 4 * ‖inner ℂ ψ ((A * B - B * A) ψ)‖ ^ 2

Core inequality. For symmetric A, B and any ψ, ‖A ψ‖² · ‖B ψ‖² ≥ ¼ ‖⟪ψ, [A,B] ψ⟫‖². The uncertainty relation is this applied to the centered observables. Derived from the unsquared commutator_le_two_mul_norm by squaring (CONVENTIONS §9.3: one Cauchy–Schwarz, two consumers).

theorem CSD.Empirical.Uncertainty.robertson_uncertainty {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A B : Module.End ℂ H) (hA : LinearMap.IsSymmetric A) (hB : LinearMap.IsSymmetric B) (ψ : H) : variance A ψ * variance B ψ ≥ 1 / 4 * ‖inner ℂ ψ ((A * B - B * A) ψ)‖ ^ 2

Robertson uncertainty relation. For self-adjoint observables A, B and any state ψ, Var_ψ(A) · Var_ψ(B) ≥ ¼ ‖⟪ψ, [A,B] ψ⟫‖².