feat(QuantumInfo): Robertson uncertainty relation for mixed states

[naype888-cloud]

feat(QuantumInfo): Robertson uncertainty relation for mixed states

Proves Robertson's uncertainty relation (1929) for two Hermitian observables on an arbitrary
finite-dimensional mixed state (MState), via Cauchy–Schwarz on the Hilbert–Schmidt space.
Single new file plus its import line, and three helper lemmas on MState.

t-quantum-info

Files

• QuantumInfo/Measurements/RobertsonUncertainty.lean — new file, 228 lines.
• QuantumInfo.lean — one public import line for the new module (kept sorted).
• QuantumInfo/States/Mixed/MState.lean — three helper lemmas (exp_val_ℂ_hermitian, variance, variance_nonneg).

Definitions added

All in QuantumInfo/Measurements/RobertsonUncertainty.lean.

Name	Meaning
HermitianMat.Bracket	Commutator bracket ⁅G, O⁆ = i(GO − OG) as a HermitianMat.
MState.hsVec	(private) Hilbert–Schmidt embedding of a matrix into EuclideanSpace ℂ (d × d).
MState.centeredVec	(private) The centered vector A √ρ − ⟨A⟩ √ρ in Hilbert–Schmidt space.

Theorems

Name	Statement
robertson_uncertainty	For Hermitian G, O on a mixed state ρ: ⟨i[G,O]⟩² / 4 ≤ Var(G) · Var(O). (H. P. Robertson, Phys. Rev. 34, 163–164 (1929).)
robertson_normalized	Under the normalization ⟨i[G,O]⟩ = 1: 1 ≤ 4 · Var(O) · Var(G). Free of positivity hypotheses.

Proof strategy

Embed √ρ and A√ρ into EuclideanSpace ℂ (d × d) (the Hilbert–Schmidt space), form the
centered vector A√ρ − ⟨A⟩√ρ, show its squared norm is the variance, then apply Cauchy–Schwarz
to the pair of centered vectors. The imaginary part of the inner product recovers the commutator
expectation.

On hsVec vs Matrix.toEuclideanLin

hsVec is a deliberately minimal wrapper placing matrix entries into EuclideanSpace ℂ (d × d).
Using Mathlib's Matrix.toEuclideanLin would pull in an additional [DecidableEq d] threading
beyond what is already needed for the commutator bracket. Happy to switch if reviewers prefer.

References

• H. P. Robertson, The Uncertainty Principle, Phys. Rev. 34, 163–164 (1929)

AI disclosure

AI-assisted (Claude). The author has certified every definition, theorem statement, and proof
step, and has personally verified the bibliographic references.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[jstoobysmith]

@Timeroot would you be able to review this PR?

[Timeroot]

I think the main thing is that this should be done for MState instead. You'll find it has a lot more of the API you want already there.

[Timeroot]

This can use ketToEuclidean in Braket.lean, feel free to make that non-private. Same for the two lemmas below.

[Timeroot]

I'm not sure this definition should exist, but if it should, it should go in another file!

[Timeroot]

Down to here, all in another file if keeping at all.

[Timeroot]

You know I think actually this whole thing can be done for mixed states, which easily generalized the Ket formulation. I don't think it's any more mathematically complicated. These values like expValC are just restating the specialization for MState.expValC, and so you might as well go that route!

[Timeroot]

This type of inner ℂ and starRingEnd ℂ notation is much much more verbose than it needs to be. I think most of this could be done much shorter.

Really this whole proof could likely be golfed down..

[naype888-cloud]

Thanks, this makes sense. I reworked the file around `MState` instead of the pure-state `Ket` formulation. The auxiliary `Ket.toEuclideanSpace`, `Matrix.onVec`, and `Ket.expValC` definitions are gone; the result now uses the existing `MState.exp_val_ℂ` / `MState.exp_val` API and proves Robertson directly for mixed states, with the pure-state Cramér–Rao statement as a specialization.

…

