feat: Hilbert space & unbounded operators on Space#957
Draft
gloges wants to merge 11 commits intolean-phys-community:masterfrom
Draft
feat: Hilbert space & unbounded operators on Space#957gloges wants to merge 11 commits intolean-phys-community:masterfrom
gloges wants to merge 11 commits intolean-phys-community:masterfrom
Conversation
| open LinearPMap | ||
|
|
||
| -- Nothing here uses any specific properties of this particular Hilbert space | ||
| abbrev hilbSp d := SpaceDHilbertSpace d |
Member
There was a problem hiding this comment.
Why do we need this abbreviation? If it is down to not wanting to write SpaceDHilbertSpace I think we should probably aim for notation
Contributor
Author
There was a problem hiding this comment.
Just a temporary abbreviation - all instances of SpaceDHilbertSpace are now removed for unbounded operators.
| so that `hilbSp × hilbSp` has the structure of an inner product space. | ||
| -/ | ||
|
|
||
| abbrev hilbSp2 (d : ℕ) := hilbSp d × hilbSp d |
Member
There was a problem hiding this comment.
Do you mean the tensor product here? If not maybe we could add a doc for why this is needed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.