feat: Hilbert space & unbounded operators on Space#957
feat: Hilbert space & unbounded operators on Space#957gloges wants to merge 20 commits intolean-phys-community:masterfrom
Conversation
|
Still more to do (e.g. products, x,p,L instances), but I think this is a good break point now that everything is sorry free. |
morrison-daniel
left a comment
morrison-daniel
left a comment
There was a problem hiding this comment.
Since you mentioned being a beginner I added quite a few comments to help with style and structure, but really it is quite good work. Feel free to comment/DM on Zulip if you have questions!
| /-- The domain of an unbounded operator is dense in the Hilbert space. -/ | ||
| dense_domain : Dense (domain : Set HS) | ||
| /-- An unbounded operator is closable. -/ | ||
| is_closable : toLinearPMap.IsClosable |
There was a problem hiding this comment.
I think this isn't necessary since dense_domain and CompleteSpace should guarantee this condition
There was a problem hiding this comment.
Closability is required for the adjoint to be densely defined and thus also of type UnboundedOperator (cf. Schmüdgen Theorem 1.8.i).
| instance : CoeFun (UnboundedOperator HS) | ||
| (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun'⟩ | ||
|
|
||
| lemma ext' (U T : UnboundedOperator HS) : U.toLinearPMap = T.toLinearPMap → U = T := by |
There was a problem hiding this comment.
[ext] attribute should auto-generate this lemma and the one below.
There was a problem hiding this comment.
The autogenerated ext lemma is (x.domain = y.domain) → (x.toFun ≍ y.toFun) → x = y and the HEq docs say to avoid it, so I think this is worth keeping.
PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
Outdated
Show resolved
Hide resolved
PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
Outdated
Show resolved
Hide resolved
PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
Outdated
Show resolved
Hide resolved
morrison-daniel
added
awaiting-author
|
Also, in general it is helpful for review to break up larger changes like this into multiple smaller PRs around 100-200 lines if you can. Don't worry about it for this one, but keep it in mind for the future. |
|
Thanks very much for the comprehensive feedback! I've extracted the submodule lemmas for getting the inner product structure onto the |
|
This looks good to me, but I think Daniel has now got a tighter control of this PR so will leave any final reviews to him. |
jstoobysmith
removed
the
awaiting-author
3 participants
Initial progress for single-particle QM on
Space d, addressing #851.SpaceDHilbertSpaceandSchwartzSubmodulecarry over from 1d with only minor changes (cf. OneDimension/HilbertSpace).UnboundedOperatoris defined using LinearPMap with additional density and closability hypotheses. Nothing inUnboundedOperatordepends on the particular Hilbert space and can be easily generalized in the future.A few sorries remain to be filled in; two I think I can do after understanding how to work with InnerProductSpace/PiL2.