On Sat, Aug 29, 2026 at 2:26 PM Alex Meiburg ***@***.***> wrote: ***@***.**** commented on this pull request. I think the main thing is that this should be done for MState instead. You'll find it has a lot more of the API you want already there. ------------------------------ In QuantumInfo/Measurements/CramerRao.lean <#1587 (comment)> : > +## C. The quantum Cramér–Rao bound +-/ + ***@***.*** 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 := This can use ketToEuclidean in Braket.lean, feel free to make that non-private. Same for the two lemmas below. ------------------------------ In QuantumInfo/Measurements/CramerRao.lean <#1587 (comment)> : > + ψ.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 ***@***.***_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 := I'm not sure this definition should exist, but if it should, it should go in another file! ------------------------------ In QuantumInfo/Measurements/CramerRao.lean <#1587 (comment)> : > + 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) Down to here, all in another file if keeping at all. ------------------------------ In QuantumInfo/Measurements/CramerRao.lean <#1587 (comment)> : > +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 ℂ) : ℂ := You know I think actually this whole thing can be done for mixed states, which easily generalized the Ket formulation. I don't think it's any more mathematically complicated. These values like expValC are just restating the specialization for MState.expValC, and so you might as well go that route! ------------------------------ In QuantumInfo/Measurements/CramerRao.lean <#1587 (comment)> : > +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) : ℂ) - This type of inner ℂ and starRingEnd ℂ notation is much much more verbose than it needs to be. I think most of this could be done much shorter. Really this whole proof could likely be golfed down.. — Reply to this email directly, view it on GitHub <#1587?email_source=notifications&email_token=B5YMS3ZNEUUNWYWEXF3ZAFD5MM4APA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBVHEYDONRQGMY2M4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KYZTPN52GK4S7MNWGSY3L#pullrequestreview-5059076031>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/B5YMS356MIXPBUNGPQ537SL5MM4APAVCNFSNUABFKJSXA33TNF2G64TZHM3TQNZVG42DSNZYHNEXG43VMU5TKMRYGQ4DCMZZGE2KC5QC> . Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/B5YMS37ZQ5WTR76U4VKS45D5MM4APA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBVHEYDONRQGMY2M4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2KUZTPN52GK4S7NFXXG> and Android <https://github.com/notifications/mobile/android/B5YMS3ZHLNUGGFMNYHZRTVT5MM4APA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBVHEYDONRQGMY2M4TFMFZW63VGMF2XI2DPOKSWK5TFNZ2K4ZTPN52GK4S7MFXGI4TPNFSA>. Download it today! You are receiving this because you authored the thread.Message ID: <leanprover-community/physlib/pull/1587/review/5059076031 ***@***.***>

[Timeroot]

1. There's no need for hsVec, there's already an inner product space API on HermitianMat that is exactly what you're asking for.
2. exp_val_ℂ_hermitian should go shortly after the definition of exp_val_ℂ in MState.lean, I would say, and probably be marked simp. I'm also sure it can be a shorter proof.
3. I don't think the definition sqrtMat should exist. Note that some of the facts you prove about it (trace_sandwich, inner_sqrt_left, etc.) hold for any PSD HermitianMat, not just a ρ.H. (That is: the fact that it's trace one is not being used here.) Try to factor out where possible.
4. MState.variance is a good definition and belongs in MState near MState.exp_val. Put variance_nonneg with it. Would be nice if it could be a positivityExt but no pressure.
5. comm_exp_val shouldn't exist as a definition. There should be a definition of commutator on HermitianMat that gives another HermitianMat, if there's not yet; this would be an instance : Bracket HermitianMat I think. Then you just have rho.exp_val \bracketLeft G, O \bracketRight.
6. Instead of stating cramerRao_unitary as 1 / (4 * ρ.variance G) ≤ ρ.variance O with a hypothesis the denominator is positive, use 1 ≤ 4 * ρ.variance O * ρ.variance G. Then, no positivity hypotheses needed! This is stronger, too, since it automatically excludes the case that the variances are zero.
7. The theorem cramerRao_unitary you have stated appears to just be the Heisenberg uncertainty principle. Nothing you mention in the docstring about exponentials or derivatives are actually there. I'd happily welcome this proof of the uncertainty principle, but this isn't Cramer-Rao as it stands.
8. I don't see a need to specialize to cramerRao_pure_unitary, it's literally the same exact signature but narrower. I think we can delete it.

[jstoobysmith]

@Timeroot do you think we are in a position to merge this?

[Timeroot]

@jstoobysmith No, at a minimum I'd need points 2, 4, 7 above addressed

[jstoobysmith]

Sorry my bad - presumed these where covered by the latest commit.

awaiting-author

[naype888-cloud]

Thanks for the thorough review — sorry for the delay getting back.

This commit addresses the points you flagged as minimum for merge:

• Point 2: exp_val_ℂ_hermitian moved to MState.lean, marked @[simp].
• Point 4: MState.variance and variance_nonneg now live in MState.lean next to exp_val. The nonnegativity proof goes through exp_val_nonneg on the centered observable (A − ⟨A⟩)².
• Point 7: File renamed to RobertsonUncertainty.lean, docstrings updated throughout — this is Robertson's uncertainty relation, not Cramér–Rao.
• Point 6: Added robertson_normalized stating 1 ≤ 4 * Var(O) * Var(G) under the normalization ⟨i[G,O]⟩ = 1, no positivity hypothesis.
• Point 8: cramerRao_pure_unitary deleted.

Still working on points 1, 3, 5 (replacing hsVec/sqrtMat with the existing HermitianMat inner product API, and the Bracket instance for the commutator). Will push a follow-up commit for those shortly.

-awaiting-author

[naype888-cloud]

Follow-up commit addressing the remaining points:

