feat(OperatorAlgebra): unitary one-parameter group automorphisms and Hamiltonian dynamics - #1607
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. |
jstoobysmith
added
ready-to-merge
|
This now has merge conflict (maybe I merged the wrong PR first, so this content might have been included with your other PR - sorry) |
… post-leanprover-community#1608 merge PR leanprover-community#1608 (reorganize states, observables, and measurement) merged into master first, and had independently moved Physlib/QuantumMechanics/OperatorAlgebra to PhyslibAlpha/QuantumMechanics/OperatorAlgebra (with a reorg splitting Observable/State/Effect/PositiveElement/POVM into their own files). PR leanprover-community#1607's branch had independently made the same folder move on top of the pre-reorg layout, producing "added in both" conflicts at the new PhyslibAlpha paths that git couldn't resolve as a 3-way merge. Rebuilds this branch on top of current master: - Basic.lean, HilbertSpace.lean, Observables/{Jordan,Lie}.lean under PhyslibAlpha/QuantumMechanics/OperatorAlgebra/ are left as master's post-reorg versions (PR leanprover-community#1607 never intended to touch them). - Dynamics/Automorphism.lean: master's current file plus PR leanprover-community#1607's unitary-automorphism-group additions (AutomorphismGroup structure, conjugation, the UnitaryOneParameterGroup.toAutomorphism construction and its differential/uniqueness characterization), with imports updated for the post-leanprover-community#1608 module layout (Observables.Lie now lives under PhyslibAlpha). - Dynamics/Hamiltonian.lean: new file, PR leanprover-community#1607's Hamiltonian dynamics content (unitaryEvolution, hamiltonianFlow, equivariance, Heisenberg equation, and the classification of Hamiltonians up to conjugation and scalar shift), with its Automorphism import updated to PhyslibAlpha. - Physlib/Mathematics/OneParameterSubgroups/Unitary.lean: adds commute_generator, hasDerivAt, hasDerivAt_star (unaffected by the folder move, applies cleanly on top of master). - PhyslibAlpha.lean: adds the missing import line for the new Dynamics.Hamiltonian module (Dynamics.Automorphism was already imported via leanprover-community#1608's merge). - Physlib.lean: unchanged (already has no OperatorAlgebra imports post-leanprover-community#1608). Verified: `lake build` (full) succeeds with 0 errors, and scripts/PhyslibAlpha/noAlphaImports.py reports no violations. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jv3aja8R6JnqJTvmsjuGxF
4a9a746 to
c98fc59
Compare
2 participants
Adds the automorphism-group action of a norm-continuous unitary one-parameter group on
B(H)by conjugation, proves it satisfies (and is the unique solution of) the Heisenberg equation of motion, and specializes this to Hamiltonian dynamicsU_H(t) = exp(-itH/ℏ), including the classification of when two Hamiltonians generate the same flows.Split out of #1590.
With the Discussion David Gross opened I expect some of these notions to be reworked in the future.
I wanted to get the code out there but can also put it into PhyslibAlpha if that is more appropriate.