States, expectation, and uncertainty relations - #1577
Conversation
|
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.
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. |
|
Maybe in this we can also subsume the definitions and lemmas within ./Operators/StateObservables/ where possible? |
|
Putting on awaiting-author for the comment above |
I dont think it is time for that. |
|
-awaiting-author |
Adds OperatorAlgebra.Measurement.State (expectation, centering, covariance, variance) and OperatorAlgebra.Measurement.Uncertainty (GNS Cauchy-Schwarz, Robertson-Schrodinger and Robertson uncertainty relations), built on the existing Jordan/Lie observable API. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ent/State.lean Basic.lean's own docstring already says elementary results about each notion should live in their own file; State's structure definition was left behind there instead. Move it into Measurement/State.lean, which already builds the expectation/covariance/variance API on top of it and had its own duplicate CoeFun instance — drop that duplicate now that the struct lives alongside it. Addresses jstoobysmith's review comment on removing overlap. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
3d14f7f to
0830bb8
Compare
jstoobysmith
left a comment
There was a problem hiding this comment.
One quick comment from me here.
There was a problem hiding this comment.
Should "State" really be under "Measurement"?
There was a problem hiding this comment.
I see what you mean. I’m using the Heisenberg view, where states act on observables by assigning expectation values, so grouping them with measurement seemed natural.
There was a problem hiding this comment.
Ok, can we put a comment to this effect in the doc-string?
|
awaiting-author |
|
-awaiting-author |
|
awaiting-author For the comment above. |
|
@TomOleDiem Just a ping about the comment above |
|
Superseded by #1590, which isolates the reviewed primitive API split. |
Adds states and the uncertainty relations built on the existing Jordan/Lie observable API.
OperatorAlgebra.Measurement.State: the expectation functionalω⟨a⟩, centering, covariance, and variance.OperatorAlgebra.Measurement.Uncertainty: the GNS Cauchy–Schwarz inequality for states, and the Robertson–Schrödinger and Robertson uncertainty relations.