1. Physlib
  2. QuantumMechanics
  3. Operators
  4. Uncertainty
Imports
/- Copyright (c) 2026 Axiomatic-AI. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina -/ module public import Physlib.QuantumMechanics.Operators.Covariance

Uncertainty bounds for partial linear maps

i. Overview

In this module we prove abstract Robertson and Robertson–Schrödinger uncertainty bounds for symmetric partial linear maps on a complex inner product space. The statements are independent of any concrete position or momentum operator.

The centered-commutator results use only the domain assumptions needed to form the centered vectors. The raw-commutator results add the second-order domain hypotheses required to apply A to Bψ and B to Aψ.

ii. Key results

    inner_im_of_commutator_eq : an anti-Hermitian commutator identity fixes the imaginary part of an inner product.

    centeredCommutatorExpectation : the scalar commutator of the centered vectors.

    rawCommutatorExpectation : the expectation of the raw commutator on a state.

    inner_centered_commutator_of_raw_commutator : a raw commutator expectation gives the centered commutator expectation.

    state_uncertainty_squared_of_centered_commutator : the Robertson squared bound from a centered commutator identity.

    state_uncertainty_squared_with_covariance_of_centered_commutator : the strengthened Robertson–Schrödinger bound.

    state_uncertainty_of_centered_commutator : the standard-deviation form of the bound.

    state_uncertainty_squared_of_raw_commutator, state_uncertainty_squared_with_covariance_of_raw_commutator, and state_uncertainty_of_raw_commutator : variants using a raw commutator expectation.

iii. Table of contents

    A. Inner product lemmas

    B. Centered commutator bounds

    C. Raw commutator bounds

iv. References

    [H. P. Robertson, The Uncertainty Principle (1929)][robertson1929uncertainty].

    [E. Schrodinger, Zum Heisenbergschen Unscharfeprinzip (1930)][schrodinger1930heisenberg].

    [B. C. Hall, Quantum Theory for Mathematicians, Chapter 12][hall2013quantum].

@[expose] public section

A. Inner product lemmas

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hu:Hv:Hc:ℝh_comm:⟪u, v⟫_ℂ - ⟪v, u⟫_ℂ = Complex.I * ↑ch_conj_im:(⟪v, u⟫_ℂ).im = -(⟪u, v⟫_ℂ).imh_im:(⟪u, v⟫_ℂ).im - -(⟪u, v⟫_ℂ).im = c⊢ (⟪u, v⟫_ℂ).im = c / 2 All goals completed! 🐙H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hu:Hv:Hc:ℝh_comm:⟪u, v⟫_ℂ - ⟪v, u⟫_ℂ = Complex.I * ↑c⊢ (⟪u, v⟫_ℂ).re * (⟪u, v⟫_ℂ).re + c / 2 * (c / 2) = (⟪u, v⟫_ℂ).re ^ 2 + (c / 2) ^ 2 All goals completed! 🐙H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hψ:Ha:Hb:Hμa:ℝμb:ℝhμa_right:⟪ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ψ⟫_ℂ = ↑μahμb_right:⟪ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ψ⟫_ℂ = ↑μbhψ_norm:‖ψ‖ = 1⊢ ⟪a, b⟫_ℂ - ↑μb * ↑μa - star ↑μa * ↑μb + star ↑μa * ↑μb * ↑1 ^ 2 - (⟪b, a⟫_ℂ - ↑μa * ↑μb - star ↑μb * ↑μa + star ↑μb * ↑μa * ↑1 ^ 2) = ⟪a, b⟫_ℂ - ⟪b, a⟫_ℂ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hψ:Ha:Hb:Hμa:ℝμb:ℝhμa_right:⟪ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ψ⟫_ℂ = ↑μahμb_right:⟪ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ψ⟫_ℂ = ↑μbhψ_norm:‖ψ‖ = 1⊢ ⟪a, b⟫_ℂ - ↑μa * ↑μb - ↑μa * ↑μb + ↑μa * (↑μb * (↑1 * ↑1)) - (⟪b, a⟫_ℂ - ↑μa * ↑μb - ↑μa * ↑μb + ↑μa * (↑μb * (↑1 * ↑1))) = ⟪a, b⟫_ℂ - ⟪b, a⟫_ℂ All goals completed! 🐙All goals completed! 🐙 _ = Complex.I * c := h_raw

The scalar commutator of the centered vectors of A and B in the state ψ.

def centeredCommutatorExpectation (A B : H →ₗ.[ℂ] H) (ψ : A.domain) (hψB : (ψ : H) ∈ B.domain) : ℂ := ⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ - ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ

The expectation of the raw commutator [A, B] in the state ψ, with explicit second-order domain witnesses.

