States, expectation, and uncertainty relations

Physlib.lean

@@ -341,6 +341,8 @@ public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic
 public import Physlib.QuantumMechanics.OperatorAlgebra.Basic
 public import Physlib.QuantumMechanics.OperatorAlgebra.Dynamics.Automorphism
 public import Physlib.QuantumMechanics.OperatorAlgebra.HilbertSpace
+public import Physlib.QuantumMechanics.OperatorAlgebra.Measurement.State
+public import Physlib.QuantumMechanics.OperatorAlgebra.Measurement.Uncertainty
 public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Jordan
 public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Lie
 public import Physlib.QuantumMechanics.Operators.AngularMomentum

Physlib/QuantumMechanics/OperatorAlgebra/Basic.lean

@@ -25,7 +25,8 @@ The basic notions of observable, positive element, effect, state, unitary, chann
 POVM depend only on the observable algebra.
 
 This file only defines the vocabulary. Elementary results about each notion live in their own
-file (`Observable.lean`, `Effect.lean`, `State.lean`, ...).
+file (e.g. `Measurement/State.lean` for states, `Observables/Jordan.lean` for the Jordan
+product, ...).
 
 -/
 
@@ -69,15 +70,6 @@ structure POVM (A : Type*) [OperatorAlgebra A] (X : Type*) [Fintype X] where
 or time evolution under a Hamiltonian — acting on observables by conjugation, `a ↦ U a U⋆`. -/
 noncomputable abbrev Unitary (A : Type*) [OperatorAlgebra A] := unitary A
 
-/-- A state on `A`: a positive complex-linear functional normalized by `ω 1 = 1`. `ω a` is the
-expected outcome of measuring observable `a` in this state — a state records everything that can
-be learned about the system by measurement. -/
-structure State (A : Type*) [OperatorAlgebra A] where
-  /-- The positive linear functional underlying the state. -/
-  toPositiveLinearMap : A →ₚ[ℂ] ℂ
-  /-- A state assigns expectation one to the identity observable. -/
-  map_one : toPositiveLinearMap 1 = 1
-
 /-- A channel from `A₁` to `A₂` — physicists' name for a unital completely positive (UCP) map,
 the most general notion of dynamics this framework expresses. -/
 abbrev Channel (A₁ A₂ : Type*) [OperatorAlgebra A₁] [OperatorAlgebra A₂] :=

