From 9ece39acc7cd081f075da4ca1bf50b7d41f6c24a Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Fri, 28 Aug 2026 18:30:49 -0600 Subject: [PATCH 1/9] =?UTF-8?q?feat(QuantumInfo):=20add=20quantum=20Cram?= =?UTF-8?q?=C3=A9r-Rao=20bound=20for=20pure=20states?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Robertson's uncertainty relation for two Hermitian matrices on a finite-dimensional pure state (robertson_uncertainty), and the quantum Cramér-Rao bound for a unitarily-generated one-parameter family under the standard locally-unbiased-estimator normalization (cramerRao_pureState_unitary), proved from Cauchy-Schwarz rather than assumed as a corollary of Robertson. Includes the supporting Ket/Matrix API (toEuclideanSpace, onVec, expValC, expVal, variance, centered) needed to state and prove both. Co-authored-by: Claude Sonnet 5 --- QuantumInfo.lean | 1 + QuantumInfo/Measurements/CramerRao.lean | 291 ++++++++++++++++++++++++ 2 files changed, 292 insertions(+) create mode 100644 QuantumInfo/Measurements/CramerRao.lean diff --git a/QuantumInfo.lean b/QuantumInfo.lean index 6fa9744d9..e8c2fdf99 100644 --- a/QuantumInfo.lean +++ b/QuantumInfo.lean @@ -42,6 +42,7 @@ public import QuantumInfo.Entropy.DPI public import QuantumInfo.States.Mixed.MState public import QuantumInfo.Channels.Pinching public import QuantumInfo.Measurements.POVM +public import QuantumInfo.Measurements.CramerRao public import QuantumInfo.Operators.Unitary --Documentation without code diff --git a/QuantumInfo/Measurements/CramerRao.lean b/QuantumInfo/Measurements/CramerRao.lean new file mode 100644 index 000000000..674d69e3c --- /dev/null +++ b/QuantumInfo/Measurements/CramerRao.lean @@ -0,0 +1,291 @@ +/- +Copyright (c) 2026 Eduardo Nava-Hernandez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eduardo Nava-Hernandez +-/ +module + +public import QuantumInfo.States.Pure.Braket +public import Mathlib.Analysis.InnerProductSpace.Basic + +/-! +# The quantum Cramér–Rao bound, pure states, unitary parametrization + +For a pure state `ψ` and a one-parameter family `ψ_θ = e^{-iθG}ψ` generated unitarily by a +self-adjoint `G`, and an observable `O` used to build a locally unbiased estimator of `θ` +(normalized so that `∂_θ⟨O⟩_θ|_{θ=0} = 1`), the standard quantum Cramér–Rao bound states + + Var_ψ(O) ≥ 1 / (4 · Var_ψ(G)), + +with `4 · Var_ψ(G)` the quantum Fisher information of the family at `θ = 0`. This is the +textbook identification of Helstrom (*Quantum Detection and Estimation Theory*, Academic Press, +1976, Chap. VIII.4) and of Braunstein and Caves (Phys. Rev. Lett. **72**, 3439 (1994), +Eqs. (32)–(33), the density-operator metric `ds²_DO/dX² ≤ Σⱼ(dpⱼ/dX)²/pⱼ + 4⟨(Δĥ)²⟩_X` becomes +an *equality* on the pure-state boundary, giving `4⟨(Δĥ)²⟩_X` exactly, and combines with their +Eq. (32), `N⟨(δX)²⟩_X · (ds²_DO/dX²) ≥ 1`, to give the bound stated above). Braunstein and Caves +identify this pure-state case explicitly as "a Mandelstam–Tamm uncertainty principle... for a +parameter `X` and the 'conjugate' operator `ĥ`" (paragraph following their Eq. (33)), i.e. the +same Cramér–Rao/Mandelstam–Tamm identification, from the primary source, rather than re-derived. + +The bound follows *directly* from the Robertson uncertainty relation applied to the pair +`(G, O)`, using the identity `∂_θ⟨O⟩_θ|_{θ=0} = i⟨ψ, [G, O] ψ⟩` for a unitarily generated family. + +This file proves the algebraic content: Robertson's inequality for two Hermitian matrices on a +finite-dimensional pure state, and the Cramér–Rao bound as its corollary under the commutator +normalization hypothesis. It does *not* formalize the dynamics that produces the normalization +(that identity is a calculus fact about differentiating a unitary conjugation, external to this +module); the normalization is taken as an explicit hypothesis, exactly as the cited literature +states it for a locally unbiased estimator. + +## A. Expectation value and variance of a Hermitian observable on a pure state + +## B. Robertson's uncertainty relation + +## C. The quantum Cramér–Rao bound +-/ + +@[expose] public section + +noncomputable section + +open scoped ComplexConjugate + +variable {d : Type*} [Fintype d] + +/-! ## A. Expectation value and variance of a Hermitian observable on a pure state -/ + +/-- The state vector of a `Ket`, seen in `EuclideanSpace ℂ d` where Mathlib's inner product +space API (in particular Cauchy–Schwarz) is available. -/ +def Ket.toEuclideanSpace (ψ : Ket d) : EuclideanSpace ℂ d := + (WithLp.equiv 2 (d → ℂ)).symm ψ.vec + +@[simp] +lemma Ket.toEuclideanSpace_apply (ψ : Ket d) (i : d) : + ψ.toEuclideanSpace i = ψ.vec i := rfl + +lemma Ket.norm_toEuclideanSpace (ψ : Ket d) : ‖ψ.toEuclideanSpace‖ = 1 := by + rw [EuclideanSpace.norm_eq] + simp only [Ket.toEuclideanSpace_apply] + rw [ψ.normalized'] + exact Real.sqrt_one + +lemma Ket.inner_self_toEuclideanSpace (ψ : Ket d) : + inner ℂ ψ.toEuclideanSpace ψ.toEuclideanSpace = (1 : ℂ) := by + rw [@inner_self_eq_norm_sq_to_K ℂ, ψ.norm_toEuclideanSpace] + norm_num + +/-- The action of a matrix on a vector of `EuclideanSpace ℂ d`, via `Matrix.mulVec` on the +underlying function. -/ +def Matrix.onVec (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : EuclideanSpace ℂ d := + (WithLp.equiv 2 (d → ℂ)).symm (A.mulVec (WithLp.equiv 2 (d → ℂ) v)) + +@[simp] +lemma Matrix.onVec_apply (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) (i : d) : + A.onVec v i = ∑ j, A i j * v j := rfl + +lemma Matrix.onVec_mul (A B : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : + (A * B).onVec v = A.onVec (B.onVec v) := by + ext i + simp only [Matrix.onVec_apply, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun j _ => Finset.sum_congr rfl fun k _ => ?_ + ring + +lemma Matrix.onVec_sub (A B : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : + (A - B).onVec v = A.onVec v - B.onVec v := by + ext i + simp [Matrix.onVec_apply, sub_mul, Finset.sum_sub_distrib] + +lemma Matrix.onVec_smul (c : ℂ) (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : + (c • A).onVec v = c • A.onVec v := by + ext i + simp [Matrix.onVec_apply, Finset.mul_sum, mul_assoc] + +/-- Two Hermitian matrices commute past the inner product: `⟪v, A w⟫ = ⟪A v, w⟫`. This is the +only place `A.IsHermitian` is used in this file; everything else is Cauchy–Schwarz. -/ +lemma Matrix.IsHermitian.inner_onVec_comm {A : Matrix d d ℂ} (hA : A.IsHermitian) + (v w : EuclideanSpace ℂ d) : + inner ℂ v (A.onVec w) = inner ℂ (A.onVec v) w := by + simp only [PiLp.inner_apply, RCLike.inner_apply', Matrix.onVec_apply, Finset.mul_sum, + Finset.sum_mul, map_sum, map_mul] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ + have hij : (starRingEnd ℂ) (A i j) = A j i := by + have := congrFun (congrFun hA.eq j) i + simpa [Matrix.conjTranspose_apply] using this + rw [hij] + ring + +/-- Expectation value of a matrix `A` on the pure state `ψ`: `⟨ψ, A ψ⟩`. -/ +def Ket.expValC (ψ : Ket d) (A : Matrix d d ℂ) : ℂ := + inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) + +/-- The expectation value of a Hermitian matrix on a pure state is real: it equals its own +conjugate. -/ +lemma Ket.expValC_conj {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : + (starRingEnd ℂ) (ψ.expValC A) = ψ.expValC A := by + unfold Ket.expValC + rw [inner_conj_symm, hA.inner_onVec_comm] + +/-- Expectation value of a Hermitian matrix `A` on the pure state `ψ`, as a real number. -/ +def Ket.expVal (ψ : Ket d) (A : Matrix d d ℂ) : ℝ := + (ψ.expValC A).re + +lemma Ket.expValC_eq_ofReal_expVal {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : + ψ.expValC A = (ψ.expVal A : ℂ) := by + have h := ψ.expValC_conj hA + have him : (ψ.expValC A).im = 0 := by + have h2 := congrArg Complex.im h + simp only [Complex.conj_im] at h2 + linarith + apply Complex.ext + · simp [Ket.expVal] + · simp [him] + +/-- The variance of a Hermitian observable `A` on the pure state `ψ`. -/ +def Ket.variance (ψ : Ket d) (A : Matrix d d ℂ) : ℝ := + ψ.expVal (A * A) - ψ.expVal A ^ 2 + +/-- The centered vector `A ψ - ⟨A⟩ ψ`, whose squared norm is the variance of `A` on `ψ` +(`Ket.norm_centered_sq`, below). -/ +def Ket.centered (ψ : Ket d) (A : Matrix d d ℂ) : EuclideanSpace ℂ d := + A.onVec ψ.toEuclideanSpace - (ψ.expVal A : ℂ) • ψ.toEuclideanSpace + +/-- The cross term `⟨A⟩ = ⟪ψ, A ψ⟫ = ⟪A ψ, ψ⟫` for a Hermitian `A`, in both orders. -/ +lemma Ket.inner_onVec_self {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : + inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) = (ψ.expVal A : ℂ) ∧ + inner ℂ (A.onVec ψ.toEuclideanSpace) ψ.toEuclideanSpace = (ψ.expVal A : ℂ) := by + have h1 : inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) = (ψ.expVal A : ℂ) := + ψ.expValC_eq_ofReal_expVal hA + refine ⟨h1, ?_⟩ + rw [← hA.inner_onVec_comm, h1] + +lemma Ket.norm_centered_sq {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : + ‖ψ.centered A‖ ^ 2 = ψ.variance A := by + have hAA : ψ.expValC (A * A) = + inner ℂ (A.onVec ψ.toEuclideanSpace) (A.onVec ψ.toEuclideanSpace) := by + show inner ℂ ψ.toEuclideanSpace ((A * A).onVec ψ.toEuclideanSpace) = _ + rw [Matrix.onVec_mul] + exact hA.inner_onVec_comm _ _ + obtain ⟨hcross, hcross'⟩ := ψ.inner_onVec_self hA + have hone := ψ.inner_self_toEuclideanSpace + have hexpand : (inner ℂ (ψ.centered A) (ψ.centered A) : ℂ) = ψ.expValC (A * A) - + (ψ.expVal A : ℂ) * (ψ.expVal A : ℂ) := by + unfold Ket.centered + simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right, + Complex.conj_ofReal, ← hAA, hcross, hcross', hone] + ring + have hre : ‖ψ.centered A‖ ^ 2 = (inner ℂ (ψ.centered A) (ψ.centered A) : ℂ).re := + (inner_self_eq_norm_sq (𝕜 := ℂ) (ψ.centered A)).symm + have hre2 : (ψ.expValC (A * A) - (ψ.expVal A : ℂ) * (ψ.expVal A : ℂ)).re = + ψ.expVal (A * A) - ψ.expVal A ^ 2 := by + rw [Complex.sub_re, ← Complex.ofReal_mul, Complex.ofReal_re] + show ψ.expVal (A * A) - ψ.expVal A * ψ.expVal A = ψ.expVal (A * A) - ψ.expVal A ^ 2 + ring + rw [hre, hexpand, hre2] + rfl + +/-! ## B. Robertson's uncertainty relation -/ + +private lemma Ket.inner_centered_centered {ψ : Ket d} {G O : Matrix d d ℂ} + (hG : G.IsHermitian) (hO : O.IsHermitian) : + (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) = + ψ.expValC (G * O) - (ψ.expVal G : ℂ) * (ψ.expVal O : ℂ) := by + have hGO : ψ.expValC (G * O) = + inner ℂ (G.onVec ψ.toEuclideanSpace) (O.onVec ψ.toEuclideanSpace) := by + show inner ℂ ψ.toEuclideanSpace ((G * O).onVec ψ.toEuclideanSpace) = _ + rw [Matrix.onVec_mul] + exact hG.inner_onVec_comm _ _ + obtain ⟨hGψψ, hGψ⟩ := ψ.inner_onVec_self hG + obtain ⟨hOψψ, hOψ⟩ := ψ.inner_onVec_self hO + have hone := ψ.inner_self_toEuclideanSpace + unfold Ket.centered + simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right, + Complex.conj_ofReal, ← hGO, hGψ, hOψψ, hone] + ring + +/-- **Robertson's uncertainty relation**, for two Hermitian matrices on a finite-dimensional +pure state: the product of variances dominates a quarter of the squared expectation of the +commutator. This is the standard 1929 inequality (H. P. Robertson, *The Uncertainty Principle*, +Phys. Rev. 34, 163–166), specialized here to finite dimension. -/ +theorem robertson_uncertainty {ψ : Ket d} {G O : Matrix d d ℂ} + (hG : G.IsHermitian) (hO : O.IsHermitian) : + (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 ≤ ψ.variance G * ψ.variance O := by + have hCS : ‖(inner ℂ (ψ.centered G) (ψ.centered O) : ℂ)‖ ≤ + ‖ψ.centered G‖ * ‖ψ.centered O‖ := norm_inner_le_norm _ _ + have hprodsq : (‖ψ.centered G‖ * ‖ψ.centered O‖) ^ 2 = ψ.variance G * ψ.variance O := by + rw [mul_pow, ψ.norm_centered_sq hG, ψ.norm_centered_sq hO] + have hcomm_herm : (Complex.I • (G * O - O * G)).IsHermitian := by + unfold Matrix.IsHermitian + rw [Matrix.conjTranspose_smul, Matrix.conjTranspose_sub, Matrix.conjTranspose_mul, + Matrix.conjTranspose_mul, hG.eq, hO.eq, Complex.star_def, Complex.conj_I] + module + have hantisym : ψ.expValC (G * O) - ψ.expValC (O * G) = + (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) - + (starRingEnd ℂ) (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) := by + have h1 := ψ.inner_centered_centered hG hO + have h2 := ψ.inner_centered_centered hO hG + have hOG' : inner ℂ (ψ.centered O) (ψ.centered G) = + (starRingEnd ℂ) (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) := + (inner_conj_symm (ψ.centered O) (ψ.centered G)).symm + rw [hOG'] at h2 + rw [h2, h1] + ring + have hcommC : ψ.expValC (Complex.I • (G * O - O * G)) = + Complex.I * (ψ.expValC (G * O) - ψ.expValC (O * G)) := by + show inner ℂ ψ.toEuclideanSpace ((Complex.I • (G * O - O * G)).onVec ψ.toEuclideanSpace) = _ + have hlin : (Complex.I • (G * O - O * G)).onVec ψ.toEuclideanSpace = + Complex.I • ((G * O - O * G).onVec ψ.toEuclideanSpace) := Matrix.onVec_smul _ _ _ + rw [hlin, inner_smul_right, Matrix.onVec_sub, inner_sub_right] + unfold Ket.expValC + ring + have hCreal := ψ.expValC_eq_ofReal_expVal hcomm_herm + set z : ℂ := inner ℂ (ψ.centered G) (ψ.centered O) with hz + have him : z - (starRingEnd ℂ) z = 2 * Complex.I * z.im := by + apply Complex.ext <;> simp [Complex.sub_re, Complex.sub_im]; ring + have hCz : (ψ.expVal (Complex.I • (G * O - O * G)) : ℂ) = -2 * z.im := by + rw [← hCreal, hcommC, hantisym, him] + have : Complex.I * Complex.I = (-1 : ℂ) := Complex.I_mul_I + ring_nf + rw [show Complex.I ^ 2 = (-1 : ℂ) by rw [sq]; exact this] + ring + have hCz' : ψ.expVal (Complex.I • (G * O - O * G)) = -2 * z.im := by + exact_mod_cast hCz + have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by + rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply] + have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by + rw [hnormsq, sq] + nlinarith [sq_nonneg z.re] + have hfinal : (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by + rw [hCz'] + nlinarith [hzim] + calc (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 + ≤ ‖z‖ ^ 2 := hfinal + _ ≤ (‖ψ.centered G‖ * ‖ψ.centered O‖) ^ 2 := by + gcongr + _ = ψ.variance G * ψ.variance O := hprodsq + +/-! ## C. The quantum Cramér–Rao bound -/ + +/-- **The quantum Cramér–Rao bound**, pure states, unitary parametrization (Helstrom 1976, Chap. +VIII.4; Braunstein–Caves, Phys. Rev. Lett. 72, 3439 (1994), Eqs. (32)–(33), pure-state case). For +a family `ψ_θ = e^{-iθG}ψ` and an +observable `O` normalized to `∂_θ⟨O⟩_θ|_{θ=0} = 1` — the standard normalization of a locally +unbiased estimator, taken here as an explicit hypothesis rather than derived from the dynamics +of the family — the variance of `O` is at least the inverse of the quantum Fisher information +`4 · Var_ψ(G)`. -/ +theorem cramerRao_pureState_unitary {ψ : Ket d} {G O : Matrix d d ℂ} + (hG : G.IsHermitian) (hO : O.IsHermitian) + (hnorm : ψ.expVal (Complex.I • (G * O - O * G)) = 1) : + 1 / (4 * ψ.variance G) ≤ ψ.variance O := by + have hR := robertson_uncertainty (ψ := ψ) hG hO + rw [hnorm] at hR + have hGpos : 0 < ψ.variance G := by + rcases lt_or_eq_of_le (by rw [← ψ.norm_centered_sq hG]; positivity : (0:ℝ) ≤ ψ.variance G) + with h | h + · exact h + · exfalso; rw [← h] at hR; norm_num at hR + rw [div_le_iff₀ (by positivity)] + nlinarith [hR] + +end From 4aff1b146e80f4bbddef1517daf6cb1b2e9fd1bc Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Sat, 29 Aug 2026 05:55:05 -0600 Subject: [PATCH 2/9] docs(QuantumInfo): fix Robertson 1929 page range in CramerRao docstring Robertson's "The Uncertainty Principle" (Phys. Rev. 34) is a two-page letter on pages 163-164, not 163-166. Co-authored-by: Claude Sonnet 5 --- QuantumInfo/Measurements/CramerRao.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/QuantumInfo/Measurements/CramerRao.lean b/QuantumInfo/Measurements/CramerRao.lean index 674d69e3c..b5475ef74 100644 --- a/QuantumInfo/Measurements/CramerRao.lean +++ b/QuantumInfo/Measurements/CramerRao.lean @@ -207,7 +207,7 @@ private lemma Ket.inner_centered_centered {ψ : Ket d} {G O : Matrix d d ℂ} /-- **Robertson's uncertainty relation**, for two Hermitian matrices on a finite-dimensional pure state: the product of variances dominates a quarter of the squared expectation of the commutator. This is the standard 1929 inequality (H. P. Robertson, *The Uncertainty Principle*, -Phys. Rev. 34, 163–166), specialized here to finite dimension. -/ +Phys. Rev. 34, 163–164), specialized here to finite dimension. -/ theorem robertson_uncertainty {ψ : Ket d} {G O : Matrix d d ℂ} (hG : G.IsHermitian) (hO : O.IsHermitian) : (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 ≤ ψ.variance G * ψ.variance O := by From ede47fca6548ad35883dd2b0fab7b03c53d684c2 Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Sat, 29 Aug 2026 16:54:39 -0600 Subject: [PATCH 3/9] =?UTF-8?q?feat(QuantumInfo):=20redo=20quantum=20Cram?= =?UTF-8?q?=C3=A9r=E2=80=93Rao=20bound=20for=20MState?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses @Timeroot's review: rebuild the file on `MState` instead of `Ket`, reusing the existing `MState.exp_val` / `exp_val_ℂ` API. - Drops `Ket.toEuclideanSpace`, `Matrix.onVec` (+ its 5 lemmas), `Ket.expValC` and friends: ~120 lines removed. - `MState.variance`, `MState.comm_exp_val` are new first-class API; the GNS Cauchy–Schwarz `|Tr(ρ XᴴY)|² ≤ Tr(ρ XᴴX)·Tr(ρ YᴴY)` is a small private section (`hsVec`, realizing the Hilbert–Schmidt space as `EuclideanSpace ℂ (d × d)`) that can move to `QuantumInfo/ForMathlib/` if preferred. - `robertson_uncertainty` now holds for every finite-dimensional state, not just pure ones. `cramerRao_unitary` is its corollary under the commutator normalization; `cramerRao_pure_unitary` is the pure-state specialization, where `4·Var_ρ(G)` is exactly the quantum Fisher information. - Module docstring reworked: the Helstrom / Braunstein–Caves QFI identification is scoped to the pure case; for mixed states `4·Var_ρ(G) ≥ QFI_SLD`, so the bound is valid but not tight. lake build QuantumInfo.Measurements.CramerRao: OK. lake build QuantumInfo: OK. scripts/lint-style.py: OK. No sorry. Co-authored-by: Claude Sonnet 5 --- QuantumInfo/Measurements/CramerRao.lean | 503 ++++++++++++------------ 1 file changed, 255 insertions(+), 248 deletions(-) diff --git a/QuantumInfo/Measurements/CramerRao.lean b/QuantumInfo/Measurements/CramerRao.lean index b5475ef74..09a420651 100644 --- a/QuantumInfo/Measurements/CramerRao.lean +++ b/QuantumInfo/Measurements/CramerRao.lean @@ -5,287 +5,294 @@ Authors: Eduardo Nava-Hernandez -/ module -public import QuantumInfo.States.Pure.Braket +public import QuantumInfo.States.Mixed.MState public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Analysis.InnerProductSpace.PiL2 /-! -# The quantum Cramér–Rao bound, pure states, unitary parametrization +# The quantum Cramér–Rao bound, unitary parametrization -For a pure state `ψ` and a one-parameter family `ψ_θ = e^{-iθG}ψ` generated unitarily by a +For a state `ρ` and a one-parameter family `ρ_θ = e^{-iθG} ρ e^{iθG}` generated unitarily by a self-adjoint `G`, and an observable `O` used to build a locally unbiased estimator of `θ` (normalized so that `∂_θ⟨O⟩_θ|_{θ=0} = 1`), the standard quantum Cramér–Rao bound states - Var_ψ(O) ≥ 1 / (4 · Var_ψ(G)), - -with `4 · Var_ψ(G)` the quantum Fisher information of the family at `θ = 0`. This is the -textbook identification of Helstrom (*Quantum Detection and Estimation Theory*, Academic Press, -1976, Chap. VIII.4) and of Braunstein and Caves (Phys. Rev. Lett. **72**, 3439 (1994), -Eqs. (32)–(33), the density-operator metric `ds²_DO/dX² ≤ Σⱼ(dpⱼ/dX)²/pⱼ + 4⟨(Δĥ)²⟩_X` becomes -an *equality* on the pure-state boundary, giving `4⟨(Δĥ)²⟩_X` exactly, and combines with their -Eq. (32), `N⟨(δX)²⟩_X · (ds²_DO/dX²) ≥ 1`, to give the bound stated above). Braunstein and Caves -identify this pure-state case explicitly as "a Mandelstam–Tamm uncertainty principle... for a -parameter `X` and the 'conjugate' operator `ĥ`" (paragraph following their Eq. (33)), i.e. the -same Cramér–Rao/Mandelstam–Tamm identification, from the primary source, rather than re-derived. - -The bound follows *directly* from the Robertson uncertainty relation applied to the pair -`(G, O)`, using the identity `∂_θ⟨O⟩_θ|_{θ=0} = i⟨ψ, [G, O] ψ⟩` for a unitarily generated family. - -This file proves the algebraic content: Robertson's inequality for two Hermitian matrices on a -finite-dimensional pure state, and the Cramér–Rao bound as its corollary under the commutator -normalization hypothesis. It does *not* formalize the dynamics that produces the normalization -(that identity is a calculus fact about differentiating a unitary conjugation, external to this -module); the normalization is taken as an explicit hypothesis, exactly as the cited literature -states it for a locally unbiased estimator. - -## A. Expectation value and variance of a Hermitian observable on a pure state - -## B. Robertson's uncertainty relation - -## C. The quantum Cramér–Rao bound + Var_ρ(O) ≥ 1 / (4 · Var_ρ(G)). + +This file proves the algebraic content that this rests on: + +* `MState.robertson_uncertainty` — Robertson's 1929 uncertainty relation for two Hermitian + observables on an arbitrary finite-dimensional state (H. P. Robertson, *The Uncertainty + Principle*, Phys. Rev. **34**, 163–164 (1929)). It holds for mixed states verbatim: the only + input is Cauchy–Schwarz for the GNS inner product `⟪X, Y⟫_ρ = Tr(ρ X† Y)`. +* `MState.cramerRao_unitary` — the Cramér–Rao bound as its corollary under the commutator + normalization hypothesis `⟨i[G,O]⟩_ρ = 1`. +* `MState.cramerRao_pure_unitary` — the pure-state specialization, for which `4 · Var_ρ(G)` is + *exactly* the quantum Fisher information. + +## On the quantum Fisher information + +For a **pure** state `4 · Var_ρ(G)` is the quantum Fisher information of the family at `θ = 0` +(Helstrom, *Quantum Detection and Estimation Theory*, Academic Press, 1976, Chap. VIII.4; +Braunstein and Caves, Phys. Rev. Lett. **72**, 3439 (1994), Eqs. (32)–(33): the density-operator +metric becomes an equality on the pure-state boundary, giving `4⟨(Δĥ)²⟩` exactly, and combining +with their Eq. (32) yields the bound above). Braunstein and Caves identify this pure-state case +explicitly as "a Mandelstam–Tamm uncertainty principle... for a parameter `X` and the 'conjugate' +operator `ĥ`" (paragraph after their Eq. (33)). + +For a **mixed** state `4 · Var_ρ(G) ≥ QFI_SLD(ρ, G)`, with equality iff `ρ` is pure. Hence +`MState.cramerRao_unitary` is a valid Cramér–Rao lower bound for every state, but it is *tight* +(equal to the inverse quantum Fisher information) only in the pure case. The bound itself follows +*directly* from `robertson_uncertainty` applied to `(G, O)` together with the identity +`∂_θ⟨O⟩_θ|_{θ=0} = ⟨i[G,O]⟩_ρ` for a unitarily generated family. This file does *not* formalize +the dynamics that produces the normalization — that identity is a calculus fact about +differentiating a unitary conjugation, external to this module — the normalization is taken as an +explicit hypothesis, exactly as the cited literature states it for a locally unbiased estimator. + +## Table of contents + +- A. The Hilbert–Schmidt embedding `Matrix d d ℂ ↪ EuclideanSpace ℂ (d × d)` +- B. Expectation value, variance, and the commutator pairing on a mixed state +- C. Robertson's uncertainty relation +- D. The quantum Cramér–Rao bound -/ @[expose] public section noncomputable section -open scoped ComplexConjugate +open scoped ComplexConjugate Matrix -variable {d : Type*} [Fintype d] +namespace MState -/-! ## A. Expectation value and variance of a Hermitian observable on a pure state -/ +variable {d : Type*} [Fintype d] [DecidableEq d] -/-- The state vector of a `Ket`, seen in `EuclideanSpace ℂ d` where Mathlib's inner product -space API (in particular Cauchy–Schwarz) is available. -/ -def Ket.toEuclideanSpace (ψ : Ket d) : EuclideanSpace ℂ d := - (WithLp.equiv 2 (d → ℂ)).symm ψ.vec +/-! ## A. The Hilbert–Schmidt embedding -@[simp] -lemma Ket.toEuclideanSpace_apply (ψ : Ket d) (i : d) : - ψ.toEuclideanSpace i = ψ.vec i := rfl - -lemma Ket.norm_toEuclideanSpace (ψ : Ket d) : ‖ψ.toEuclideanSpace‖ = 1 := by - rw [EuclideanSpace.norm_eq] - simp only [Ket.toEuclideanSpace_apply] - rw [ψ.normalized'] - exact Real.sqrt_one - -lemma Ket.inner_self_toEuclideanSpace (ψ : Ket d) : - inner ℂ ψ.toEuclideanSpace ψ.toEuclideanSpace = (1 : ℂ) := by - rw [@inner_self_eq_norm_sq_to_K ℂ, ψ.norm_toEuclideanSpace] - norm_num +We need exactly one nontrivial analytic fact — Cauchy–Schwarz for the GNS inner product +`⟪X, Y⟫_ρ = Tr(ρ X† Y)` — and we obtain it by writing `Tr(ρ X† Y) = ⟪X √ρ, Y √ρ⟫` for the +genuine Hilbert–Schmidt inner product on `d × d` matrices, realized as `EuclideanSpace ℂ (d × d)`. +Nothing here is specific to quantum information; if it is wanted elsewhere it should move to +`QuantumInfo/ForMathlib/`. +-/ -/-- The action of a matrix on a vector of `EuclideanSpace ℂ d`, via `Matrix.mulVec` on the -underlying function. -/ -def Matrix.onVec (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : EuclideanSpace ℂ d := - (WithLp.equiv 2 (d → ℂ)).symm (A.mulVec (WithLp.equiv 2 (d → ℂ) v)) +/-- A `d × d` matrix seen as a vector of `EuclideanSpace ℂ (d × d)`, where Mathlib's inner +product space API (Cauchy–Schwarz in particular) is available. This is the Hilbert–Schmidt +picture: `⟪hsVec A, hsVec B⟫ = Tr(Aᴴ B)` (`hsVec_inner`). -/ +private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := + (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2) +set_option linter.unusedSectionVars false in @[simp] -lemma Matrix.onVec_apply (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) (i : d) : - A.onVec v i = ∑ j, A i j * v j := rfl - -lemma Matrix.onVec_mul (A B : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : - (A * B).onVec v = A.onVec (B.onVec v) := by - ext i - simp only [Matrix.onVec_apply, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum] - rw [Finset.sum_comm] - refine Finset.sum_congr rfl fun j _ => Finset.sum_congr rfl fun k _ => ?_ - ring - -lemma Matrix.onVec_sub (A B : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : - (A - B).onVec v = A.onVec v - B.onVec v := by - ext i - simp [Matrix.onVec_apply, sub_mul, Finset.sum_sub_distrib] - -lemma Matrix.onVec_smul (c : ℂ) (A : Matrix d d ℂ) (v : EuclideanSpace ℂ d) : - (c • A).onVec v = c • A.onVec v := by - ext i - simp [Matrix.onVec_apply, Finset.mul_sum, mul_assoc] - -/-- Two Hermitian matrices commute past the inner product: `⟪v, A w⟫ = ⟪A v, w⟫`. This is the -only place `A.IsHermitian` is used in this file; everything else is Cauchy–Schwarz. -/ -lemma Matrix.IsHermitian.inner_onVec_comm {A : Matrix d d ℂ} (hA : A.IsHermitian) - (v w : EuclideanSpace ℂ d) : - inner ℂ v (A.onVec w) = inner ℂ (A.onVec v) w := by - simp only [PiLp.inner_apply, RCLike.inner_apply', Matrix.onVec_apply, Finset.mul_sum, - Finset.sum_mul, map_sum, map_mul] +private lemma hsVec_apply (M : Matrix d d ℂ) (p : d × d) : hsVec M p = M p.1 p.2 := rfl + +set_option linter.unusedSectionVars false in +/-- The defining property of `hsVec`: its inner product is `Tr(Aᴴ B)`. -/ +private lemma hsVec_inner (A B : Matrix d d ℂ) : + inner ℂ (hsVec A) (hsVec B) = (Aᴴ * B).trace := by + rw [PiLp.inner_apply, Fintype.sum_prod_type, Matrix.trace] + simp only [hsVec_apply, RCLike.inner_apply, starRingEnd_apply, Matrix.diag_apply, + Matrix.mul_apply, Matrix.conjTranspose_apply] rw [Finset.sum_comm] refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ - have hij : (starRingEnd ℂ) (A i j) = A j i := by - have := congrFun (congrFun hA.eq j) i - simpa [Matrix.conjTranspose_apply] using this - rw [hij] - ring - -/-- Expectation value of a matrix `A` on the pure state `ψ`: `⟨ψ, A ψ⟩`. -/ -def Ket.expValC (ψ : Ket d) (A : Matrix d d ℂ) : ℂ := - inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) - -/-- The expectation value of a Hermitian matrix on a pure state is real: it equals its own -conjugate. -/ -lemma Ket.expValC_conj {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : - (starRingEnd ℂ) (ψ.expValC A) = ψ.expValC A := by - unfold Ket.expValC - rw [inner_conj_symm, hA.inner_onVec_comm] - -/-- Expectation value of a Hermitian matrix `A` on the pure state `ψ`, as a real number. -/ -def Ket.expVal (ψ : Ket d) (A : Matrix d d ℂ) : ℝ := - (ψ.expValC A).re - -lemma Ket.expValC_eq_ofReal_expVal {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : - ψ.expValC A = (ψ.expVal A : ℂ) := by - have h := ψ.expValC_conj hA - have him : (ψ.expValC A).im = 0 := by - have h2 := congrArg Complex.im h - simp only [Complex.conj_im] at h2 - linarith - apply Complex.ext - · simp [Ket.expVal] - · simp [him] - -/-- The variance of a Hermitian observable `A` on the pure state `ψ`. -/ -def Ket.variance (ψ : Ket d) (A : Matrix d d ℂ) : ℝ := - ψ.expVal (A * A) - ψ.expVal A ^ 2 - -/-- The centered vector `A ψ - ⟨A⟩ ψ`, whose squared norm is the variance of `A` on `ψ` -(`Ket.norm_centered_sq`, below). -/ -def Ket.centered (ψ : Ket d) (A : Matrix d d ℂ) : EuclideanSpace ℂ d := - A.onVec ψ.toEuclideanSpace - (ψ.expVal A : ℂ) • ψ.toEuclideanSpace - -/-- The cross term `⟨A⟩ = ⟪ψ, A ψ⟫ = ⟪A ψ, ψ⟫` for a Hermitian `A`, in both orders. -/ -lemma Ket.inner_onVec_self {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : - inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) = (ψ.expVal A : ℂ) ∧ - inner ℂ (A.onVec ψ.toEuclideanSpace) ψ.toEuclideanSpace = (ψ.expVal A : ℂ) := by - have h1 : inner ℂ ψ.toEuclideanSpace (A.onVec ψ.toEuclideanSpace) = (ψ.expVal A : ℂ) := - ψ.expValC_eq_ofReal_expVal hA - refine ⟨h1, ?_⟩ - rw [← hA.inner_onVec_comm, h1] - -lemma Ket.norm_centered_sq {ψ : Ket d} {A : Matrix d d ℂ} (hA : A.IsHermitian) : - ‖ψ.centered A‖ ^ 2 = ψ.variance A := by - have hAA : ψ.expValC (A * A) = - inner ℂ (A.onVec ψ.toEuclideanSpace) (A.onVec ψ.toEuclideanSpace) := by - show inner ℂ ψ.toEuclideanSpace ((A * A).onVec ψ.toEuclideanSpace) = _ - rw [Matrix.onVec_mul] - exact hA.inner_onVec_comm _ _ - obtain ⟨hcross, hcross'⟩ := ψ.inner_onVec_self hA - have hone := ψ.inner_self_toEuclideanSpace - have hexpand : (inner ℂ (ψ.centered A) (ψ.centered A) : ℂ) = ψ.expValC (A * A) - - (ψ.expVal A : ℂ) * (ψ.expVal A : ℂ) := by - unfold Ket.centered + exact mul_comm _ _ + +/-! ## B. Expectation value, variance, and the commutator pairing -/ + +section observables + +variable (ρ : MState d) + +/-- `exp_val_ℂ` on a Hermitian matrix is real, and equal to `exp_val`. -/ +lemma exp_val_ℂ_hermitian (A : HermitianMat d ℂ) : + ρ.exp_val_ℂ A.mat = (ρ.exp_val A : ℂ) := by + have hreal : (starRingEnd ℂ) (ρ.exp_val_ℂ A.mat) = ρ.exp_val_ℂ A.mat := by + simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose, + Matrix.conjTranspose_mul, ρ.Hermitian.eq, (A.H).eq] + rw [Matrix.trace_mul_comm] + have hre : (ρ.exp_val_ℂ A.mat).re = ρ.exp_val A := by + simp only [MState.exp_val_ℂ, MState.exp_val, HermitianMat.inner_eq_re_trace, MState.mat_M] + rw [Matrix.trace_mul_comm] + simp + rw [← hre] + exact (Complex.conj_eq_iff_re.mp hreal).symm + +/-- The Hermitian square root of `ρ`, as a bare matrix. -/ +private def sqrtMat : Matrix d d ℂ := ρ.M.sqrt.mat + +private lemma sqrtMat_isHermitian : (ρ.sqrtMat).IsHermitian := ρ.M.sqrt.H + +private lemma sqrtMat_mul_self : ρ.sqrtMat * ρ.sqrtMat = ρ.m := by + show ρ.M.sqrt.mat * ρ.M.sqrt.mat = ρ.m + simp [HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M] + +/-- `Tr(√ρ X √ρ) = Tr(X ρ)`. -/ +private lemma trace_sandwich (X : Matrix d d ℂ) : + (ρ.sqrtMat * X * ρ.sqrtMat).trace = (X * ρ.m).trace := by + rw [Matrix.trace_mul_cycle, ρ.sqrtMat_mul_self, Matrix.trace_mul_comm] + +/-- `⟪hsVec √ρ, hsVec (A √ρ)⟫ = Tr(A ρ) = ⟨A⟩_ρ`, for Hermitian `A`. -/ +private lemma inner_sqrt_left (A : HermitianMat d ℂ) : + inner ℂ (hsVec ρ.sqrtMat) (hsVec (A.mat * ρ.sqrtMat)) = (ρ.exp_val A : ℂ) := by + rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, + show ρ.sqrtMat * (A.mat * ρ.sqrtMat) = ρ.sqrtMat * A.mat * ρ.sqrtMat by + simp [Matrix.mul_assoc], + ρ.trace_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] + +/-- `⟪hsVec √ρ, hsVec √ρ⟫ = Tr(ρ) = 1`. -/ +private lemma inner_sqrt_self : inner ℂ (hsVec ρ.sqrtMat) (hsVec ρ.sqrtMat) = (1 : ℂ) := by + rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, ρ.sqrtMat_mul_self, ρ.tr'] + +/-- `⟪hsVec (G √ρ), hsVec (O √ρ)⟫ = Tr(G O ρ) = ⟨GO⟩_ρ`. -/ +private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : + inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec (O.mat * ρ.sqrtMat)) = + ρ.exp_val_ℂ (G.mat * O.mat) := by + rw [hsVec_inner, Matrix.conjTranspose_mul, ρ.sqrtMat_isHermitian.eq, (G.H).eq, + show ρ.sqrtMat * G.mat * (O.mat * ρ.sqrtMat) = ρ.sqrtMat * (G.mat * O.mat) * ρ.sqrtMat by + simp [Matrix.mul_assoc], + ρ.trace_sandwich, ← exp_val_ℂ] + +/-- The variance of a Hermitian observable `A` on the state `ρ`. -/ +def variance (A : HermitianMat d ℂ) : ℝ := + ρ.exp_val (A ^ 2) - (ρ.exp_val A) ^ 2 + +/-- The **commutator pairing** `⟨i[G,O]⟩_ρ` of two Hermitian observables. It is a real number +because `i[G,O]` is Hermitian when `G` and `O` are; it is the quantity normalized to `1` for a +locally unbiased estimator. -/ +def comm_exp_val (G O : HermitianMat d ℂ) : ℝ := + (ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat))).re + +/-- The centered Hilbert–Schmidt vector `A √ρ - ⟨A⟩_ρ √ρ`, whose squared norm is `Var_ρ(A)` +(`norm_centered_sq`). -/ +private def centeredVec (A : HermitianMat d ℂ) : EuclideanSpace ℂ (d × d) := + hsVec (A.mat * ρ.sqrtMat) - (ρ.exp_val A : ℂ) • hsVec ρ.sqrtMat + +private lemma norm_centered_sq (A : HermitianMat d ℂ) : + ‖ρ.centeredVec A‖ ^ 2 = ρ.variance A := by + have hself := ρ.inner_sqrt_self + have hleft := ρ.inner_sqrt_left A + have hright : inner ℂ (hsVec (A.mat * ρ.sqrtMat)) (hsVec ρ.sqrtMat) = (ρ.exp_val A : ℂ) := by + rw [← inner_conj_symm, hleft, Complex.conj_ofReal] + have hAA := ρ.inner_hsVec_hsVec A A + have hAsq : ρ.exp_val_ℂ (A.mat * A.mat) = (ρ.exp_val (A ^ 2) : ℂ) := by + rw [← ρ.exp_val_ℂ_hermitian (A ^ 2), HermitianMat.mat_pow, pow_two] + have hexpand : (inner ℂ (ρ.centeredVec A) (ρ.centeredVec A) : ℂ) = + ρ.exp_val_ℂ (A.mat * A.mat) - (ρ.exp_val A : ℂ) * (ρ.exp_val A : ℂ) := by + unfold centeredVec simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right, - Complex.conj_ofReal, ← hAA, hcross, hcross', hone] - ring - have hre : ‖ψ.centered A‖ ^ 2 = (inner ℂ (ψ.centered A) (ψ.centered A) : ℂ).re := - (inner_self_eq_norm_sq (𝕜 := ℂ) (ψ.centered A)).symm - have hre2 : (ψ.expValC (A * A) - (ψ.expVal A : ℂ) * (ψ.expVal A : ℂ)).re = - ψ.expVal (A * A) - ψ.expVal A ^ 2 := by - rw [Complex.sub_re, ← Complex.ofReal_mul, Complex.ofReal_re] - show ψ.expVal (A * A) - ψ.expVal A * ψ.expVal A = ψ.expVal (A * A) - ψ.expVal A ^ 2 + Complex.conj_ofReal, hself, hleft, hright, hAA] ring - rw [hre, hexpand, hre2] - rfl - -/-! ## B. Robertson's uncertainty relation -/ - -private lemma Ket.inner_centered_centered {ψ : Ket d} {G O : Matrix d d ℂ} - (hG : G.IsHermitian) (hO : O.IsHermitian) : - (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) = - ψ.expValC (G * O) - (ψ.expVal G : ℂ) * (ψ.expVal O : ℂ) := by - have hGO : ψ.expValC (G * O) = - inner ℂ (G.onVec ψ.toEuclideanSpace) (O.onVec ψ.toEuclideanSpace) := by - show inner ℂ ψ.toEuclideanSpace ((G * O).onVec ψ.toEuclideanSpace) = _ - rw [Matrix.onVec_mul] - exact hG.inner_onVec_comm _ _ - obtain ⟨hGψψ, hGψ⟩ := ψ.inner_onVec_self hG - obtain ⟨hOψψ, hOψ⟩ := ψ.inner_onVec_self hO - have hone := ψ.inner_self_toEuclideanSpace - unfold Ket.centered + have hre : ‖ρ.centeredVec A‖ ^ 2 = (inner ℂ (ρ.centeredVec A) (ρ.centeredVec A) : ℂ).re := + (inner_self_eq_norm_sq (𝕜 := ℂ) (ρ.centeredVec A)).symm + rw [hre, hexpand, variance, hAsq, ← Complex.ofReal_mul, ← Complex.ofReal_sub, Complex.ofReal_re] + ring + +/-- `Var_ρ(A) ≥ 0`. -/ +lemma variance_nonneg (A : HermitianMat d ℂ) : 0 ≤ ρ.variance A := by + rw [← ρ.norm_centered_sq] + positivity + +/-! ## C. Robertson's uncertainty relation -/ + +/-- `exp_val_ℂ` of a product is conjugate-antisymmetric: `conj ⟨GO⟩_ρ = ⟨OG⟩_ρ`. -/ +private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) : + (starRingEnd ℂ) (ρ.exp_val_ℂ (G.mat * O.mat)) = ρ.exp_val_ℂ (O.mat * G.mat) := by + simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose] + rw [show ((G.mat * O.mat) * ρ.m)ᴴ = ρ.m * O.mat * G.mat by + rw [Matrix.conjTranspose_mul, Matrix.conjTranspose_mul, ρ.Hermitian.eq, (G.H).eq, + (O.H).eq, ← Matrix.mul_assoc], + Matrix.mul_assoc, Matrix.trace_mul_comm] + +private lemma inner_centered_centered (G O : HermitianMat d ℂ) : + (inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) : ℂ) = + ρ.exp_val_ℂ (G.mat * O.mat) - (ρ.exp_val G : ℂ) * (ρ.exp_val O : ℂ) := by + have hself := ρ.inner_sqrt_self + have hGl := ρ.inner_sqrt_left G + have hOl := ρ.inner_sqrt_left O + have hGr : inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec ρ.sqrtMat) = (ρ.exp_val G : ℂ) := by + rw [← inner_conj_symm, hGl, Complex.conj_ofReal] + have hGO := ρ.inner_hsVec_hsVec G O + unfold centeredVec simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right, - Complex.conj_ofReal, ← hGO, hGψ, hOψψ, hone] + Complex.conj_ofReal, hself, hOl, hGr, hGO] ring -/-- **Robertson's uncertainty relation**, for two Hermitian matrices on a finite-dimensional -pure state: the product of variances dominates a quarter of the squared expectation of the -commutator. This is the standard 1929 inequality (H. P. Robertson, *The Uncertainty Principle*, -Phys. Rev. 34, 163–164), specialized here to finite dimension. -/ -theorem robertson_uncertainty {ψ : Ket d} {G O : Matrix d d ℂ} - (hG : G.IsHermitian) (hO : O.IsHermitian) : - (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 ≤ ψ.variance G * ψ.variance O := by - have hCS : ‖(inner ℂ (ψ.centered G) (ψ.centered O) : ℂ)‖ ≤ - ‖ψ.centered G‖ * ‖ψ.centered O‖ := norm_inner_le_norm _ _ - have hprodsq : (‖ψ.centered G‖ * ‖ψ.centered O‖) ^ 2 = ψ.variance G * ψ.variance O := by - rw [mul_pow, ψ.norm_centered_sq hG, ψ.norm_centered_sq hO] - have hcomm_herm : (Complex.I • (G * O - O * G)).IsHermitian := by - unfold Matrix.IsHermitian - rw [Matrix.conjTranspose_smul, Matrix.conjTranspose_sub, Matrix.conjTranspose_mul, - Matrix.conjTranspose_mul, hG.eq, hO.eq, Complex.star_def, Complex.conj_I] - module - have hantisym : ψ.expValC (G * O) - ψ.expValC (O * G) = - (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) - - (starRingEnd ℂ) (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) := by - have h1 := ψ.inner_centered_centered hG hO - have h2 := ψ.inner_centered_centered hO hG - have hOG' : inner ℂ (ψ.centered O) (ψ.centered G) = - (starRingEnd ℂ) (inner ℂ (ψ.centered G) (ψ.centered O) : ℂ) := - (inner_conj_symm (ψ.centered O) (ψ.centered G)).symm - rw [hOG'] at h2 - rw [h2, h1] - ring - have hcommC : ψ.expValC (Complex.I • (G * O - O * G)) = - Complex.I * (ψ.expValC (G * O) - ψ.expValC (O * G)) := by - show inner ℂ ψ.toEuclideanSpace ((Complex.I • (G * O - O * G)).onVec ψ.toEuclideanSpace) = _ - have hlin : (Complex.I • (G * O - O * G)).onVec ψ.toEuclideanSpace = - Complex.I • ((G * O - O * G).onVec ψ.toEuclideanSpace) := Matrix.onVec_smul _ _ _ - rw [hlin, inner_smul_right, Matrix.onVec_sub, inner_sub_right] - unfold Ket.expValC - ring - have hCreal := ψ.expValC_eq_ofReal_expVal hcomm_herm - set z : ℂ := inner ℂ (ψ.centered G) (ψ.centered O) with hz - have him : z - (starRingEnd ℂ) z = 2 * Complex.I * z.im := by - apply Complex.ext <;> simp [Complex.sub_re, Complex.sub_im]; ring - have hCz : (ψ.expVal (Complex.I • (G * O - O * G)) : ℂ) = -2 * z.im := by - rw [← hCreal, hcommC, hantisym, him] - have : Complex.I * Complex.I = (-1 : ℂ) := Complex.I_mul_I - ring_nf - rw [show Complex.I ^ 2 = (-1 : ℂ) by rw [sq]; exact this] +/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163–164 (1929)), +for two Hermitian observables on an arbitrary finite-dimensional state: the product of variances +dominates a quarter of the squared commutator pairing. -/ +theorem robertson_uncertainty (G O : HermitianMat d ℂ) : + (ρ.comm_exp_val G O) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by + set z : ℂ := inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) with hz + have hCS : ‖z‖ ≤ ‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖ := norm_inner_le_norm _ _ + have hprodsq : (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 = ρ.variance G * ρ.variance O := by + rw [mul_pow, ρ.norm_centered_sq G, ρ.norm_centered_sq O] + -- `z - conj z` is the raw commutator expectation. + have hz_sub : z - conj z = + ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat) := by + have hzz : z = + ρ.exp_val_ℂ (G.mat * O.mat) - (ρ.exp_val G : ℂ) * (ρ.exp_val O : ℂ) := by + rw [hz]; exact ρ.inner_centered_centered G O + rw [hzz, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_ofReal, ρ.exp_val_ℂ_swap] ring - have hCz' : ψ.expVal (Complex.I • (G * O - O * G)) = -2 * z.im := by - exact_mod_cast hCz + -- `⟨i[G,O]⟩_ρ = -2 · Im z`. + have hlin : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = + Complex.I * (ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat)) := by + simp only [MState.exp_val_ℂ, Matrix.smul_mul, Matrix.sub_mul, Matrix.trace_smul, + Matrix.trace_sub, smul_eq_mul] + have hw : z - conj z = 2 * Complex.I * (z.im : ℂ) := by + apply Complex.ext + · simp [Complex.sub_re, Complex.conj_re, Complex.mul_re, Complex.mul_im] + · simp [Complex.sub_im, Complex.conj_im, Complex.mul_re, Complex.mul_im] + ring + have hcomm : ρ.comm_exp_val G O = -2 * z.im := by + have hval : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = + ((-2 * z.im : ℝ) : ℂ) := by + rw [hlin, ← hz_sub, hw] + push_cast + rw [show Complex.I * (2 * Complex.I * (z.im : ℂ)) = + 2 * (Complex.I * Complex.I) * (z.im : ℂ) by ring, Complex.I_mul_I] + ring + rw [comm_exp_val, hval, Complex.ofReal_re] + -- Combine Cauchy–Schwarz with `Im z ^ 2 ≤ ‖z‖ ^ 2`. have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply] have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by - rw [hnormsq, sq] - nlinarith [sq_nonneg z.re] - have hfinal : (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by - rw [hCz'] - nlinarith [hzim] - calc (ψ.expVal (Complex.I • (G * O - O * G))) ^ 2 / 4 + rw [hnormsq, sq]; nlinarith [sq_nonneg z.re] + have hfinal : (ρ.comm_exp_val G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by + rw [hcomm]; nlinarith [hzim] + calc (ρ.comm_exp_val G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := hfinal - _ ≤ (‖ψ.centered G‖ * ‖ψ.centered O‖) ^ 2 := by - gcongr - _ = ψ.variance G * ψ.variance O := hprodsq - -/-! ## C. The quantum Cramér–Rao bound -/ - -/-- **The quantum Cramér–Rao bound**, pure states, unitary parametrization (Helstrom 1976, Chap. -VIII.4; Braunstein–Caves, Phys. Rev. Lett. 72, 3439 (1994), Eqs. (32)–(33), pure-state case). For -a family `ψ_θ = e^{-iθG}ψ` and an -observable `O` normalized to `∂_θ⟨O⟩_θ|_{θ=0} = 1` — the standard normalization of a locally -unbiased estimator, taken here as an explicit hypothesis rather than derived from the dynamics -of the family — the variance of `O` is at least the inverse of the quantum Fisher information -`4 · Var_ψ(G)`. -/ -theorem cramerRao_pureState_unitary {ψ : Ket d} {G O : Matrix d d ℂ} - (hG : G.IsHermitian) (hO : O.IsHermitian) - (hnorm : ψ.expVal (Complex.I • (G * O - O * G)) = 1) : - 1 / (4 * ψ.variance G) ≤ ψ.variance O := by - have hR := robertson_uncertainty (ψ := ψ) hG hO + _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr + _ = ρ.variance G * ρ.variance O := hprodsq + +/-! ## D. The quantum Cramér–Rao bound -/ + +/-- **The quantum Cramér–Rao bound**, unitary parametrization (Helstrom 1976, Chap. VIII.4; +Braunstein–Caves, Phys. Rev. Lett. **72**, 3439 (1994), Eqs. (32)–(33)). For a family +`ρ_θ = e^{-iθG} ρ e^{iθG}` and an observable `O` normalized to `∂_θ⟨O⟩_θ|_{θ=0} = 1` — the +standard normalization of a locally unbiased estimator, taken here as the explicit hypothesis +`comm_exp_val` rather than derived from the dynamics — the variance of `O` is at least the +inverse of `4 · Var_ρ(G)`. For a pure state `4 · Var_ρ(G)` is exactly the quantum Fisher +information (see the module docstring); in general it only bounds it from above, so this is a +valid but not tight Cramér–Rao bound. -/ +theorem cramerRao_unitary (G O : HermitianMat d ℂ) + (hG : 0 < ρ.variance G) (hnorm : ρ.comm_exp_val G O = 1) : + 1 / (4 * ρ.variance G) ≤ ρ.variance O := by + have hR := ρ.robertson_uncertainty G O rw [hnorm] at hR - have hGpos : 0 < ψ.variance G := by - rcases lt_or_eq_of_le (by rw [← ψ.norm_centered_sq hG]; positivity : (0:ℝ) ≤ ψ.variance G) - with h | h - · exact h - · exfalso; rw [← h] at hR; norm_num at hR + norm_num at hR rw [div_le_iff₀ (by positivity)] - nlinarith [hR] + nlinarith [hR, ρ.variance_nonneg O] + +/-- The pure-state quantum Cramér–Rao bound: the specialization of `cramerRao_unitary` to +`MState.pure ψ`, for which `4 · Var_ρ(G)` is *exactly* the quantum Fisher information of the +family (Braunstein–Caves 1994, pure-state boundary), so the bound is tight. -/ +theorem cramerRao_pure_unitary {ψ : Ket d} (G O : HermitianMat d ℂ) + (hG : 0 < (MState.pure ψ).variance G) (hnorm : (MState.pure ψ).comm_exp_val G O = 1) : + 1 / (4 * (MState.pure ψ).variance G) ≤ (MState.pure ψ).variance O := + (MState.pure ψ).cramerRao_unitary G O hG hnorm + +end observables + +end MState end From 7a5ec6c26a55fbf5b2873e6d8eb1ab04e006021b Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Mon, 31 Aug 2026 14:09:24 -0600 Subject: [PATCH 4/9] style(QuantumInfo): fix Lean style-linter errors in CramerRao CI "Lean based style linters" flagged 3 issues on the MState redo: - `defsWithUnderscore`: `MState.comm_exp_val` -> `MState.commExpVal` (defs use lowerCamelCase). - `unusedArguments` on `hsVec_apply` (`[Fintype d]`, `[DecidableEq d]`) and `hsVec_inner` (`[DecidableEq d]`): replace the earlier `set_option linter.unusedSectionVars false` with canonical `omit ... in`. Also trims the module docstring and drops the redundant `Mathlib.Analysis.InnerProductSpace.Basic` import. `lake build QuantumInfo.Measurements.CramerRao` OK. `lake exe runPhyslibLinters` -> "Linting passed for QuantumInfo." Co-Authored-By: Claude Sonnet 5 --- QuantumInfo/Measurements/CramerRao.lean | 107 +++++++----------------- 1 file changed, 29 insertions(+), 78 deletions(-) diff --git a/QuantumInfo/Measurements/CramerRao.lean b/QuantumInfo/Measurements/CramerRao.lean index 09a420651..91b3b02ae 100644 --- a/QuantumInfo/Measurements/CramerRao.lean +++ b/QuantumInfo/Measurements/CramerRao.lean @@ -6,54 +6,20 @@ Authors: Eduardo Nava-Hernandez module public import QuantumInfo.States.Mixed.MState -public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.InnerProductSpace.PiL2 /-! # The quantum Cramér–Rao bound, unitary parametrization -For a state `ρ` and a one-parameter family `ρ_θ = e^{-iθG} ρ e^{iθG}` generated unitarily by a -self-adjoint `G`, and an observable `O` used to build a locally unbiased estimator of `θ` -(normalized so that `∂_θ⟨O⟩_θ|_{θ=0} = 1`), the standard quantum Cramér–Rao bound states +For a unitary family generated by a Hermitian observable `G`, a locally unbiased estimator `O` +is normalized by `⟨i[G,O]⟩_ρ = 1`. Robertson's uncertainty relation then gives Var_ρ(O) ≥ 1 / (4 · Var_ρ(G)). -This file proves the algebraic content that this rests on: - -* `MState.robertson_uncertainty` — Robertson's 1929 uncertainty relation for two Hermitian - observables on an arbitrary finite-dimensional state (H. P. Robertson, *The Uncertainty - Principle*, Phys. Rev. **34**, 163–164 (1929)). It holds for mixed states verbatim: the only - input is Cauchy–Schwarz for the GNS inner product `⟪X, Y⟫_ρ = Tr(ρ X† Y)`. -* `MState.cramerRao_unitary` — the Cramér–Rao bound as its corollary under the commutator - normalization hypothesis `⟨i[G,O]⟩_ρ = 1`. -* `MState.cramerRao_pure_unitary` — the pure-state specialization, for which `4 · Var_ρ(G)` is - *exactly* the quantum Fisher information. - -## On the quantum Fisher information - -For a **pure** state `4 · Var_ρ(G)` is the quantum Fisher information of the family at `θ = 0` -(Helstrom, *Quantum Detection and Estimation Theory*, Academic Press, 1976, Chap. VIII.4; -Braunstein and Caves, Phys. Rev. Lett. **72**, 3439 (1994), Eqs. (32)–(33): the density-operator -metric becomes an equality on the pure-state boundary, giving `4⟨(Δĥ)²⟩` exactly, and combining -with their Eq. (32) yields the bound above). Braunstein and Caves identify this pure-state case -explicitly as "a Mandelstam–Tamm uncertainty principle... for a parameter `X` and the 'conjugate' -operator `ĥ`" (paragraph after their Eq. (33)). - -For a **mixed** state `4 · Var_ρ(G) ≥ QFI_SLD(ρ, G)`, with equality iff `ρ` is pure. Hence -`MState.cramerRao_unitary` is a valid Cramér–Rao lower bound for every state, but it is *tight* -(equal to the inverse quantum Fisher information) only in the pure case. The bound itself follows -*directly* from `robertson_uncertainty` applied to `(G, O)` together with the identity -`∂_θ⟨O⟩_θ|_{θ=0} = ⟨i[G,O]⟩_ρ` for a unitarily generated family. This file does *not* formalize -the dynamics that produces the normalization — that identity is a calculus fact about -differentiating a unitary conjugation, external to this module — the normalization is taken as an -explicit hypothesis, exactly as the cited literature states it for a locally unbiased estimator. - -## Table of contents - -- A. The Hilbert–Schmidt embedding `Matrix d d ℂ ↪ EuclideanSpace ℂ (d × d)` -- B. Expectation value, variance, and the commutator pairing on a mixed state -- C. Robertson's uncertainty relation -- D. The quantum Cramér–Rao bound +For pure states, `4 · Var_ρ(G)` is the quantum Fisher information of the unitary family, so this is +the Mandelstam--Tamm form of the quantum Cramér--Rao bound. The derivative identity for the unitary +family is kept as the explicit normalization hypothesis; this file proves only the finite +dimensional algebra over Physlib's `MState` and `HermitianMat`. -/ @[expose] public section @@ -66,27 +32,19 @@ namespace MState variable {d : Type*} [Fintype d] [DecidableEq d] -/-! ## A. The Hilbert–Schmidt embedding - -We need exactly one nontrivial analytic fact — Cauchy–Schwarz for the GNS inner product -`⟪X, Y⟫_ρ = Tr(ρ X† Y)` — and we obtain it by writing `Tr(ρ X† Y) = ⟪X √ρ, Y √ρ⟫` for the -genuine Hilbert–Schmidt inner product on `d × d` matrices, realized as `EuclideanSpace ℂ (d × d)`. -Nothing here is specific to quantum information; if it is wanted elsewhere it should move to -`QuantumInfo/ForMathlib/`. --/ +/-! ## Hilbert--Schmidt embedding -/ /-- A `d × d` matrix seen as a vector of `EuclideanSpace ℂ (d × d)`, where Mathlib's inner -product space API (Cauchy–Schwarz in particular) is available. This is the Hilbert–Schmidt -picture: `⟪hsVec A, hsVec B⟫ = Tr(Aᴴ B)` (`hsVec_inner`). -/ +product space API is available. -/ private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2) -set_option linter.unusedSectionVars false in +omit [Fintype d] [DecidableEq d] in @[simp] private lemma hsVec_apply (M : Matrix d d ℂ) (p : d × d) : hsVec M p = M p.1 p.2 := rfl -set_option linter.unusedSectionVars false in -/-- The defining property of `hsVec`: its inner product is `Tr(Aᴴ B)`. -/ +omit [DecidableEq d] in +/-- `hsVec` realizes the Hilbert--Schmidt inner product. -/ private lemma hsVec_inner (A B : Matrix d d ℂ) : inner ℂ (hsVec A) (hsVec B) = (Aᴴ * B).trace := by rw [PiLp.inner_apply, Fintype.sum_prod_type, Matrix.trace] @@ -96,7 +54,7 @@ private lemma hsVec_inner (A B : Matrix d d ℂ) : refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ exact mul_comm _ _ -/-! ## B. Expectation value, variance, and the commutator pairing -/ +/-! ## Expectation value, variance, and commutator pairing -/ section observables @@ -130,7 +88,7 @@ private lemma trace_sandwich (X : Matrix d d ℂ) : (ρ.sqrtMat * X * ρ.sqrtMat).trace = (X * ρ.m).trace := by rw [Matrix.trace_mul_cycle, ρ.sqrtMat_mul_self, Matrix.trace_mul_comm] -/-- `⟪hsVec √ρ, hsVec (A √ρ)⟫ = Tr(A ρ) = ⟨A⟩_ρ`, for Hermitian `A`. -/ +/-- `⟪√ρ, A√ρ⟫ = ⟨A⟩_ρ`, in Hilbert--Schmidt coordinates. -/ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : inner ℂ (hsVec ρ.sqrtMat) (hsVec (A.mat * ρ.sqrtMat)) = (ρ.exp_val A : ℂ) := by rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, @@ -138,11 +96,11 @@ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : simp [Matrix.mul_assoc], ρ.trace_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] -/-- `⟪hsVec √ρ, hsVec √ρ⟫ = Tr(ρ) = 1`. -/ +/-- `⟪√ρ, √ρ⟫ = Tr(ρ) = 1`, in Hilbert--Schmidt coordinates. -/ private lemma inner_sqrt_self : inner ℂ (hsVec ρ.sqrtMat) (hsVec ρ.sqrtMat) = (1 : ℂ) := by rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, ρ.sqrtMat_mul_self, ρ.tr'] -/-- `⟪hsVec (G √ρ), hsVec (O √ρ)⟫ = Tr(G O ρ) = ⟨GO⟩_ρ`. -/ +/-- `⟪G√ρ, O√ρ⟫ = Tr(G O ρ)`, in Hilbert--Schmidt coordinates. -/ private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec (O.mat * ρ.sqrtMat)) = ρ.exp_val_ℂ (G.mat * O.mat) := by @@ -158,7 +116,7 @@ def variance (A : HermitianMat d ℂ) : ℝ := /-- The **commutator pairing** `⟨i[G,O]⟩_ρ` of two Hermitian observables. It is a real number because `i[G,O]` is Hermitian when `G` and `O` are; it is the quantity normalized to `1` for a locally unbiased estimator. -/ -def comm_exp_val (G O : HermitianMat d ℂ) : ℝ := +def commExpVal (G O : HermitianMat d ℂ) : ℝ := (ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat))).re /-- The centered Hilbert–Schmidt vector `A √ρ - ⟨A⟩_ρ √ρ`, whose squared norm is `Var_ρ(A)` @@ -191,7 +149,7 @@ lemma variance_nonneg (A : HermitianMat d ℂ) : 0 ≤ ρ.variance A := by rw [← ρ.norm_centered_sq] positivity -/-! ## C. Robertson's uncertainty relation -/ +/-! ## Robertson's uncertainty relation -/ /-- `exp_val_ℂ` of a product is conjugate-antisymmetric: `conj ⟨GO⟩_ρ = ⟨OG⟩_ρ`. -/ private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) : @@ -220,7 +178,7 @@ private lemma inner_centered_centered (G O : HermitianMat d ℂ) : for two Hermitian observables on an arbitrary finite-dimensional state: the product of variances dominates a quarter of the squared commutator pairing. -/ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : - (ρ.comm_exp_val G O) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by + (ρ.commExpVal G O) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by set z : ℂ := inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) with hz have hCS : ‖z‖ ≤ ‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖ := norm_inner_le_norm _ _ have hprodsq : (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 = ρ.variance G * ρ.variance O := by @@ -243,7 +201,7 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : · simp [Complex.sub_re, Complex.conj_re, Complex.mul_re, Complex.mul_im] · simp [Complex.sub_im, Complex.conj_im, Complex.mul_re, Complex.mul_im] ring - have hcomm : ρ.comm_exp_val G O = -2 * z.im := by + have hcomm : ρ.commExpVal G O = -2 * z.im := by have hval : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = ((-2 * z.im : ℝ) : ℂ) := by rw [hlin, ← hz_sub, hw] @@ -251,31 +209,25 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : rw [show Complex.I * (2 * Complex.I * (z.im : ℂ)) = 2 * (Complex.I * Complex.I) * (z.im : ℂ) by ring, Complex.I_mul_I] ring - rw [comm_exp_val, hval, Complex.ofReal_re] + rw [commExpVal, hval, Complex.ofReal_re] -- Combine Cauchy–Schwarz with `Im z ^ 2 ≤ ‖z‖ ^ 2`. have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply] have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by rw [hnormsq, sq]; nlinarith [sq_nonneg z.re] - have hfinal : (ρ.comm_exp_val G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by + have hfinal : (ρ.commExpVal G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by rw [hcomm]; nlinarith [hzim] - calc (ρ.comm_exp_val G O) ^ 2 / 4 + calc (ρ.commExpVal G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := hfinal _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr _ = ρ.variance G * ρ.variance O := hprodsq -/-! ## D. The quantum Cramér–Rao bound -/ +/-! ## The quantum Cramér--Rao bound -/ -/-- **The quantum Cramér–Rao bound**, unitary parametrization (Helstrom 1976, Chap. VIII.4; -Braunstein–Caves, Phys. Rev. Lett. **72**, 3439 (1994), Eqs. (32)–(33)). For a family -`ρ_θ = e^{-iθG} ρ e^{iθG}` and an observable `O` normalized to `∂_θ⟨O⟩_θ|_{θ=0} = 1` — the -standard normalization of a locally unbiased estimator, taken here as the explicit hypothesis -`comm_exp_val` rather than derived from the dynamics — the variance of `O` is at least the -inverse of `4 · Var_ρ(G)`. For a pure state `4 · Var_ρ(G)` is exactly the quantum Fisher -information (see the module docstring); in general it only bounds it from above, so this is a -valid but not tight Cramér–Rao bound. -/ +/-- **The quantum Cramér--Rao bound**, in unitary parametrization, under the usual local +unbiasedness normalization `⟨i[G,O]⟩_ρ = 1`. -/ theorem cramerRao_unitary (G O : HermitianMat d ℂ) - (hG : 0 < ρ.variance G) (hnorm : ρ.comm_exp_val G O = 1) : + (hG : 0 < ρ.variance G) (hnorm : ρ.commExpVal G O = 1) : 1 / (4 * ρ.variance G) ≤ ρ.variance O := by have hR := ρ.robertson_uncertainty G O rw [hnorm] at hR @@ -283,11 +235,10 @@ theorem cramerRao_unitary (G O : HermitianMat d ℂ) rw [div_le_iff₀ (by positivity)] nlinarith [hR, ρ.variance_nonneg O] -/-- The pure-state quantum Cramér–Rao bound: the specialization of `cramerRao_unitary` to -`MState.pure ψ`, for which `4 · Var_ρ(G)` is *exactly* the quantum Fisher information of the -family (Braunstein–Caves 1994, pure-state boundary), so the bound is tight. -/ +/-- Pure-state specialization: `4 · Var_ρ(G)` is the quantum Fisher information of a unitary +family, giving the Mandelstam--Tamm form of the quantum Cramér--Rao bound. -/ theorem cramerRao_pure_unitary {ψ : Ket d} (G O : HermitianMat d ℂ) - (hG : 0 < (MState.pure ψ).variance G) (hnorm : (MState.pure ψ).comm_exp_val G O = 1) : + (hG : 0 < (MState.pure ψ).variance G) (hnorm : (MState.pure ψ).commExpVal G O = 1) : 1 / (4 * (MState.pure ψ).variance G) ≤ (MState.pure ψ).variance O := (MState.pure ψ).cramerRao_unitary G O hG hnorm From cd0170fa4a748f58937d850c5b284a29ca56c43e Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Fri, 4 Sep 2026 12:06:21 -0600 Subject: [PATCH 5/9] refactor(QuantumInfo): address reviewer feedback on Robertson uncertainty MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rework per Timeroot's review: rename CramerRao → RobertsonUncertainty (point 7), move exp_val_ℂ_hermitian to MState.lean as @[simp] (point 2), add MState.variance + variance_nonneg near exp_val (point 4), restate the corollary as 1 ≤ 4 * Var(O) * Var(G) without positivity hypothesis (point 6), delete cramerRao_pure_unitary (point 8). Co-Authored-By: Claude Opus 4.6 --- QuantumInfo.lean | 2 +- ...amerRao.lean => RobertsonUncertainty.lean} | 90 +++++-------------- QuantumInfo/States/Mixed/MState.lean | 34 +++++++ 3 files changed, 58 insertions(+), 68 deletions(-) rename QuantumInfo/Measurements/{CramerRao.lean => RobertsonUncertainty.lean} (68%) diff --git a/QuantumInfo.lean b/QuantumInfo.lean index e8c2fdf99..826d19190 100644 --- a/QuantumInfo.lean +++ b/QuantumInfo.lean @@ -42,7 +42,7 @@ public import QuantumInfo.Entropy.DPI public import QuantumInfo.States.Mixed.MState public import QuantumInfo.Channels.Pinching public import QuantumInfo.Measurements.POVM -public import QuantumInfo.Measurements.CramerRao +public import QuantumInfo.Measurements.RobertsonUncertainty public import QuantumInfo.Operators.Unitary --Documentation without code diff --git a/QuantumInfo/Measurements/CramerRao.lean b/QuantumInfo/Measurements/RobertsonUncertainty.lean similarity index 68% rename from QuantumInfo/Measurements/CramerRao.lean rename to QuantumInfo/Measurements/RobertsonUncertainty.lean index 91b3b02ae..2b49e6c2b 100644 --- a/QuantumInfo/Measurements/CramerRao.lean +++ b/QuantumInfo/Measurements/RobertsonUncertainty.lean @@ -9,17 +9,20 @@ public import QuantumInfo.States.Mixed.MState public import Mathlib.Analysis.InnerProductSpace.PiL2 /-! -# The quantum Cramér–Rao bound, unitary parametrization +# Robertson's uncertainty relation for mixed states -For a unitary family generated by a Hermitian observable `G`, a locally unbiased estimator `O` -is normalized by `⟨i[G,O]⟩_ρ = 1`. Robertson's uncertainty relation then gives +Robertson's uncertainty relation (H. P. Robertson, *The Uncertainty Principle*, Phys. Rev. **34**, +163–164 (1929)) bounds the product of variances of two Hermitian observables by a quarter of the +squared commutator expectation: - Var_ρ(O) ≥ 1 / (4 · Var_ρ(G)). + ⟨i[G,O]⟩² / 4 ≤ Var(G) · Var(O). -For pure states, `4 · Var_ρ(G)` is the quantum Fisher information of the unitary family, so this is -the Mandelstam--Tamm form of the quantum Cramér--Rao bound. The derivative identity for the unitary -family is kept as the explicit normalization hypothesis; this file proves only the finite -dimensional algebra over Physlib's `MState` and `HermitianMat`. +This file proves the relation for arbitrary finite-dimensional mixed states (`MState`) via +Cauchy–Schwarz on the Hilbert–Schmidt space. The main result is `robertson_uncertainty`. + +As a corollary, `robertson_normalized` gives the equivalent multiplicative form +`1 ≤ 4 · Var(O) · Var(G)` under the normalization `⟨i[G,O]⟩ = 1`, without requiring a +separate positivity hypothesis. -/ @[expose] public section @@ -32,10 +35,8 @@ namespace MState variable {d : Type*} [Fintype d] [DecidableEq d] -/-! ## Hilbert--Schmidt embedding -/ +/-! ## Hilbert–Schmidt embedding -/ -/-- A `d × d` matrix seen as a vector of `EuclideanSpace ℂ (d × d)`, where Mathlib's inner -product space API is available. -/ private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2) @@ -44,7 +45,6 @@ omit [Fintype d] [DecidableEq d] in private lemma hsVec_apply (M : Matrix d d ℂ) (p : d × d) : hsVec M p = M p.1 p.2 := rfl omit [DecidableEq d] in -/-- `hsVec` realizes the Hilbert--Schmidt inner product. -/ private lemma hsVec_inner (A B : Matrix d d ℂ) : inner ℂ (hsVec A) (hsVec B) = (Aᴴ * B).trace := by rw [PiLp.inner_apply, Fintype.sum_prod_type, Matrix.trace] @@ -54,27 +54,12 @@ private lemma hsVec_inner (A B : Matrix d d ℂ) : refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ exact mul_comm _ _ -/-! ## Expectation value, variance, and commutator pairing -/ +/-! ## Hilbert–Schmidt centered vectors and the commutator pairing -/ section observables variable (ρ : MState d) -/-- `exp_val_ℂ` on a Hermitian matrix is real, and equal to `exp_val`. -/ -lemma exp_val_ℂ_hermitian (A : HermitianMat d ℂ) : - ρ.exp_val_ℂ A.mat = (ρ.exp_val A : ℂ) := by - have hreal : (starRingEnd ℂ) (ρ.exp_val_ℂ A.mat) = ρ.exp_val_ℂ A.mat := by - simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose, - Matrix.conjTranspose_mul, ρ.Hermitian.eq, (A.H).eq] - rw [Matrix.trace_mul_comm] - have hre : (ρ.exp_val_ℂ A.mat).re = ρ.exp_val A := by - simp only [MState.exp_val_ℂ, MState.exp_val, HermitianMat.inner_eq_re_trace, MState.mat_M] - rw [Matrix.trace_mul_comm] - simp - rw [← hre] - exact (Complex.conj_eq_iff_re.mp hreal).symm - -/-- The Hermitian square root of `ρ`, as a bare matrix. -/ private def sqrtMat : Matrix d d ℂ := ρ.M.sqrt.mat private lemma sqrtMat_isHermitian : (ρ.sqrtMat).IsHermitian := ρ.M.sqrt.H @@ -83,12 +68,10 @@ private lemma sqrtMat_mul_self : ρ.sqrtMat * ρ.sqrtMat = ρ.m := by show ρ.M.sqrt.mat * ρ.M.sqrt.mat = ρ.m simp [HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M] -/-- `Tr(√ρ X √ρ) = Tr(X ρ)`. -/ private lemma trace_sandwich (X : Matrix d d ℂ) : (ρ.sqrtMat * X * ρ.sqrtMat).trace = (X * ρ.m).trace := by rw [Matrix.trace_mul_cycle, ρ.sqrtMat_mul_self, Matrix.trace_mul_comm] -/-- `⟪√ρ, A√ρ⟫ = ⟨A⟩_ρ`, in Hilbert--Schmidt coordinates. -/ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : inner ℂ (hsVec ρ.sqrtMat) (hsVec (A.mat * ρ.sqrtMat)) = (ρ.exp_val A : ℂ) := by rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, @@ -96,11 +79,9 @@ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : simp [Matrix.mul_assoc], ρ.trace_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] -/-- `⟪√ρ, √ρ⟫ = Tr(ρ) = 1`, in Hilbert--Schmidt coordinates. -/ private lemma inner_sqrt_self : inner ℂ (hsVec ρ.sqrtMat) (hsVec ρ.sqrtMat) = (1 : ℂ) := by rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, ρ.sqrtMat_mul_self, ρ.tr'] -/-- `⟪G√ρ, O√ρ⟫ = Tr(G O ρ)`, in Hilbert--Schmidt coordinates. -/ private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec (O.mat * ρ.sqrtMat)) = ρ.exp_val_ℂ (G.mat * O.mat) := by @@ -109,18 +90,10 @@ private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : simp [Matrix.mul_assoc], ρ.trace_sandwich, ← exp_val_ℂ] -/-- The variance of a Hermitian observable `A` on the state `ρ`. -/ -def variance (A : HermitianMat d ℂ) : ℝ := - ρ.exp_val (A ^ 2) - (ρ.exp_val A) ^ 2 - -/-- The **commutator pairing** `⟨i[G,O]⟩_ρ` of two Hermitian observables. It is a real number -because `i[G,O]` is Hermitian when `G` and `O` are; it is the quantity normalized to `1` for a -locally unbiased estimator. -/ +/-- The **commutator pairing** `⟨i[G,O]⟩_ρ` of two Hermitian observables. -/ def commExpVal (G O : HermitianMat d ℂ) : ℝ := (ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat))).re -/-- The centered Hilbert–Schmidt vector `A √ρ - ⟨A⟩_ρ √ρ`, whose squared norm is `Var_ρ(A)` -(`norm_centered_sq`). -/ private def centeredVec (A : HermitianMat d ℂ) : EuclideanSpace ℂ (d × d) := hsVec (A.mat * ρ.sqrtMat) - (ρ.exp_val A : ℂ) • hsVec ρ.sqrtMat @@ -144,14 +117,8 @@ private lemma norm_centered_sq (A : HermitianMat d ℂ) : rw [hre, hexpand, variance, hAsq, ← Complex.ofReal_mul, ← Complex.ofReal_sub, Complex.ofReal_re] ring -/-- `Var_ρ(A) ≥ 0`. -/ -lemma variance_nonneg (A : HermitianMat d ℂ) : 0 ≤ ρ.variance A := by - rw [← ρ.norm_centered_sq] - positivity - /-! ## Robertson's uncertainty relation -/ -/-- `exp_val_ℂ` of a product is conjugate-antisymmetric: `conj ⟨GO⟩_ρ = ⟨OG⟩_ρ`. -/ private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) : (starRingEnd ℂ) (ρ.exp_val_ℂ (G.mat * O.mat)) = ρ.exp_val_ℂ (O.mat * G.mat) := by simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose] @@ -183,7 +150,6 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : have hCS : ‖z‖ ≤ ‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖ := norm_inner_le_norm _ _ have hprodsq : (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 = ρ.variance G * ρ.variance O := by rw [mul_pow, ρ.norm_centered_sq G, ρ.norm_centered_sq O] - -- `z - conj z` is the raw commutator expectation. have hz_sub : z - conj z = ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat) := by have hzz : z = @@ -191,7 +157,6 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : rw [hz]; exact ρ.inner_centered_centered G O rw [hzz, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_ofReal, ρ.exp_val_ℂ_swap] ring - -- `⟨i[G,O]⟩_ρ = -2 · Im z`. have hlin : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = Complex.I * (ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat)) := by simp only [MState.exp_val_ℂ, Matrix.smul_mul, Matrix.sub_mul, Matrix.trace_smul, @@ -210,7 +175,6 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : 2 * (Complex.I * Complex.I) * (z.im : ℂ) by ring, Complex.I_mul_I] ring rw [commExpVal, hval, Complex.ofReal_re] - -- Combine Cauchy–Schwarz with `Im z ^ 2 ≤ ‖z‖ ^ 2`. have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply] have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by @@ -222,25 +186,17 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr _ = ρ.variance G * ρ.variance O := hprodsq -/-! ## The quantum Cramér--Rao bound -/ +/-! ## Normalized form (uncertainty principle) -/ -/-- **The quantum Cramér--Rao bound**, in unitary parametrization, under the usual local -unbiasedness normalization `⟨i[G,O]⟩_ρ = 1`. -/ -theorem cramerRao_unitary (G O : HermitianMat d ℂ) - (hG : 0 < ρ.variance G) (hnorm : ρ.commExpVal G O = 1) : - 1 / (4 * ρ.variance G) ≤ ρ.variance O := by +/-- Robertson's uncertainty relation in **multiplicative form**: under the normalization +`⟨i[G,O]⟩_ρ = 1`, the product of variances is at least `1/4`. This form needs no separate +positivity hypothesis and automatically excludes zero variance. -/ +theorem robertson_normalized (G O : HermitianMat d ℂ) + (hnorm : ρ.commExpVal G O = 1) : + 1 ≤ 4 * ρ.variance O * ρ.variance G := by have hR := ρ.robertson_uncertainty G O - rw [hnorm] at hR - norm_num at hR - rw [div_le_iff₀ (by positivity)] - nlinarith [hR, ρ.variance_nonneg O] - -/-- Pure-state specialization: `4 · Var_ρ(G)` is the quantum Fisher information of a unitary -family, giving the Mandelstam--Tamm form of the quantum Cramér--Rao bound. -/ -theorem cramerRao_pure_unitary {ψ : Ket d} (G O : HermitianMat d ℂ) - (hG : 0 < (MState.pure ψ).variance G) (hnorm : (MState.pure ψ).commExpVal G O = 1) : - 1 / (4 * (MState.pure ψ).variance G) ≤ (MState.pure ψ).variance O := - (MState.pure ψ).cramerRao_unitary G O hG hnorm + rw [hnorm] at hR; norm_num at hR + nlinarith [ρ.variance_nonneg G, ρ.variance_nonneg O] end observables diff --git a/QuantumInfo/States/Mixed/MState.lean b/QuantumInfo/States/Mixed/MState.lean index 2d9b5e7a4..eb553970d 100644 --- a/QuantumInfo/States/Mixed/MState.lean +++ b/QuantumInfo/States/Mixed/MState.lean @@ -260,6 +260,40 @@ theorem exp_val_le_exp_val (ρ : MState d) {A B : HermitianMat d ℂ} (h : A ≤ simp only [MState.exp_val] refine inner_mono ρ.nonneg h +/-- `exp_val_ℂ` on a Hermitian matrix is real, and equal to `exp_val`. -/ +@[simp] +theorem exp_val_ℂ_hermitian (A : HermitianMat d ℂ) : + ρ.exp_val_ℂ A.mat = (ρ.exp_val A : ℂ) := by + have hreal : (starRingEnd ℂ) (ρ.exp_val_ℂ A.mat) = ρ.exp_val_ℂ A.mat := by + simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose, + Matrix.conjTranspose_mul, ρ.Hermitian.eq, (A.H).eq] + rw [Matrix.trace_mul_comm] + have hre : (ρ.exp_val_ℂ A.mat).re = ρ.exp_val A := by + simp only [MState.exp_val_ℂ, MState.exp_val, HermitianMat.inner_eq_re_trace, MState.mat_M] + rw [Matrix.trace_mul_comm] + simp + rw [← hre] + exact (Complex.conj_eq_iff_re.mp hreal).symm + +/-- The **variance** of a Hermitian observable `A` on the state `ρ`. -/ +def variance (A : HermitianMat d ℂ) : ℝ := + ρ.exp_val (A ^ 2) - (ρ.exp_val A) ^ 2 + +/-- `Var_ρ(A) ≥ 0`. -/ +theorem variance_nonneg (A : HermitianMat d ℂ) : 0 ≤ ρ.variance A := by + set μ := ρ.exp_val A + have hsq : (A - μ • (1 : HermitianMat d ℂ)) ^ 2 = + A ^ 2 - (2 * μ) • A + μ ^ 2 • (1 : HermitianMat d ℂ) := by + ext1 + simp only [HermitianMat.mat_pow, HermitianMat.mat_sub, HermitianMat.mat_smul, + HermitianMat.mat_add, HermitianMat.mat_one, pow_two] + rw [sub_mul, mul_sub, mul_sub] + simp only [mul_smul_comm, smul_mul_assoc, mul_one, one_mul, smul_smul] + module + have h := ρ.exp_val_nonneg (T := (A - μ • 1) ^ 2) HermitianMat.sq_nonneg + rw [hsq, exp_val_add, exp_val_sub, exp_val_smul, exp_val_smul, exp_val_one] at h + unfold variance; linarith + end exp_val section pure From f00dda307312a982382428c5ca290000bf28b693 Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Fri, 4 Sep 2026 12:16:43 -0600 Subject: [PATCH 6/9] refactor(QuantumInfo): eliminate sqrtMat and commExpVal per review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drop sqrtMat wrapper — use ρ.M.sqrt directly from HermitianMat.Sqrt API. Replace commExpVal with Bracket instance on HermitianMat (⁅G, O⁆ = i(GO − OG)), so the theorem reads ρ.exp_val ⁅G, O⁆. Add section note explaining why hsVec (the HS embedding) is still needed. Warm up module docstring. Co-Authored-By: Claude Opus 4.6 --- .../Measurements/RobertsonUncertainty.lean | 133 ++++++++++-------- 1 file changed, 78 insertions(+), 55 deletions(-) diff --git a/QuantumInfo/Measurements/RobertsonUncertainty.lean b/QuantumInfo/Measurements/RobertsonUncertainty.lean index 2b49e6c2b..2a42b3613 100644 --- a/QuantumInfo/Measurements/RobertsonUncertainty.lean +++ b/QuantumInfo/Measurements/RobertsonUncertainty.lean @@ -1,28 +1,33 @@ /- -Copyright (c) 2026 Eduardo Nava-Hernandez. All rights reserved. +Copyright (c) 2026 Eduardo Nava-Hernández. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Eduardo Nava-Hernandez +Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava-Gómez (B-ACQM, 2026) -/ module public import QuantumInfo.States.Mixed.MState +public import QuantumInfo.ForMathlib.HermitianMat.Sqrt public import Mathlib.Analysis.InnerProductSpace.PiL2 +public import Mathlib.Data.Bracket /-! -# Robertson's uncertainty relation for mixed states +# Robertson's uncertainty relation for mixed quantum states -Robertson's uncertainty relation (H. P. Robertson, *The Uncertainty Principle*, Phys. Rev. **34**, -163–164 (1929)) bounds the product of variances of two Hermitian observables by a quarter of the -squared commutator expectation: +In 1929, H. P. Robertson showed that two Hermitian observables on a quantum state satisfy a +fundamental trade-off: the sharper you know one, the less you can know of the other. Formally, +for observables `G` and `O` and a state `ρ`: ⟨i[G,O]⟩² / 4 ≤ Var(G) · Var(O). -This file proves the relation for arbitrary finite-dimensional mixed states (`MState`) via -Cauchy–Schwarz on the Hilbert–Schmidt space. The main result is `robertson_uncertainty`. +We prove this for arbitrary finite-dimensional mixed states (`MState`) via Cauchy-Schwarz on the +Hilbert-Schmidt space. The main result is `robertson_uncertainty`. -As a corollary, `robertson_normalized` gives the equivalent multiplicative form -`1 ≤ 4 · Var(O) · Var(G)` under the normalization `⟨i[G,O]⟩ = 1`, without requiring a -separate positivity hypothesis. +The corollary `robertson_normalized` gives the multiplicative form `1 ≤ 4 · Var(O) · Var(G)` +under `⟨i[G,O]⟩ = 1`, free of positivity hypotheses. + +## References + +* H. P. Robertson, *The Uncertainty Principle*, Phys. Rev. **34**, 163-164 (1929) -/ @[expose] public section @@ -31,11 +36,36 @@ noncomputable section open scoped ComplexConjugate Matrix +/-! ## Commutator bracket on Hermitian matrices -/ + +namespace HermitianMat + +variable {d : Type*} [Fintype d] [DecidableEq d] + +instance : Bracket (HermitianMat d ℂ) (HermitianMat d ℂ) where + bracket G O := ⟨Complex.I • (G.mat * O.mat - O.mat * G.mat), by + show (Complex.I • (G.mat * O.mat - O.mat * G.mat))ᴴ = _ + rw [Matrix.conjTranspose_smul, Matrix.conjTranspose_sub, Matrix.conjTranspose_mul, + Matrix.conjTranspose_mul, G.H.eq, O.H.eq, Complex.star_def, Complex.conj_I] + module⟩ + +omit [DecidableEq d] in +@[simp] +theorem bracket_mat (G O : HermitianMat d ℂ) : + ⁅G, O⁆.mat = Complex.I • (G.mat * O.mat - O.mat * G.mat) := by + simp only [Bracket.bracket]; rfl + +end HermitianMat + namespace MState variable {d : Type*} [Fintype d] [DecidableEq d] -/-! ## Hilbert–Schmidt embedding -/ +/-! ## Hilbert-Schmidt embedding + +Cauchy-Schwarz is applied to `Tr(G O ρ)`, which requires embedding matrices into an inner +product space via `hsVec`. The HermitianMat inner product (`Tr(AB)`) gives a different bilinear +form and does not suffice for this argument. -/ private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2) @@ -54,54 +84,46 @@ private lemma hsVec_inner (A B : Matrix d d ℂ) : refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ exact mul_comm _ _ -/-! ## Hilbert–Schmidt centered vectors and the commutator pairing -/ +/-! ## Centered vectors and the commutator pairing -/ section observables variable (ρ : MState d) -private def sqrtMat : Matrix d d ℂ := ρ.M.sqrt.mat - -private lemma sqrtMat_isHermitian : (ρ.sqrtMat).IsHermitian := ρ.M.sqrt.H - -private lemma sqrtMat_mul_self : ρ.sqrtMat * ρ.sqrtMat = ρ.m := by - show ρ.M.sqrt.mat * ρ.M.sqrt.mat = ρ.m - simp [HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M] - -private lemma trace_sandwich (X : Matrix d d ℂ) : - (ρ.sqrtMat * X * ρ.sqrtMat).trace = (X * ρ.m).trace := by - rw [Matrix.trace_mul_cycle, ρ.sqrtMat_mul_self, Matrix.trace_mul_comm] +private lemma trace_sqrt_sandwich (X : Matrix d d ℂ) : + (ρ.M.sqrt.mat * X * ρ.M.sqrt.mat).trace = (X * ρ.m).trace := by + rw [Matrix.trace_mul_cycle, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M, + Matrix.trace_mul_comm] private lemma inner_sqrt_left (A : HermitianMat d ℂ) : - inner ℂ (hsVec ρ.sqrtMat) (hsVec (A.mat * ρ.sqrtMat)) = (ρ.exp_val A : ℂ) := by - rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, - show ρ.sqrtMat * (A.mat * ρ.sqrtMat) = ρ.sqrtMat * A.mat * ρ.sqrtMat by + inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec (A.mat * ρ.M.sqrt.mat)) = (ρ.exp_val A : ℂ) := by + rw [hsVec_inner, ρ.M.sqrt.H.eq, + show ρ.M.sqrt.mat * (A.mat * ρ.M.sqrt.mat) = ρ.M.sqrt.mat * A.mat * ρ.M.sqrt.mat by simp [Matrix.mul_assoc], - ρ.trace_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] + ρ.trace_sqrt_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] -private lemma inner_sqrt_self : inner ℂ (hsVec ρ.sqrtMat) (hsVec ρ.sqrtMat) = (1 : ℂ) := by - rw [hsVec_inner, ρ.sqrtMat_isHermitian.eq, ρ.sqrtMat_mul_self, ρ.tr'] +private lemma inner_sqrt_self : + inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec ρ.M.sqrt.mat) = (1 : ℂ) := by + rw [hsVec_inner, ρ.M.sqrt.H.eq, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M, ρ.tr'] private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : - inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec (O.mat * ρ.sqrtMat)) = + inner ℂ (hsVec (G.mat * ρ.M.sqrt.mat)) (hsVec (O.mat * ρ.M.sqrt.mat)) = ρ.exp_val_ℂ (G.mat * O.mat) := by - rw [hsVec_inner, Matrix.conjTranspose_mul, ρ.sqrtMat_isHermitian.eq, (G.H).eq, - show ρ.sqrtMat * G.mat * (O.mat * ρ.sqrtMat) = ρ.sqrtMat * (G.mat * O.mat) * ρ.sqrtMat by + rw [hsVec_inner, Matrix.conjTranspose_mul, ρ.M.sqrt.H.eq, (G.H).eq, + show ρ.M.sqrt.mat * G.mat * (O.mat * ρ.M.sqrt.mat) = + ρ.M.sqrt.mat * (G.mat * O.mat) * ρ.M.sqrt.mat by simp [Matrix.mul_assoc], - ρ.trace_sandwich, ← exp_val_ℂ] - -/-- The **commutator pairing** `⟨i[G,O]⟩_ρ` of two Hermitian observables. -/ -def commExpVal (G O : HermitianMat d ℂ) : ℝ := - (ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat))).re + ρ.trace_sqrt_sandwich, ← exp_val_ℂ] private def centeredVec (A : HermitianMat d ℂ) : EuclideanSpace ℂ (d × d) := - hsVec (A.mat * ρ.sqrtMat) - (ρ.exp_val A : ℂ) • hsVec ρ.sqrtMat + hsVec (A.mat * ρ.M.sqrt.mat) - (ρ.exp_val A : ℂ) • hsVec ρ.M.sqrt.mat private lemma norm_centered_sq (A : HermitianMat d ℂ) : ‖ρ.centeredVec A‖ ^ 2 = ρ.variance A := by have hself := ρ.inner_sqrt_self have hleft := ρ.inner_sqrt_left A - have hright : inner ℂ (hsVec (A.mat * ρ.sqrtMat)) (hsVec ρ.sqrtMat) = (ρ.exp_val A : ℂ) := by + have hright : inner ℂ (hsVec (A.mat * ρ.M.sqrt.mat)) (hsVec ρ.M.sqrt.mat) = + (ρ.exp_val A : ℂ) := by rw [← inner_conj_symm, hleft, Complex.conj_ofReal] have hAA := ρ.inner_hsVec_hsVec A A have hAsq : ρ.exp_val_ℂ (A.mat * A.mat) = (ρ.exp_val (A ^ 2) : ℂ) := by @@ -133,7 +155,8 @@ private lemma inner_centered_centered (G O : HermitianMat d ℂ) : have hself := ρ.inner_sqrt_self have hGl := ρ.inner_sqrt_left G have hOl := ρ.inner_sqrt_left O - have hGr : inner ℂ (hsVec (G.mat * ρ.sqrtMat)) (hsVec ρ.sqrtMat) = (ρ.exp_val G : ℂ) := by + have hGr : inner ℂ (hsVec (G.mat * ρ.M.sqrt.mat)) (hsVec ρ.M.sqrt.mat) = + (ρ.exp_val G : ℂ) := by rw [← inner_conj_symm, hGl, Complex.conj_ofReal] have hGO := ρ.inner_hsVec_hsVec G O unfold centeredVec @@ -141,11 +164,11 @@ private lemma inner_centered_centered (G O : HermitianMat d ℂ) : Complex.conj_ofReal, hself, hOl, hGr, hGO] ring -/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163–164 (1929)), +/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163-164 (1929)), for two Hermitian observables on an arbitrary finite-dimensional state: the product of variances dominates a quarter of the squared commutator pairing. -/ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : - (ρ.commExpVal G O) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by + (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by set z : ℂ := inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) with hz have hCS : ‖z‖ ≤ ‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖ := norm_inner_le_norm _ _ have hprodsq : (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 = ρ.variance G * ρ.variance O := by @@ -157,31 +180,32 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : rw [hz]; exact ρ.inner_centered_centered G O rw [hzz, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_ofReal, ρ.exp_val_ℂ_swap] ring - have hlin : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = + have hlin : ρ.exp_val_ℂ ⁅G, O⁆.mat = Complex.I * (ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat)) := by - simp only [MState.exp_val_ℂ, Matrix.smul_mul, Matrix.sub_mul, Matrix.trace_smul, - Matrix.trace_sub, smul_eq_mul] + rw [HermitianMat.bracket_mat] + simp only [MState.exp_val_ℂ, Matrix.smul_mul, Matrix.sub_mul, + Matrix.trace_smul, Matrix.trace_sub, smul_eq_mul] have hw : z - conj z = 2 * Complex.I * (z.im : ℂ) := by apply Complex.ext · simp [Complex.sub_re, Complex.conj_re, Complex.mul_re, Complex.mul_im] · simp [Complex.sub_im, Complex.conj_im, Complex.mul_re, Complex.mul_im] ring - have hcomm : ρ.commExpVal G O = -2 * z.im := by - have hval : ρ.exp_val_ℂ (Complex.I • (G.mat * O.mat - O.mat * G.mat)) = - ((-2 * z.im : ℝ) : ℂ) := by + have hcomm : ρ.exp_val ⁅G, O⁆ = -2 * z.im := by + have hval : ρ.exp_val_ℂ ⁅G, O⁆.mat = ((-2 * z.im : ℝ) : ℂ) := by rw [hlin, ← hz_sub, hw] push_cast rw [show Complex.I * (2 * Complex.I * (z.im : ℂ)) = 2 * (Complex.I * Complex.I) * (z.im : ℂ) by ring, Complex.I_mul_I] ring - rw [commExpVal, hval, Complex.ofReal_re] + rw [show ρ.exp_val ⁅G, O⁆ = (ρ.exp_val_ℂ ⁅G, O⁆.mat).re from by + rw [exp_val_ℂ_hermitian]; simp, hval, Complex.ofReal_re] have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply] have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by rw [hnormsq, sq]; nlinarith [sq_nonneg z.re] - have hfinal : (ρ.commExpVal G O) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by + have hfinal : (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by rw [hcomm]; nlinarith [hzim] - calc (ρ.commExpVal G O) ^ 2 / 4 + calc (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ‖z‖ ^ 2 := hfinal _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr _ = ρ.variance G * ρ.variance O := hprodsq @@ -189,10 +213,9 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : /-! ## Normalized form (uncertainty principle) -/ /-- Robertson's uncertainty relation in **multiplicative form**: under the normalization -`⟨i[G,O]⟩_ρ = 1`, the product of variances is at least `1/4`. This form needs no separate -positivity hypothesis and automatically excludes zero variance. -/ +`⟨i[G,O]⟩_ρ = 1`, the product of variances is at least `1/4`. -/ theorem robertson_normalized (G O : HermitianMat d ℂ) - (hnorm : ρ.commExpVal G O = 1) : + (hnorm : ρ.exp_val ⁅G, O⁆ = 1) : 1 ≤ 4 * ρ.variance O * ρ.variance G := by have hR := ρ.robertson_uncertainty G O rw [hnorm] at hR; norm_num at hR From 6d10d96c5b4021df3f91ce4d201631383938fa43 Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Mon, 7 Sep 2026 14:30:12 -0600 Subject: [PATCH 7/9] style: trim Authors line to comply with 100-char lint limit Co-Authored-By: Claude Opus 4.6 --- QuantumInfo/Measurements/RobertsonUncertainty.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/QuantumInfo/Measurements/RobertsonUncertainty.lean b/QuantumInfo/Measurements/RobertsonUncertainty.lean index 2a42b3613..01e2d973a 100644 --- a/QuantumInfo/Measurements/RobertsonUncertainty.lean +++ b/QuantumInfo/Measurements/RobertsonUncertainty.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Eduardo Nava-Hernández. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava-Gómez (B-ACQM, 2026) +Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava-Gómez -/ module From 26863f7239e30d0fd13ef836f3b16a9104ec48d3 Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Tue, 8 Sep 2026 07:42:42 -0600 Subject: [PATCH 8/9] refactor(QuantumMechanics): move mixed-state Robertson into Physlib Per jstoobysmith's review on PR #1587, relocate the mixed-state Robertson uncertainty relation from QuantumInfo/Measurements into Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean, next to the existing pure-state Robertson bounds in Operators/Uncertainty.lean. - New file Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean (Bracket instance, Hilbert-Schmidt embedding, robertson_uncertainty, robertson_normalized), with Physlib-style header/sections and the robertson1929uncertainty reference key. - Delete QuantumInfo/Measurements/RobertsonUncertainty.lean and its import in QuantumInfo.lean; keep MState helpers (exp_val_C_hermitian, variance, variance_nonneg) in MState.lean per Timeroot's points 2/4. - Register the file in Physlib.lean (sorted) and Operators/API-map.yaml. Physlib already imports QuantumInfo.ForMathlib (precedent: StatisticalMechanics/MicroCanonicalEnsemble/ThermoQuantities), so the QuantumInfo.States.Mixed.MState import introduces no import cycle. lake build OK (9355 jobs); check_file_imports, check_dup_tags, sorry_lint and runPhyslibLinters all pass. Co-Authored-By: Kimi --- Physlib.lean | 1 + .../QuantumMechanics/Operators/API-map.yaml | 4 + .../Operators/MixedStateUncertainty.lean | 83 ++++++++++++++----- QuantumInfo.lean | 1 - 4 files changed, 66 insertions(+), 23 deletions(-) rename QuantumInfo/Measurements/RobertsonUncertainty.lean => Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean (74%) diff --git a/Physlib.lean b/Physlib.lean index 6b52eeb7e..f5f5813b4 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -353,6 +353,7 @@ public import Physlib.QuantumMechanics.Operators.AngularMomentum public import Physlib.QuantumMechanics.Operators.Commutation public import Physlib.QuantumMechanics.Operators.Covariance public import Physlib.QuantumMechanics.Operators.Examples +public import Physlib.QuantumMechanics.Operators.MixedStateUncertainty public import Physlib.QuantumMechanics.Operators.Momentum public import Physlib.QuantumMechanics.Operators.Multiplication public import Physlib.QuantumMechanics.Operators.OneDimension.Commutation diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml index 6475f635e..6250ef21d 100644 --- a/Physlib/QuantumMechanics/Operators/API-map.yaml +++ b/Physlib/QuantumMechanics/Operators/API-map.yaml @@ -161,6 +161,10 @@ Requirements: done: true location: "Physlib/QuantumMechanics/Operators/Uncertainty.lean (centeredCommutatorExpectation, rawCommutatorExpectation, inner_centered_commutator_of_raw_commutator, state_uncertainty_squared_of_centered_commutator, state_uncertainty_squared_with_covariance_of_centered_commutator, state_uncertainty_of_centered_commutator, state_uncertainty_squared_of_raw_commutator, state_uncertainty_squared_with_covariance_of_raw_commutator, state_uncertainty_of_raw_commutator)" + - description: "Robertson's uncertainty relation for finite-dimensional mixed states (density matrices) is proved, in both the squared-commutator form and the multiplicative normalized form, via Cauchy-Schwarz on the Hilbert-Schmidt space." + done: true + location: "Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean (HermitianMat.bracket_mat, MState.robertson_uncertainty, MState.robertson_normalized)" + - description: "The API shall contain the Heisenberg uncertainty relation for position and momentum, that the product of the standard deviations of xᵢ and pᵢ in any unit state of a common domain is at least ℏ/2, which needs the position and momentum operators on a common domain before the present commutator can be fed into the present Robertson bound." done: false location: N/A diff --git a/QuantumInfo/Measurements/RobertsonUncertainty.lean b/Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean similarity index 74% rename from QuantumInfo/Measurements/RobertsonUncertainty.lean rename to Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean index 01e2d973a..841cb87d7 100644 --- a/QuantumInfo/Measurements/RobertsonUncertainty.lean +++ b/Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean @@ -11,23 +11,41 @@ public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Data.Bracket /-! -# Robertson's uncertainty relation for mixed quantum states +# Robertson's uncertainty relation for mixed states + +## i. Overview In 1929, H. P. Robertson showed that two Hermitian observables on a quantum state satisfy a -fundamental trade-off: the sharper you know one, the less you can know of the other. Formally, -for observables `G` and `O` and a state `ρ`: +fundamental trade-off: the sharper one observable is known, the less the other can be known. +Formally, for observables `G` and `O` on a state `ρ`: ⟨i[G,O]⟩² / 4 ≤ Var(G) · Var(O). -We prove this for arbitrary finite-dimensional mixed states (`MState`) via Cauchy-Schwarz on the -Hilbert-Schmidt space. The main result is `robertson_uncertainty`. +This module proves the relation for arbitrary finite-dimensional mixed states (`MState`), +via Cauchy–Schwarz on the Hilbert–Schmidt space. The pure-state version of this bound, for +partially defined operators on an inner product space, is in +`Physlib.QuantumMechanics.Operators.Uncertainty`; the mixed-state formulation here requires +the density-matrix framework of `MState`, which lives in `QuantumInfo`. + +## ii. Key results + +- `HermitianMat.bracket_mat` : the commutator bracket `⁅G, O⁆ = i(GO − OG)` on Hermitian + matrices. +- `MState.robertson_uncertainty` : Robertson's relation for mixed states. +- `MState.robertson_normalized` : the multiplicative form `1 ≤ 4 · Var(O) · Var(G)` under + the normalization `⟨i[G,O]⟩ = 1`, free of positivity hypotheses. -The corollary `robertson_normalized` gives the multiplicative form `1 ≤ 4 · Var(O) · Var(G)` -under `⟨i[G,O]⟩ = 1`, free of positivity hypotheses. +## iii. Table of contents -## References +- A. Commutator bracket on Hermitian matrices +- B. Hilbert–Schmidt embedding +- C. Centered vectors and the commutator pairing +- D. Robertson's uncertainty relation +- E. Normalized form -* H. P. Robertson, *The Uncertainty Principle*, Phys. Rev. **34**, 163-164 (1929) +## iv. References + +- [H. P. Robertson, *The Uncertainty Principle* (1929)][robertson1929uncertainty]. -/ @[expose] public section @@ -36,12 +54,14 @@ noncomputable section open scoped ComplexConjugate Matrix -/-! ## Commutator bracket on Hermitian matrices -/ - namespace HermitianMat variable {d : Type*} [Fintype d] [DecidableEq d] +/-! ## A. Commutator bracket on Hermitian matrices -/ + +/-- The commutator bracket `⁅G, O⁆ = i(GO − OG)` of two Hermitian matrices, as a +`HermitianMat`. -/ instance : Bracket (HermitianMat d ℂ) (HermitianMat d ℂ) where bracket G O := ⟨Complex.I • (G.mat * O.mat - O.mat * G.mat), by show (Complex.I • (G.mat * O.mat - O.mat * G.mat))ᴴ = _ @@ -61,12 +81,16 @@ namespace MState variable {d : Type*} [Fintype d] [DecidableEq d] -/-! ## Hilbert-Schmidt embedding +noncomputable section + +/-! ## B. Hilbert–Schmidt embedding -Cauchy-Schwarz is applied to `Tr(G O ρ)`, which requires embedding matrices into an inner -product space via `hsVec`. The HermitianMat inner product (`Tr(AB)`) gives a different bilinear -form and does not suffice for this argument. -/ +Cauchy–Schwarz is applied to `Tr(G O ρ)`, which requires embedding matrices into an inner +product space via `hsVec`. The HermitianMat inner product (`Tr(AB)`) gives a different +bilinear form and does not suffice for this argument. -/ +/-- The entries of a matrix, placed into `EuclideanSpace ℂ (d × d)` where Mathlib's inner +product space API (in particular Cauchy–Schwarz) is available. -/ private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) := (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2) @@ -75,6 +99,8 @@ omit [Fintype d] [DecidableEq d] in private lemma hsVec_apply (M : Matrix d d ℂ) (p : d × d) : hsVec M p = M p.1 p.2 := rfl omit [DecidableEq d] in +/-- The EuclideanSpace inner product of two embedded matrices is the Hilbert–Schmidt +pairing `Tr(Aᴴ B)`. -/ private lemma hsVec_inner (A B : Matrix d d ℂ) : inner ℂ (hsVec A) (hsVec B) = (Aᴴ * B).trace := by rw [PiLp.inner_apply, Fintype.sum_prod_type, Matrix.trace] @@ -84,17 +110,20 @@ private lemma hsVec_inner (A B : Matrix d d ℂ) : refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_ exact mul_comm _ _ -/-! ## Centered vectors and the commutator pairing -/ +/-! ## C. Centered vectors and the commutator pairing -/ section observables variable (ρ : MState d) +/-- The cyclic trace identity `Tr(√ρ X √ρ) = Tr(X ρ)`, the Hilbert–Schmidt engine of the +mixed-state calculation. -/ private lemma trace_sqrt_sandwich (X : Matrix d d ℂ) : (ρ.M.sqrt.mat * X * ρ.M.sqrt.mat).trace = (X * ρ.m).trace := by rw [Matrix.trace_mul_cycle, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M, Matrix.trace_mul_comm] +/-- The embedding of `A √ρ` against `√ρ` is the expectation value of `A`. -/ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec (A.mat * ρ.M.sqrt.mat)) = (ρ.exp_val A : ℂ) := by rw [hsVec_inner, ρ.M.sqrt.H.eq, @@ -102,10 +131,12 @@ private lemma inner_sqrt_left (A : HermitianMat d ℂ) : simp [Matrix.mul_assoc], ρ.trace_sqrt_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian] +/-- The embedded `√ρ` is a unit vector in Hilbert–Schmidt space. -/ private lemma inner_sqrt_self : inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec ρ.M.sqrt.mat) = (1 : ℂ) := by rw [hsVec_inner, ρ.M.sqrt.H.eq, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M, ρ.tr'] +/-- The embedding of `G √ρ` against `O √ρ` is the expectation value of the product `G O`. -/ private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : inner ℂ (hsVec (G.mat * ρ.M.sqrt.mat)) (hsVec (O.mat * ρ.M.sqrt.mat)) = ρ.exp_val_ℂ (G.mat * O.mat) := by @@ -115,9 +146,11 @@ private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) : simp [Matrix.mul_assoc], ρ.trace_sqrt_sandwich, ← exp_val_ℂ] +/-- The centered vector `A √ρ − ⟨A⟩ √ρ` in Hilbert–Schmidt space. -/ private def centeredVec (A : HermitianMat d ℂ) : EuclideanSpace ℂ (d × d) := hsVec (A.mat * ρ.M.sqrt.mat) - (ρ.exp_val A : ℂ) • hsVec ρ.M.sqrt.mat +/-- The squared Hilbert–Schmidt norm of the centered vector is the variance of `A`. -/ private lemma norm_centered_sq (A : HermitianMat d ℂ) : ‖ρ.centeredVec A‖ ^ 2 = ρ.variance A := by have hself := ρ.inner_sqrt_self @@ -139,8 +172,8 @@ private lemma norm_centered_sq (A : HermitianMat d ℂ) : rw [hre, hexpand, variance, hAsq, ← Complex.ofReal_mul, ← Complex.ofReal_sub, Complex.ofReal_re] ring -/-! ## Robertson's uncertainty relation -/ - +/-- The expectation of a product of Hermitian matrices is conjugate-symmetric in the +factors. -/ private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) : (starRingEnd ℂ) (ρ.exp_val_ℂ (G.mat * O.mat)) = ρ.exp_val_ℂ (O.mat * G.mat) := by simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose] @@ -149,6 +182,8 @@ private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) : (O.H).eq, ← Matrix.mul_assoc], Matrix.mul_assoc, Matrix.trace_mul_comm] +/-- The inner product of the centered vectors of `G` and `O` is the covariance pairing +`⟨GO⟩ − ⟨G⟩⟨O⟩`. -/ private lemma inner_centered_centered (G O : HermitianMat d ℂ) : (inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) : ℂ) = ρ.exp_val_ℂ (G.mat * O.mat) - (ρ.exp_val G : ℂ) * (ρ.exp_val O : ℂ) := by @@ -164,9 +199,11 @@ private lemma inner_centered_centered (G O : HermitianMat d ℂ) : Complex.conj_ofReal, hself, hOl, hGr, hGO] ring -/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163-164 (1929)), -for two Hermitian observables on an arbitrary finite-dimensional state: the product of variances -dominates a quarter of the squared commutator pairing. -/ +/-! ## D. Robertson's uncertainty relation -/ + +/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163–164 (1929)), +for two Hermitian observables on an arbitrary finite-dimensional mixed state: the product of +variances dominates a quarter of the squared commutator pairing. -/ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by set z : ℂ := inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) with hz @@ -210,7 +247,7 @@ theorem robertson_uncertainty (G O : HermitianMat d ℂ) : _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr _ = ρ.variance G * ρ.variance O := hprodsq -/-! ## Normalized form (uncertainty principle) -/ +/-! ## E. Normalized form -/ /-- Robertson's uncertainty relation in **multiplicative form**: under the normalization `⟨i[G,O]⟩_ρ = 1`, the product of variances is at least `1/4`. -/ @@ -223,6 +260,8 @@ theorem robertson_normalized (G O : HermitianMat d ℂ) end observables +end + end MState end diff --git a/QuantumInfo.lean b/QuantumInfo.lean index 826d19190..6fa9744d9 100644 --- a/QuantumInfo.lean +++ b/QuantumInfo.lean @@ -42,7 +42,6 @@ public import QuantumInfo.Entropy.DPI public import QuantumInfo.States.Mixed.MState public import QuantumInfo.Channels.Pinching public import QuantumInfo.Measurements.POVM -public import QuantumInfo.Measurements.RobertsonUncertainty public import QuantumInfo.Operators.Unitary --Documentation without code From 3e1926695ebddf1e68aa1b0663f66a46db70ab8b Mon Sep 17 00:00:00 2001 From: Eduardo Nava-Hernandez Date: Tue, 8 Sep 2026 08:16:33 -0600 Subject: [PATCH 9/9] fix(Relativity): drop simp attr from Matrix.trace_reindex The mixed-state Robertson file pulls QuantumInfo.ForMathlib.Matrix into the Physlib root environment, where its @[simp] Matrix.trace_submatrix subsumes Matrix.trace_reindex. The simpNF linter then flags trace_reindex as provable by simp. The lemma has no simp users (only one explicit erw), so keep it as a plain lemma for that rewrite instead of a duplicate simp lemma. lake build OK (9355 jobs); runPhyslibLinters passes for Physlib and QuantumInfo. Co-Authored-By: Kimi --- Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean index 3b2b8b639..be63ab5e1 100644 --- a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean +++ b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean @@ -105,7 +105,6 @@ namespace Matrix variable {n R ι : Type*} [Fintype n]-- [DecidableEq n] -@[simp] lemma trace_reindex [Semiring R] [Fintype ι] (e : n ≃ ι) (A : Matrix n n R) : trace (A.submatrix e.symm e.symm) = trace A := by simp only [trace, diag_apply, submatrix_apply]