• Point 1 (hsVec): The Hilbert-Schmidt embedding stays because Cauchy-Schwarz needs Tr(GOρ), not Tr(GO) — the HermitianMat inner product gives the wrong bilinear form. Added a section note explaining this. Happy to discuss alternatives.
• Point 3 (sqrtMat): Eliminated. Now uses ρ.M.sqrt directly from HermitianMat.Sqrt — no private wrapper.
• Point 5 (commExpVal): Replaced with a Bracket (HermitianMat d ℂ) instance defining ⁅G, O⁆ = i(GO − OG). The theorem now reads ρ.exp_val ⁅G, O⁆ instead of ρ.commExpVal G O.

All 8 review points addressed. Build green (9257 jobs).

— Eduardo Nava-Hernández, B-ACQM 2026

[naype888-cloud]

"My English isn't great, but I'm uploading this code as the foundation for a theorem that already compiles in Lean 4. The setup requires a Cauchy-Robertson-Fiedler-Niven-Szego chain, so I’ll be validating whatever is missing along that chain until I can prove Nava-Robertson "dimensional uncertainty theorem" using those pillars. This is just one part of it, but I’ll be closing the gaps step by step. Once I have all the pieces in place, I’ll build the final theorem on top of them. Like I said, it already compiles and type-checks, but it’s still missing a canonical basis in several places. I've already fixed all the code style to match the requirements here."

[jstoobysmith]

Looking at this PR, it might also be suitable to go directly into ./Physlib, where a lot of the underlying quantities are already defined. e.g. in ./Physlib/QuantumMechanics/Operators where we already have variance etc.

[naype888-cloud]

Done — the mixed-state Robertson relation now lives in
Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean, alongside the pure-state bounds in
Uncertainty.lean, exactly where you suggested. The MState helpers (variance, variance_nonneg,
exp_val_ℂ_hermitian) stay next to exp_val in MState.lean per Timeroot's earlier points, and the file is
registered in the Operators API map. Build is green (9355 jobs) and every CI linter passes.

I'll be brief, because there is a large amount of mathematics still to be discharged: this PR is
deliberately one load-bearing pillar of a longer formal chain — Cauchy–Schwarz, Robertson, Fiedler, Niven,
Szegő — which I am validating incrementally, gap by gap, with the explicit goal of assembling the
elementary Nava–Robertson dimensional uncertainty theorem on top of exactly these pieces. Each merged
lemma is a fixed rung; the chain only gets shorter from here. If the review asks for more work on this PR,
it will get done — that is precisely what a theorem type-checker is for; Lean 4 is the force multiplier in
this pipeline. As stated before: it compiles, it type-checks, and the remaining gaps are a matter of time,
not of truth.

[jstoobysmith]

Sorry, I just realised there is this exact result here:

physlib/PhyslibAlpha/QuantumMechanics/OperatorAlgebra/States/Uncertainty.lean

Line 115 in d2159de

lemma robertson (ω : State A) (a b : Observable A) :

Are there any improvements you would want to include there?

You may also be interested in the following ongoing zulip

https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Integrating.20QuantumInfo/with/622475071

[naype888-cloud]

Thank you for pointing that out — the existing robertson in PhyslibAlpha/.../Uncertainty.lean is a great result. However, the two lemmas live in different generality:

	Existing State.robertson	This PR's MState.robertson_uncertainty
Domain	State A (abstract OperatorAlgebra)	MState d (density matrices, QuantumInfo)
States covered	Pure states	Arbitrary mixed states (convex combinations of pure states)
Proof engine	GNS Cauchy–Schwarz	Hilbert–Schmidt embedding + Cauchy–Schwarz

A pure state is a rank-1 density matrix; a mixed state is any positive semidefinite trace-1 matrix. Every pure-state bound follows from the mixed-state version (specialize to rank 1), but the converse does not hold — the density-matrix framework requires the √ρ-sandwich technique (Tr(√ρ · X · √ρ) = Tr(Xρ)) that has no analogue in the GNS argument.

Beyond the generalization itself, the PR also contributes:

• A Bracket instance on HermitianMat d ℂ (the Hermitian commutator ⁅G, O⁆ = i(GO − OG)), which is reusable infrastructure for future mixed-state results.
• robertson_normalized: the multiplicative form 1 ≤ 4 · Var(O) · Var(G) under ⟨i[G,O]⟩ = 1, convenient for applications where the commutator is pre-normalized (e.g., canonical pairs).

Happy to coordinate with the Zulip discussion on integrating QuantumInfo — if there is upstream work unifying State A and MState, this module would slot in naturally as the concrete finite-dimensional case.

[jstoobysmith]

Maybe it is worth posting a quick message on that zulip, to see what people think, and how to best implement this

[jstoobysmith]

So, if I understood the comments on the Zulip correctly, what we currently have actually does take account of mixed states.

[naype888-cloud]

sry guys i all ready fix the MSstates and the observation by timeroot and joseph, i shutdown this PR, and upload a newone attending your sugestions, this is the newone PR. #1676