Pull Request from sudhindu/Prove-It master branch #359
Conversation
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
Moved unitary_group.py and some theorems from linear_algebra.matrices to linear_algebra.matrices.transposition and added unitary_unitary_dag and unitary_dag_unitary.
Established Identity class and added . identity_def added in axioms also added to demonstration note book
…dded We updated in Qmult.py : added methods are adjoint_distribution and projection
Unitary and SpecialUnitary class move to new sub theory transposition from unitary_group package
…313-quantum_algebra_development
last update
Update InnerProdSpaces.yield_readily_provable_inner_prod_spaces() method to use set.intersection(), replace the apparently misleading 'K' with 'field', and clean up code (line lengths, comments, etc). This version has not been tested and is unlikely to work yet.
Update some assumptions in some of the notebook theorem-instantiation cells in quantum/algebra/demos to allow the notebook to run successfully. Added the extra assumption locally in a couple cells that InSet(ket_varphi, H); it might be that this assumption is better implemented at the top of the notebook in the defaults.assumptions. Related Issue: sandialabs#313.
Clean up proof of the qmult_of_bra_as_map theorem in the quantum/algebra package. This was already proven by Sudhindu and was just needing to have misc unnecessary imports and steps removed. Related Issue: sandialabs#313 .
Update InnerProdSpaces.yield_readily_provable_inner_prod_spaces() method to disclude an ExprTuple case in the if() block (this then allows the case of a list or tuple of vectors to passed to the else() block as desired). Related Issue sandialabs#313 .
…bership theorem Establish the proof of the linear_algebra/inner_products/inner_prod_field_membership theorem (along with the allowed/disallowed presumptions.txt files). See related original sandia proveit Issue: sandialabs#314.
…embership theorem Establish the proof of the linear_algebra/inner_products/inner_prod_complex_membership theorem (along with the allowed/disallowed presumptions.txt files). This proof depends on the more general theorem (proved and committed in an earlier commit) inner_prod_field_membership. See related original sandia proveit Issue: sandialabs#314.
…es.py
Incremental upgrades to linear_algebra/inner_products/inner_prod_spaces.py, mostly focused on the InnerProdSpaces.yield_readily_provable_inner_prod_spaces() method. This still raises errors when trying to deal with inner product spaces identified simply as C^{n} or R^{n}, which are not getting interpreted or transformed into actual inner product spaces but instead are being treated as sets or CartExp objects (neither of which have the desired 'field' attribute).
Incremental upgrades to linear_algebra/inner_products/inner_prod_spaces.py, mostly focused on the InnerProd.deduce_membership() and InnerProd.readily_provable_membership() methods in which blocks of code are being replaced with the InnerProdSpaces.yield_readily_provable_inner_prod_spaces() static method. This all still manifests errors when trying to deal with inner product spaces identified simply as C^{n} or R^{n}, which are not getting interpreted or transformed into actual inner product spaces but instead are being treated as sets or CartExp objects (neither of which have the desired 'field' attribute).
…entity.py Update descriptive/explanatory comments in linear_algebra/matrices/identity.py and provide some trivial reformatting for line length standards.
…/unitary_group.py
Update the `inner_prod_space_def` axiom in `linear_algebra/inner_products` to include an explicit domain specification for the vectors participating in the inner product. Also update the related `inner_prod_field_membership` and `inner_prod_complex_membership` theorems to also include vector domain specification. This update turns out not to require any user-designated changes in the proof notebooks for those two theorems (since we load in all the conditions using defaults.assuimptions).
Update InnerProdSpaces.yield_readily_provable_inner_prod_spaces() method, now allowing it to function properly for real and complex vectors and deal correctly with inner product spaces of the form R^{n} or C^{n}. This method is then called from within one or more methods in the InnerProd class (committed separately).
Update InnerProd.deduce_membership() and InnerProd.readily_provable_membership() methods, now both working properly for a variety of vector operands in the InnerProd class, including vectors in the cartesian product (CartExp) sets R^{n} and C^{n}. See some related testing and demonstrations in the linear_algebra/inner_products demonstrations notebook.
Update the demonstrations notebook for the linear_algebra/inner_products package, including tests and demonstrations of related recent work (committed separately) in the linear_algebra/inner_products/ InnerProd class and linear_algebra/inner_products/InnerProdSpaces class.
Provide proofs of three simple theorems in linear_algebra/inner_products package: hilbert_space_is_inner_prod_space hilbert_space_is_vec_space inner_prod_space_is_vec_space
Update the no_cloning theorem in the physics/quantum/algebra pkg to shift the target qubit 'b' to be paired with the unitary in the not-exists claim. Also provide an alternate version of the no_cloning theorem (perhaps to be considered a lemma). Update includes some trivial reformatting of some import statements.
313 quantum algebra development
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.
This is an experimental pull request (via Hoss) for merging Suhindu's forked Prove-It (master branch) into sandialabs/Prove-It master … We'll see what this looks like on @wwitzel 's side.