def rawCommutatorExpectation (A B : H →ₗ.[ℂ] H) (ψ : A.domain) (hψB : (ψ : H) ∈ B.domain) (hBA : A ψ ∈ B.domain) (hAB : B ⟨ψ, hψB⟩ ∈ A.domain) : ℂ := ⟪(ψ : H), A ⟨B ⟨ψ, hψB⟩, hAB⟩ - B ⟨A ψ, hBA⟩⟫_ℂ
H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ Hu:Hv:Hc:ℝh_comm:⟪u, v⟫_ℂ - ⟪v, u⟫_ℂ = Complex.I * ↑ch_sq:|c / 2| ^ 2 ≤ (‖u‖ * ‖v‖) ^ 2⊢ (|c| / 2) ^ 2 ≤ (‖u‖ * ‖v‖) ^ 2 All goals completed! 🐙x:ℝy:ℝz:ℝhx:0 ≤ xhz:0 ≤ zhxy:z ^ 2 ≤ x * yhs:z ≤ √x * √y⊢ z ≤ √x * √y All goals completed! 🐙

B. Centered commutator bounds

include h_centered

A centered commutator identity implies the squared Robertson uncertainty bound.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c⊢ (|c| / 2) ^ 2 ≤ (‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖) ^ 2 exact commutator_half_sq_le_mul_norm_sq (H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c⊢ ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ - ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = Complex.I * ↑c All goals completed! 🐙)

A centered commutator identity implies the Robertson–Schrödinger uncertainty bound.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c⊢ A.covariance B ψ hψB ^ 2 + (c / 2) ^ 2 = (⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ).re ^ 2 + (c / 2) ^ 2 All goals completed! 🐙 _ ≤ (‖centered A ψ‖ * ‖centered B ⟨ψ, hψB⟩‖) ^ 2 := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c⊢ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ^ 2 ≤ (‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖) ^ 2 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑ch_bound:‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ≤ ‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖⊢ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ^ 2 ≤ (‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖) ^ 2 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑ch_bound:‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ≤ ‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖h_inner_nonneg:0 ≤ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖⊢ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ^ 2 ≤ (‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖) ^ 2 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑ch_bound:‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ≤ ‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖h_inner_nonneg:0 ≤ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖h_mul_nonneg:0 ≤ ‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖⊢ ‖⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ‖ ^ 2 ≤ (‖A.centered ψ‖ * ‖B.centered ⟨↑ψ, hψB⟩‖) ^ 2 All goals completed! 🐙

A centered commutator identity implies the standard uncertainty bound.

lemma state_uncertainty_of_centered_commutator : |c| / 2 ≤ standardDeviation A ψ * standardDeviation B ⟨ψ, hψB⟩ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c⊢ |c| / 2 ≤ A.standardDeviation ψ * B.standardDeviation ⟨↑ψ, hψB⟩ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑ch_sq:(|c| / 2) ^ 2 ≤ A.variance ψ * B.variance ⟨↑ψ, hψB⟩⊢ |c| / 2 ≤ A.standardDeviation ψ * B.standardDeviation ⟨↑ψ, hψB⟩ refine sqrt_mul_le_of_sq_le (variance_nonneg A ψ) (H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] Hψ:↥A.domainhψB:↑ψ ∈ B.domainc:ℝh_centered:A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑ch_sq:(|c| / 2) ^ 2 ≤ A.variance ψ * B.variance ⟨↑ψ, hψB⟩⊢ 0 ≤ |c| / 2 All goals completed! 🐙) ?_ All goals completed! 🐙

C. Raw commutator bounds

include hA hB hψ_norm hBA hAB h_raw