Physlib/QuantumMechanics/OperatorAlgebra/Measurement/State.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Jordan
+public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Lie
+
+/-!
+
+# States
+
+A state on `A`: a positive complex-linear functional normalized by `ω 1 = 1`. `ω a` is the
+expected outcome of measuring observable `a` in this state — a state records everything that can
+be learned about the system by measurement.
+
+For an observable `a`, `ω⟨a⟩` denotes its real expectation value in the state
+`ω`. Subtracting this expectation centers the observable. Covariance is the
+expectation of the symmetrized product of two centered observables, and variance
+is covariance on the diagonal.
+
+More general measurement statistics are obtained by evaluating states on
+effects and POVMs.
+
+-/
+
+@[expose] public section
+
+open scoped ComplexOrder InnerProductSpace
+
+namespace OperatorAlgebra
+
+variable {A : Type*} [OperatorAlgebra A]
+
+/-- A state on `A`: a positive complex-linear functional normalized by `ω 1 = 1`. -/
+structure State (A : Type*) [OperatorAlgebra A] where
+  /-- The positive linear functional underlying the state. -/
+  toPositiveLinearMap : A →ₚ[ℂ] ℂ
+  /-- A state assigns expectation one to the identity observable. -/
+  map_one : toPositiveLinearMap 1 = 1
+
+noncomputable instance State.instCoeFun : CoeFun (State A) (fun _ => A → ℂ) where
+  coe ω := ω.toPositiveLinearMap
+
+namespace State
+
+/-! ## Expectation -/
+
+/-- The real expectation functional obtained by restricting a state to observables. -/
+noncomputable def expectation (ω : State A) : Observable A →ₗ[ℝ] ℝ where
+  toFun a := (ω.toPositiveLinearMap (a : A)).re
+  map_add' a b := by simp
+  map_smul' r a := by
+    rw [selfAdjoint.val_smul, PositiveLinearMap.map_smul_of_tower]
+    simp
+
+@[inherit_doc State.expectation]
+scoped[OperatorAlgebra] notation:max ω "⟨" a "⟩" => State.expectation ω a
+
+attribute [nolint docBlame] OperatorAlgebra.«term_⟨_⟩»
+
+lemma apply_observable_eq_expectation (ω : State A) (a : Observable A) :
+    ω (a : A) = (ω⟨a⟩ : ℂ) := by
+  apply Complex.ext
+  · rfl
+  · rw [Complex.ofReal_im]
+    have h : star (ω (a : A)) = ω (a : A) := by
+      rw [← map_star, a.property.star_eq]
+    exact Complex.conj_eq_iff_im.mp
+      (by simpa [Complex.star_def] using h)
+
+@[simp]
+lemma expectation_one (ω : State A) :
+    ω⟨(1 : Observable A)⟩ = 1 := by
+  simp [expectation, ω.map_one]
+
+/-- Positive observables have nonnegative expectation. -/
+lemma expectation_nonneg (ω : State A) {a : Observable A}
+    (ha : 0 ≤ (a : A)) :
+    0 ≤ ω⟨a⟩ :=
+  (Complex.le_def.mp (ω.toPositiveLinearMap.map_nonneg ha)).1
+
+/-! ## Centering -/
+
+/-- An observable with its expectation value subtracted. -/
+noncomputable def centered (ω : State A) (a : Observable A) : Observable A :=
+  a - ω⟨a⟩ • 1
+
+@[simp]
+lemma expectation_centered (ω : State A) (a : Observable A) :
+    ω⟨centered ω a⟩ = 0 := by
+  simp [centered]
+
+/-- Centering removes scalar multiples of the identity. -/
+@[simp]
+lemma centered_add_smul_one (ω : State A) (a : Observable A) (c : ℝ) :
+    centered ω (a + c • 1) = centered ω a := by
+  simp only [centered, map_add, map_smul, expectation_one]
+  module
+
+/-! ## Covariance and variance -/
+
+/-- Covariance is the expectation of the symmetrized product of centered observables. -/
+noncomputable def covariance (ω : State A) (a b : Observable A) : ℝ :=
+  ω⟨centered ω a ⊙ centered ω b⟩
+
+/-- Variance is covariance on the diagonal. -/
+noncomputable def variance (ω : State A) (a : Observable A) : ℝ :=
+  covariance ω a a
+
+@[simp]
+lemma covariance_self (ω : State A) (a : Observable A) :
+    covariance ω a a = variance ω a :=
+  rfl
+
+/-- Covariance is symmetric. -/
+lemma covariance_comm (ω : State A) (a b : Observable A) :
+    covariance ω a b = covariance ω b a := by
+  simp only [covariance]
+  rw [Observable.jordan_comm]
+
+/-- Adding a scalar multiple of the identity to the left observable does not change covariance. -/
+lemma covariance_add_smul_one_left (ω : State A) (a b : Observable A) (c : ℝ) :
+    covariance ω (a + c • 1) b = covariance ω a b := by
+  simp only [covariance, centered_add_smul_one]
+
+/-- Adding a scalar multiple of the identity to the right observable does not change covariance. -/
+lemma covariance_add_smul_one_right (ω : State A) (a b : Observable A) (c : ℝ) :
+    covariance ω a (b + c • 1) = covariance ω a b := by
+  simp only [covariance, centered_add_smul_one]
+
+/-- Variance is nonnegative. -/
+lemma variance_nonneg (ω : State A) (a : Observable A) :
+    0 ≤ variance ω a := by
+  rw [variance, covariance]
+  apply expectation_nonneg
+  show 0 ≤ (Observable.jordan (centered ω a) (centered ω a) : A)
+  rw [Observable.jordan_self]
+  simpa [(centered ω a).property.star_eq] using
+    star_mul_self_nonneg (centered ω a : A)
+
+end State
+
+end OperatorAlgebra

