feat: Hilbert space & unbounded operators on Space#957
feat: Hilbert space & unbounded operators on Space#957jstoobysmith merged 22 commits intoleanprover-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).
There was a problem hiding this comment.
What I mean is that I believe on a HilbertSpace (or some other common setting) any densely defined linear map is closable and so we don't need this as a separate assumption. I say this because I often see the existence of a closure be implicitly assumed in some references. Perhaps we leave this as is for now and see under what conditions closability is guaranteed and consider a refactor later.
| 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
| /-- 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.
What I mean is that I believe on a HilbertSpace (or some other common setting) any densely defined linear map is closable and so we don't need this as a separate assumption. I say this because I often see the existence of a closure be implicitly assumed in some references. Perhaps we leave this as is for now and see under what conditions closability is guaranteed and consider a refactor later.
| rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U†.dense_domain] | ||
| rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] | ||
| rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] |
|
I manually removed a couple extraneous blank lines that (hopefully) won't break anything, will approve after that. |
morrison-daniel
added
the
ready-to-merge
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
I’ve approved this aswell and will merge now
…ity#957) * d-dim Hilbert space * d-dim schwartz submodule * init progress on unbounded ops * init progress on unbounded ops * submodule lemmas * abstract away Hilbert space * linter fixes * sorry removed: closable => adjoint dense * sorry removed: symm + dense => closable * sorry-free * comments * UnboundedOperator extends LinearPMap * remove unnecessary coe * relocate submodule lemmas * style improvements * more improvements * extract adjoint_isClosable_dense * minor cleanup * lint fixes * Remove extra blank lines * Remove extra blank lines --------- Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
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.