A raw commutator expectation determines the centered commutator expectation.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] HhA:A.IsSymmetrichB:B.IsSymmetricψ:↥A.domainhψB:↑ψ ∈ B.domainhψ_norm:‖↑ψ‖ = 1hBA:↑A ψ ∈ B.domainhAB:↑B ⟨↑ψ, hψB⟩ ∈ A.domainc:ℝh_raw:A.rawCommutatorExpectation B ψ hψB hBA hAB = Complex.I * ↑ca:H := ↑A ψb:H := ↑B ⟨↑ψ, hψB⟩μa:ℝ := A.expectedValue ψμb:ℝ := B.expectedValue ⟨↑ψ, hψB⟩hμa_right:⟪↑ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ↑ψ⟫_ℂ = ↑μahμb_right:⟪↑ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ↑ψ⟫_ℂ = ↑μb⊢ A.centeredCommutatorExpectation B ψ hψB = Complex.I * ↑c calc centeredCommutatorExpectation A B ψ hψB = ⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ - ⟪centered B ⟨ψ, hψB⟩, centered A ψ⟫_ℂ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] HhA:A.IsSymmetrichB:B.IsSymmetricψ:↥A.domainhψB:↑ψ ∈ B.domainhψ_norm:‖↑ψ‖ = 1hBA:↑A ψ ∈ B.domainhAB:↑B ⟨↑ψ, hψB⟩ ∈ A.domainc:ℝh_raw:A.rawCommutatorExpectation B ψ hψB hBA hAB = Complex.I * ↑ca:H := ↑A ψb:H := ↑B ⟨↑ψ, hψB⟩μa:ℝ := A.expectedValue ψμb:ℝ := B.expectedValue ⟨↑ψ, hψB⟩hμa_right:⟪↑ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ↑ψ⟫_ℂ = ↑μahμb_right:⟪↑ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ↑ψ⟫_ℂ = ↑μb⊢ A.centeredCommutatorExpectation B ψ hψB = ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ - ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ All goals completed! 🐙 _ = ⟪a - (μa : ℂ) • (ψ : H), b - (μb : ℂ) • (ψ : H)⟫_ℂ - ⟪b - (μb : ℂ) • (ψ : H), a - (μa : ℂ) • (ψ : H)⟫_ℂ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] HhA:A.IsSymmetrichB:B.IsSymmetricψ:↥A.domainhψB:↑ψ ∈ B.domainhψ_norm:‖↑ψ‖ = 1hBA:↑A ψ ∈ B.domainhAB:↑B ⟨↑ψ, hψB⟩ ∈ A.domainc:ℝh_raw:A.rawCommutatorExpectation B ψ hψB hBA hAB = Complex.I * ↑ca:H := ↑A ψb:H := ↑B ⟨↑ψ, hψB⟩μa:ℝ := A.expectedValue ψμb:ℝ := B.expectedValue ⟨↑ψ, hψB⟩hμa_right:⟪↑ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ↑ψ⟫_ℂ = ↑μahμb_right:⟪↑ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ↑ψ⟫_ℂ = ↑μb⊢ ⟪A.centered ψ, B.centered ⟨↑ψ, hψB⟩⟫_ℂ - ⟪B.centered ⟨↑ψ, hψB⟩, A.centered ψ⟫_ℂ = ⟪a - ↑μa • ↑ψ, b - ↑μb • ↑ψ⟫_ℂ - ⟪b - ↑μb • ↑ψ, a - ↑μa • ↑ψ⟫_ℂ All goals completed! 🐙 _ = ⟪a, b⟫_ℂ - ⟪b, a⟫_ℂ := sub_expectation_commutator_eq_raw (ψ : H) a b μa μb hμa_right hμa_left hμb_right hμb_left hψ_norm _ = Complex.I * c := raw_commutator_eq_of_symmetric A B hA hB ψ hψB hBA hAB (H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HA:H →ₗ.[ℂ] HB:H →ₗ.[ℂ] HhA:A.IsSymmetrichB:B.IsSymmetricψ:↥A.domainhψB:↑ψ ∈ B.domainhψ_norm:‖↑ψ‖ = 1hBA:↑A ψ ∈ B.domainhAB:↑B ⟨↑ψ, hψB⟩ ∈ A.domainc:ℝh_raw:A.rawCommutatorExpectation B ψ hψB hBA hAB = Complex.I * ↑ca:H := ↑A ψb:H := ↑B ⟨↑ψ, hψB⟩μa:ℝ := A.expectedValue ψμb:ℝ := B.expectedValue ⟨↑ψ, hψB⟩hμa_right:⟪↑ψ, a⟫_ℂ = ↑μahμa_left:⟪a, ↑ψ⟫_ℂ = ↑μahμb_right:⟪↑ψ, b⟫_ℂ = ↑μbhμb_left:⟪b, ↑ψ⟫_ℂ = ↑μb⊢ ⟪↑ψ, ↑A ⟨↑B ⟨↑ψ, hψB⟩, hAB⟩ - ↑B ⟨↑A ψ, hBA⟩⟫_ℂ = Complex.I * ↑c All goals completed! 🐙)

A raw commutator expectation implies the squared Robertson uncertainty bound.

lemma state_uncertainty_squared_of_raw_commutator : (|c| / 2) ^ 2 ≤ variance A ψ * variance B ⟨ψ, hψB⟩ := state_uncertainty_squared_of_centered_commutator A B ψ hψB (inner_centered_commutator_of_raw_commutator A B hA hB ψ hψB hψ_norm hBA hAB h_raw)

A raw commutator expectation implies the squared uncertainty bound with covariance term.

lemma state_uncertainty_squared_with_covariance_of_raw_commutator : (covariance A B ψ hψB) ^ 2 + (c / 2) ^ 2 ≤ variance A ψ * variance B ⟨ψ, hψB⟩ := state_uncertainty_squared_with_covariance_of_centered_commutator A B ψ hψB (inner_centered_commutator_of_raw_commutator A B hA hB ψ hψB hψ_norm hBA hAB h_raw)

A raw commutator expectation implies the standard uncertainty bound.

lemma state_uncertainty_of_raw_commutator : |c| / 2 ≤ standardDeviation A ψ * standardDeviation B ⟨ψ, hψB⟩ := state_uncertainty_of_centered_commutator A B ψ hψB (inner_centered_commutator_of_raw_commutator A B hA hB ψ hψB hψ_norm hBA hAB h_raw)