Physlib/QuantumMechanics/OperatorAlgebra/Measurement/Uncertainty.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.QuantumMechanics.OperatorAlgebra.Measurement.State
+public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
+
+/-!
+
+# Uncertainty relations
+
+Positivity of a state gives a Cauchy–Schwarz inequality for expectation values.
+Applied to centered observables, this yields the Robertson–Schrödinger and
+Robertson uncertainty relations.
+
+-/
+
+@[expose] public section
+
+open scoped ComplexOrder InnerProductSpace OperatorAlgebra
+
+namespace OperatorAlgebra
+
+variable {A : Type*} [OperatorAlgebra A]
+
+namespace State
+
+/-! ## Products of observables -/
+
+/-- The product of two observables splits into its symmetric and antisymmetric parts. -/
+lemma observable_mul_decomposition (a b : Observable A) :
+    (a : A) * b =
+      (a ⊙ b : A) + Complex.I • ((⁅a, b⁆ : Observable A) : A) := by
+  change
+    (a : A) * b =
+      ↑(realPart ((a : A) * (b : A))) +
+        Complex.I • ↑(imaginaryPart ((a : A) * (b : A)))
+  exact (realPart_add_I_smul_imaginaryPart ((a : A) * (b : A))).symm
+
+/-- Centering does not change the antisymmetric part of a product. -/
+@[simp]
+lemma bracket_centered (ω : State A) (a b : Observable A) :
+    ⁅centered ω a, centered ω b⁆ = ⁅a, b⁆ := by
+  simp [centered, sub_lie, lie_sub]
+
+/-- The expectation of a centered product splits into its symmetric and antisymmetric parts. -/
+lemma apply_centered_mul_centered (ω : State A) (a b : Observable A) :
+    ω ((centered ω a : A) * centered ω b) =
+      (covariance ω a b : ℂ) + Complex.I * (ω⟨⁅a, b⁆⟩ : ℂ) := by
+  rw [observable_mul_decomposition, map_add, map_smul,
+    apply_observable_eq_expectation, apply_observable_eq_expectation,
+    bracket_centered]
+  rfl
+
+/-! ## Cauchy–Schwarz -/
+
+/-- Reversing a product of observables conjugates its state value. -/
+lemma apply_mul_comm_eq_star (ω : State A) (a b : Observable A) :
+    ω ((b : A) * a) = star (ω ((a : A) * b)) := by
+  rw [← map_star, star_mul, a.property.star_eq, b.property.star_eq]
+
+/-- GNS Cauchy–Schwarz for centered observables, before rewriting to variances. -/
+lemma centered_gns_cauchy_schwarz (ω : State A) (a b : Observable A) :
+    ‖ω ((centered ω a : A) * centered ω b)‖ *
+        ‖ω ((centered ω b : A) * centered ω a)‖ ≤
+      variance ω a * variance ω b := by
+  let φ := ω.toPositiveLinearMap
+  have h := inner_mul_inner_self_le (𝕜 := ℂ)
+    (φ.toPreGNS (centered ω a : A))
+    (φ.toPreGNS (centered ω b : A))
+  simp only [PositiveLinearMap.preGNS_inner_def,
+    PositiveLinearMap.ofPreGNS_toPreGNS,
+    (centered ω a).property.star_eq,
+    (centered ω b).property.star_eq] at h
+  rw [variance, covariance]
+  change
+    ‖φ ((centered ω a : A) * centered ω b)‖ *
+        ‖φ ((centered ω b : A) * centered ω a)‖ ≤
+      (φ ((centered ω a ⊙ centered ω a : Observable A) : A)).re *
+        (φ ((centered ω b ⊙ centered ω b : Observable A) : A)).re
+  rw [Observable.jordan_self, Observable.jordan_self]
+  exact h
+
+/-- Cauchy–Schwarz for centered observables. -/
+lemma centered_cauchy_schwarz (ω : State A) (a b : Observable A) :
+    Complex.normSq (ω ((centered ω a : A) * centered ω b)) ≤
+      variance ω a * variance ω b := by
+  calc
+    Complex.normSq (ω ((centered ω a : A) * centered ω b)) =
+        ‖ω ((centered ω a : A) * centered ω b)‖ *
+          ‖ω ((centered ω b : A) * centered ω a)‖ := by
+      rw [apply_mul_comm_eq_star]
+      simp [Complex.normSq_eq_norm_sq, pow_two]
+    _ ≤ _ := centered_gns_cauchy_schwarz ω a b
+
+/-! ## Uncertainty relations -/
+
+/--
+The Robertson–Schrödinger uncertainty inequality.
+
+With the chosen normalization of the bracket, the conventional factor `1/4`
+is absorbed into the bracket.
+-/
+lemma robertson_schrodinger (ω : State A) (a b : Observable A) :
+    covariance ω a b ^ 2 + ω⟨⁅a, b⁆⟩ ^ 2 ≤
+      variance ω a * variance ω b := by
+  have h := centered_cauchy_schwarz ω a b
+  rw [apply_centered_mul_centered, Complex.normSq_apply] at h
+  simpa [pow_two] using h
+
+/-- Covariance satisfies the Cauchy–Schwarz inequality. -/
+lemma covariance_cauchy_schwarz (ω : State A) (a b : Observable A) :
+    covariance ω a b ^ 2 ≤ variance ω a * variance ω b := by
+  nlinarith [robertson_schrodinger ω a b,
+    sq_nonneg (ω⟨⁅a, b⁆⟩)]
+
+/-- The Robertson uncertainty inequality. -/
+lemma robertson (ω : State A) (a b : Observable A) :
+    ω⟨⁅a, b⁆⟩ ^ 2 ≤ variance ω a * variance ω b := by
+  nlinarith [robertson_schrodinger ω a b,
+    sq_nonneg (covariance ω a b)]
+
+end State
+
+end OperatorAlgebra