From 5e4bbdf929e0c0e64f25b8913475179c14ff7aa0 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 24 Feb 2024 07:23:54 +0530 Subject: [PATCH 01/29] Committing changes before merge:q --- .../proveit/physics/quantum/algebra/qmult.py | 134 ++++++++++++++---- 1 file changed, 103 insertions(+), 31 deletions(-) diff --git a/packages/proveit/physics/quantum/algebra/qmult.py b/packages/proveit/physics/quantum/algebra/qmult.py index 674f613db2d4..3fa336a17561 100644 --- a/packages/proveit/physics/quantum/algebra/qmult.py +++ b/packages/proveit/physics/quantum/algebra/qmult.py @@ -104,7 +104,8 @@ def shallow_simplification(self, *, must_evaluate=False, Ket(operand.operand)): return qmult_of_bra.instantiate( {Hspace:_Hspace, varphi:operand.operand}) - elif operand in MatrixSpace.known_memberships: + elif InClass.has_known_membership( + operand, domain_type=MatrixSpace._operator_): # Qmult of a matrix. It equates to a lambda # map, but this isn't considered a simplification. # Use linmap_reduction instead if this is desired. @@ -154,38 +155,94 @@ def shallow_simplification(self, *, must_evaluate=False, expr.operands.num_entries() > 1 and InSet(expr.operands[0], Complex).proven()): expr = eq.update(expr.scalar_mult_factorization()) - + if must_evaluate==True: + if isinstance(expr,ScalarMult): + try: + expr = eq.update(expr.inner_expr().scaled.projection()) + expr = eq.update(expr.evaluation()) + except ValueError: + pass + else: + try: + expr = eq.update(expr.projection()) + expr = eq.update(expr.evaluation()) + except ValueError: + pass + + #expr = eq.update(expr.evaluation()) return eq.relation + # + @equality_prover('adjoint_distributed', 'adjoint_distribute') + def adjoint_distribution(self,**defaults_config): + if self.operands.is_double(): + _A = self.operands[0] + _B = self.operands[1] + for linmap in containing_hilbert_space_linmap_sets(_B): + _Hspace, _X = linmap.from_vspace, linmap.to_vspace + for linmap in containing_hilbert_space_linmap_sets(_A): + _Y = linmap.to_vspace + return adjoint_binary_distribution.instantiate({Hspace:_Hspace,X:_X,Y:_Y,A:_A,B:_B}) + else: + raise NotImplementedError("We only treat adjoint distribution when there are two operands") + + @equality_prover('projected', 'project') + def projection(self,**defaults_config): + from . import qmult_op_ket, ket_self_projection + from proveit.physics.quantum import ( + Bra, Ket, HilbertSpaces, var_ket_psi,psi) + from proveit.logic import Equals + if not self.operands.is_double(): + raise ValueError("'projection' method only works when there are two operands") + M,ket = self.operands + #try: + linmap_eq = Qmult(M).linmap_reduction() + # except ValueError: + # pass + yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces + for _Hspace in yield_known_hilbert_spaces(ket): + if isinstance(M, Bra) and M.operand==ket.operand: + #if M.operand==ket.operand: + #print("same") + self_proj_eq=ket_self_projection.instantiate({Hspace: _Hspace, psi:ket.operand}) + #print(self_proj_eq) + #return linmap_eq.sub_right_side_into(self_proj_eq.inner_expr().rhs.operator) + return self_proj_eq + #bra_eq=bra_def.instantiate({varphi:bra.operand, Hspace: _Hspace}) + #return bra_eq.sub_right_side_into(qmult_eq.inner_expr().rhs.operator) + else: + #print("different") + qmult_eq=qmult_op_ket.instantiate({A:M, Hspace: _Hspace, X: Complex, var_ket_psi: ket}) + #print(qmult_eq) + return linmap_eq.sub_right_side_into(qmult_eq.inner_expr().rhs.operator) @equality_prover('linmap_reduced', 'linmap_reduce') def linmap_reduction(self, **defaults_config): ''' Equate the Qmult to a linear map, if possible. ''' + from proveit.physics.quantum import QmultCodomain + # In the process of proving that 'self' is in QmultCodomain, + # it will prove it is a linear map if it can. + QmultCodomain.membership_object(self).conclude() from proveit.physics.quantum import ( Bra, Ket, HilbertSpaces, varphi) - from proveit.physics.quantum.algebra import Hspace + #from proveit.physics.quantum.algebra import Hspace from . import qmult_of_matrix, qmult_of_bra_as_map yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces if self.operands.is_single(): # Unary Qmult operand = self.operand - if operand in MatrixSpace.known_memberships: - # Qmult of matrix equates to a linear map - mspace_memberships = MatrixSpace.known_memberships[operand] - matrix_dimensions = set() - for mspace_membership in mspace_memberships: - # Qmult of a matrix is the linear map - # represented by the matrix. - mspace = mspace_membership.domain - _m, _n = (mspace.operands['rows'], - mspace.operands['columns']) - matrix_dimensions.add((_m, _n)) - for _m, _n in matrix_dimensions: - return qmult_of_matrix.instantiate( - {m:_m, n:_n, M:operand}) - elif isinstance(operand, Bra): + for mspace_membership in InClass.yield_known_memberships( + operand, domain_type=MatrixSpace._operator_): + # Qmult of a matrix is the linear map + # represented by the matrix. + mspace = mspace_membership.domain + _m, _n = (mspace.operands['rows'], + mspace.operands['columns']) + return qmult_of_matrix.instantiate( + {m:_m, n:_n, M:operand}) + if isinstance(operand, Bra): for _Hspace in yield_known_hilbert_spaces( Ket(operand.operand)): return qmult_of_bra_as_map.instantiate( @@ -194,6 +251,7 @@ def linmap_reduction(self, **defaults_config): raise NotImplementedError( "'linmap_reduction' currently only impoemented " "for a unary Qmult") + raise ValueError("%s does not evaluate to a linear map"%self) @relation_prover def deduce_in_vec_space(self, vec_space=None, *, field, @@ -564,8 +622,10 @@ def conclude(self, **defaults_config): for _attempt in (0, 1): # Handle unary Qmult on a matrix. +<<<<<<< HEAD if op in MatrixSpace.known_memberships: mspace_memberships = MatrixSpace.known_memberships[op] + print(op) thm = None matrix_dimensions = set() for mspace_membership in mspace_memberships: @@ -576,6 +636,7 @@ def conclude(self, **defaults_config): for _m, _n in matrix_dimensions: # Prove linear map membership while we are # at it. + qmult_matrix_is_linmap.instantiate( {m:_m, n:_n, M:op}, preserve_all=True) used_mspace = mspace @@ -587,6 +648,22 @@ def conclude(self, **defaults_config): _m, _n = (used_mspace.operands['rows'], used_mspace.operands['columns']) return thm.instantiate({m:_m, n:_n, M:op}) +======= + for mspace_membership in InClass.yield_known_memberships( + op, domain_type=MatrixSpace._operator_): + mspace = mspace_membership.domain + _m, _n = (mspace.operands['rows'], + mspace.operands['columns']) + # Prove linear map membership while we are + # at it. + qmult_matrix_is_linmap.instantiate( + {m:_m, n:_n, M:op}, preserve_all=True) + # Choose any valid matrix space (the last + # used ones will do) for the QmultCodomain + # membership proof. + return qmult_matrix_in_QmultCodomain.instantiate( + {m:_m, n:_n, M:op}) +>>>>>>> d8d317cee73114b80c071759ecf5d4f707aee5f6 # Handle unary Qmult on a ket. for _Hspace in yield_known_hilbert_spaces(op): @@ -878,20 +955,15 @@ def containing_hilbert_space_linmap_sets(qobj): ''' from proveit.linear_algebra.inner_products.hilbert_spaces import ( deduce_as_hilbert_space) - known_linmap_memberships = LinMap.known_memberships # Prove the membership of qobj in Q* to prove # the side-effect linear map membership as well. #QmultCodomain.membership_object(qobj).conclude() for qobj in (qobj, Qmult(qobj)): - if qobj in known_linmap_memberships: - for linmap_membership in known_linmap_memberships[qobj]: - linmap = linmap_membership.domain - if not isinstance(linmap, LinMap): - raise TypeError("Expecting LinMap.known_memberships to " - "contain known memberships of LinMap " - "domains.") - for vec_space in linmap.operands: - deduce_as_hilbert_space(vec_space) - if all(InClass(V, HilbertSpaces).proven() for V - in linmap.operands): - yield linmap + for linmap_membership in InClass.yield_known_memberships( + qobj, domain_type=LinMap._operator_): + linmap = linmap_membership.domain + for vec_space in linmap.operands: + deduce_as_hilbert_space(vec_space) + if all(InClass(V, HilbertSpaces).proven() for V + in linmap.operands): + yield linmap From 299d70eefbebc10ab48a206abe6843d04b22ff94 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 24 Feb 2024 08:05:30 +0530 Subject: [PATCH 02/29] linear_algebra/matrices: added transposition subpackage 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. --- .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../matrices/_theory_nbs_/theorems.ipynb | 28 ++--- .../matrices/_theory_nbs_/theory.ipynb | 2 +- .../matrices/transposition/__init__.py | 8 ++ .../transposition/_brief_description_.txt | 1 + .../_sub_theories_.txt} | 0 .../_theory_nbs_/__init__.py} | 0 .../transposition/_theory_nbs_/axioms.ipynb | 59 ++++++++++ .../transposition/_theory_nbs_/common.ipynb | 59 ++++++++++ .../_theory_nbs_/demonstrations.ipynb | 80 +++++++++++++ .../presumptions.txt | 3 + .../thm_proof.ipynb | 2 +- .../unitaries_are_matrices/presumptions.txt | 3 + .../unitaries_are_matrices/thm_proof.ipynb | 2 +- .../unitary_dag_unitary/presumptions.txt | 3 + .../unitary_dag_unitary}/thm_proof.ipynb | 4 +- .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../unitary_unitary_dag/presumptions.txt | 3 + .../unitary_unitary_dag/thm_proof.ipynb | 47 ++++++++ .../transposition/_theory_nbs_/theorems.ipynb | 109 ++++++++++++++++++ .../transposition/_theory_nbs_/theory.ipynb | 33 ++++++ .../{ => transposition}/unitary_group.py | 0 24 files changed, 427 insertions(+), 19 deletions(-) delete mode 100644 packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/allowed_presumptions.txt delete mode 100644 packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/disallowed_presumptions.txt create mode 100644 packages/proveit/linear_algebra/matrices/transposition/__init__.py create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_brief_description_.txt rename packages/proveit/linear_algebra/matrices/{_theory_nbs_/proofs/eigen_pow/allowed_presumptions.txt => transposition/_sub_theories_.txt} (100%) rename packages/proveit/linear_algebra/matrices/{_theory_nbs_/proofs/eigen_pow/disallowed_presumptions.txt => transposition/_theory_nbs_/__init__.py} (100%) create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/axioms.ipynb create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/common.ipynb create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/presumptions.txt rename packages/proveit/linear_algebra/matrices/{ => transposition}/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb (60%) create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/presumptions.txt rename packages/proveit/linear_algebra/matrices/{ => transposition}/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb (60%) create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/presumptions.txt rename packages/proveit/linear_algebra/matrices/{_theory_nbs_/proofs/eigen_pow => transposition/_theory_nbs_/proofs/unitary_dag_unitary}/thm_proof.ipynb (58%) rename packages/proveit/linear_algebra/matrices/{_theory_nbs_/proofs/special_unitaries_are_matrices => transposition/_theory_nbs_/proofs/unitary_unitary_dag}/allowed_presumptions.txt (100%) rename packages/proveit/linear_algebra/matrices/{_theory_nbs_/proofs/special_unitaries_are_matrices => transposition/_theory_nbs_/proofs/unitary_unitary_dag}/disallowed_presumptions.txt (100%) create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/presumptions.txt create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/thm_proof.ipynb create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theorems.ipynb create mode 100644 packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theory.ipynb rename packages/proveit/linear_algebra/matrices/{ => transposition}/unitary_group.py (100%) diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/allowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/disallowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/matrices/_theory_nbs_/theorems.ipynb index 047af04370b1..a2958ad6f969 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/theorems.ipynb @@ -93,13 +93,13 @@ "metadata": {}, "outputs": [], "source": [ - "eigen_pow = (\n", - " Forall(k,\n", - " Forall(b,\n", - " Forall((A, x), \n", - " Implies(Equals(MatrixMult(A, x), ScalarMult(b, x)), \n", - " Equals(MatrixMult(Exp(A, k), x), ScalarMult(Exp(b, k), x)))),\n", - " domain=Complex), domain=NaturalPos))" + "#eigen_pow = (\n", + "# Forall(k,\n", + "# Forall(b,\n", + "# Forall((A, x), \n", + "# Implies(Equals(MatrixMult(A, x), ScalarMult(b, x)), \n", + "# Equals(MatrixMult(Exp(A, k), x), ScalarMult(Exp(b, k), x)))),\n", + "# domain=Complex), domain=NaturalPos))" ] }, { @@ -108,9 +108,9 @@ "metadata": {}, "outputs": [], "source": [ - "unitaries_are_matrices = Forall(\n", - " n, SubsetEq(Unitary(n), MatrixSpace(Complex, n, n)),\n", - " domain=NaturalPos)" + "#unitaries_are_matrices = Forall(\n", + "# n, SubsetEq(Unitary(n), MatrixSpace(Complex, n, n)),\n", + "# domain=NaturalPos)" ] }, { @@ -119,9 +119,9 @@ "metadata": {}, "outputs": [], "source": [ - "special_unitaries_are_matrices = Forall(\n", - " n, SubsetEq(SpecialUnitary(n), MatrixSpace(Complex, n, n)),\n", - " domain=NaturalPos)" + "#special_unitaries_are_matrices = Forall(\n", + "# n, SubsetEq(SpecialUnitary(n), MatrixSpace(Complex, n, n)),\n", + "# domain=NaturalPos)" ] }, { @@ -136,7 +136,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/theory.ipynb b/packages/proveit/linear_algebra/matrices/_theory_nbs_/theory.ipynb index a1031b92cfc9..34017edf4378 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/theory.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/theory.ipynb @@ -30,7 +30,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/matrices/transposition/__init__.py b/packages/proveit/linear_algebra/matrices/transposition/__init__.py new file mode 100644 index 000000000000..a3750a8281d6 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/__init__.py @@ -0,0 +1,8 @@ +# KEEP THE FOLLOWING IN __init__.py FOR THEORY PACKAGES. +# Make additions above, or add to sys.modules[__name__].__dict__ below. +# This allows us to import common expression, axioms, and theorems of +# the theory package directly from the package. +from .unitary_group import Unitary,SpecialUnitary +import sys +from proveit._core_.theory import TheoryPackage +sys.modules[__name__] = TheoryPackage(__name__, __file__, locals()) diff --git a/packages/proveit/linear_algebra/matrices/transposition/_brief_description_.txt b/packages/proveit/linear_algebra/matrices/transposition/_brief_description_.txt new file mode 100644 index 000000000000..718f4d2ff533 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_brief_description_.txt @@ -0,0 +1 @@ +t diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/allowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_sub_theories_.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/allowed_presumptions.txt rename to packages/proveit/linear_algebra/matrices/transposition/_sub_theories_.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/disallowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/__init__.py similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/disallowed_presumptions.txt rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/__init__.py diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/axioms.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/axioms.ipynb new file mode 100644 index 000000000000..42e1cf479838 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/axioms.ipynb @@ -0,0 +1,59 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Axioms for the theory of proveit.linear_algebra.matrices.transposition\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "# Prepare this notebook for defining the axioms of a theory:\n", + "%axioms_notebook # Keep this at the top following 'import proveit'.\n", + "\n", + "# from ... import ..." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%begin axioms" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%end axioms" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/common.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/common.ipynb new file mode 100644 index 000000000000..a15336cd5c07 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/common.ipynb @@ -0,0 +1,59 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Common expressions for the theory of proveit.linear_algebra.matrices.transposition\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "# Prepare this notebook for defining the common expressions of a theory:\n", + "%common_expressions_notebook # Keep this at the top following 'import proveit'.\n", + "\n", + "# from ... import ..." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%begin common" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%end common" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb new file mode 100644 index 000000000000..fb349d68e61c --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb @@ -0,0 +1,80 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Demonstrations for the theory of proveit.linear_algebra.matrices.transposition\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "from proveit import n,c, x, y, A, B, K, P, V, W, Px, Py,N,C,U\n", + "from proveit.numbers import one,two\n", + "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices,unitary_unitary_dag,unitary_dag_unitary\n", + "%begin demonstrations" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "x=unitaries_are_matrices.instantiate({n:two})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_unitary_dag.instantiate({n:two})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_dag_unitary.instantiate({n:two})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "for i in range(3,6):\n", + " print(i)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%end demonstrations" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/presumptions.txt new file mode 100644 index 000000000000..1cd064f0b8fb --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/presumptions.txt @@ -0,0 +1,3 @@ +# THEOREMS AND THEORIES THAT MAY BE PRESUMED: +proveit +# THEOREMS AND THEORIES TO EXCLUDE: diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb similarity index 60% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb index 6a5c49c3b218..3e1adaf3e46f 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/special_unitaries_are_matrices/thm_proof.ipynb @@ -4,7 +4,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Proof of proveit.linear_algebra.matrices.special_unitaries_are_matrices theorem\n", + "Proof of proveit.linear_algebra.matrices.transposition.special_unitaries_are_matrices theorem\n", "========" ] }, diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/presumptions.txt new file mode 100644 index 000000000000..1cd064f0b8fb --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/presumptions.txt @@ -0,0 +1,3 @@ +# THEOREMS AND THEORIES THAT MAY BE PRESUMED: +proveit +# THEOREMS AND THEORIES TO EXCLUDE: diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb similarity index 60% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb index 24fce315f71d..ab9b64b86e7e 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitaries_are_matrices/thm_proof.ipynb @@ -4,7 +4,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Proof of proveit.linear_algebra.matrices.unitaries_are_matrices theorem\n", + "Proof of proveit.linear_algebra.matrices.transposition.unitaries_are_matrices theorem\n", "========" ] }, diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/presumptions.txt new file mode 100644 index 000000000000..1cd064f0b8fb --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/presumptions.txt @@ -0,0 +1,3 @@ +# THEOREMS AND THEORIES THAT MAY BE PRESUMED: +proveit +# THEOREMS AND THEORIES TO EXCLUDE: diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/thm_proof.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb similarity index 58% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/thm_proof.ipynb rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb index 34baa25c4233..4a774ec7ee3e 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb @@ -4,7 +4,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Proof of proveit.linear_algebra.matrices.eigen_pow theorem\n", + "Proof of proveit.linear_algebra.matrices.transposition.unitary_dag_unitary theorem\n", "========" ] }, @@ -24,7 +24,7 @@ "metadata": {}, "outputs": [], "source": [ - "%proving eigen_pow" + "%proving unitary_dag_unitary" ] }, { diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/allowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/allowed_presumptions.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/allowed_presumptions.txt rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/allowed_presumptions.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/disallowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/disallowed_presumptions.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/disallowed_presumptions.txt rename to packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/disallowed_presumptions.txt diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/presumptions.txt new file mode 100644 index 000000000000..1cd064f0b8fb --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/presumptions.txt @@ -0,0 +1,3 @@ +# THEOREMS AND THEORIES THAT MAY BE PRESUMED: +proveit +# THEOREMS AND THEORIES TO EXCLUDE: diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/thm_proof.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/thm_proof.ipynb new file mode 100644 index 000000000000..53d80e0fe40f --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_unitary_dag/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.linear_algebra.matrices.transposition.unitary_unitary_dag theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving unitary_unitary_dag" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theorems.ipynb new file mode 100644 index 000000000000..fddd86921871 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theorems.ipynb @@ -0,0 +1,109 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Theorems (or conjectures) for the theory of proveit.linear_algebra.matrices.transposition\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "# Prepare this notebook for defining the theorems of a theory:\n", + "%theorems_notebook # Keep this at the top following 'import proveit'.\n", + "from proveit import (a, b, b_of_j, b_of_k, c, d, f, g, i, j, k, m, n, t,\n", + " x, y, z, fj, gj, fy, A, P, U, V, W, S, alpha, beta)\n", + "from proveit import Function, ExprRange, IndexedVar\n", + "from proveit.core_expr_types import (bj, a_1_to_m, x_1_to_i, x_1_to_m,\n", + " y_1_to_j, z_1_to_k, z_1_to_n)\n", + "from proveit.core_expr_types import (\n", + " a_1_to_i, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k)\n", + "from proveit.logic import Equals, Forall, Implies, Iff, InSet, InClass, SubsetEq\n", + "from proveit.numbers import Add, Mult, Exp, Sum\n", + "from proveit.numbers import one\n", + "from proveit.numbers import (Integer, Interval, Natural, NaturalPos,\n", + " Rational, Real, Complex)\n", + "from proveit.linear_algebra import (\n", + " VecSpaces, LinMap, ScalarMult, MatrixSpace,\n", + " TensorProd, MatrixMult, Unitary, SpecialUnitary)\n", + "from proveit.linear_algebra.matrices import Identity\n", + "from proveit import Variable,Literal\n", + "from proveit.linear_algebra import Adj\n", + "# from ... import ..." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%begin theorems" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitaries_are_matrices = Forall(\n", + " n, SubsetEq(Unitary(n), MatrixSpace(Complex, n, n)),\n", + " domain=NaturalPos)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "special_unitaries_are_matrices = Forall(\n", + " n, SubsetEq(SpecialUnitary(n), MatrixSpace(Complex, n, n)),\n", + " domain=NaturalPos)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_unitary_dag=Forall(n,Forall(U,Equals(MatrixMult(U,Adj(U)),Identity(n)),domain=Unitary(n)),domain=NaturalPos)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_dag_unitary=Forall(n,Forall(U,Equals(MatrixMult(Adj(U),U),Identity(n)),domain=Unitary(n)),domain=NaturalPos)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%end theorems" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theory.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theory.ipynb new file mode 100644 index 000000000000..0b6e3934622b --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/theory.ipynb @@ -0,0 +1,33 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Theory of proveit.linear_algebra.matrices.transposition\n", + "========\n", + "\n", + "Provide description here." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "%theory # toggles between interactive and static modes" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/matrices/unitary_group.py b/packages/proveit/linear_algebra/matrices/transposition/unitary_group.py similarity index 100% rename from packages/proveit/linear_algebra/matrices/unitary_group.py rename to packages/proveit/linear_algebra/matrices/transposition/unitary_group.py From 1acd7335f43be60a2fc27a74c6cc4435dfe53f1e Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 24 Feb 2024 08:21:05 +0530 Subject: [PATCH 03/29] linear_algebra.matrices: added identity.py Established Identity class and added . identity_def added in axioms also added to demonstration note book --- .../matrices/_theory_nbs_/axioms.ipynb | 24 +++++++++++++-- .../_theory_nbs_/demonstrations.ipynb | 9 ++++-- .../linear_algebra/matrices/identity.py | 29 +++++++++++++++++++ 3 files changed, 57 insertions(+), 5 deletions(-) create mode 100644 packages/proveit/linear_algebra/matrices/identity.py diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/axioms.ipynb b/packages/proveit/linear_algebra/matrices/_theory_nbs_/axioms.ipynb index 8c27f15d0558..321ba5117ddd 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/axioms.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/axioms.ipynb @@ -18,7 +18,16 @@ "# Prepare this notebook for defining the axioms of a theory:\n", "%axioms_notebook # Keep this at the top following 'import proveit'.\n", "\n", - "# from ... import ..." + "# from ... import ...\n", + "from proveit import Function, Lambda, Conditional, Composition\n", + "from proveit.logic import And, Iff, Forall, Equals, InSet\n", + "from proveit import n,c, x, y, A, B, K, P, V, W, Px, Py,N,C\n", + "from proveit.linear_algebra import (\n", + " VecSpaces, LinMap, VecAdd, vec_subtract, ScalarMult,Identity,VecZero, Commutator, AntiCommutator,MatrixSpace)\n", + "from proveit.numbers import zero, one, Add, Natural, NaturalPos, greater\n", + "from proveit.linear_algebra.matrices import Identity\n", + "from proveit.linear_algebra.inner_products import HilbertSpaces\n", + "from proveit.numbers import one, i, Real, Complex, Add, subtract, Neg, Mult, Conjugate \n" ] }, { @@ -35,7 +44,9 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "identity_def = Forall(n, Equals(Identity(n),proveit.linear_algebra.Identity(MatrixSpace(Complex,n,n))),domain=NaturalPos)" + ] }, { "cell_type": "code", @@ -45,11 +56,18 @@ "source": [ "%end axioms" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb index 125a9574361b..79f4aee8c7d0 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb @@ -15,6 +15,9 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import n,c, x, y, A, B, K, P, V, W, Px, Py,N,C\n", + "from proveit.numbers import one,two\n", + "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices,Unitary_Unitary_dag\n", "%begin demonstrations" ] }, @@ -23,7 +26,9 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "unitaries_are_matrices.instantiate({n:two})" + ] }, { "cell_type": "code", @@ -37,7 +42,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/matrices/identity.py b/packages/proveit/linear_algebra/matrices/identity.py new file mode 100644 index 000000000000..d9a43537c6ce --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/identity.py @@ -0,0 +1,29 @@ +from proveit import Function, Literal + +class Identity(Function): + ''' + The identity map of a vector space is a linear map that maps + any element to itself. + ''' + + _operator_ = Literal(string_format='1',latex_format=r'\mathbbm{1}', theory=__file__) + + def _config_latex_tool(self, lt): + if 'bbm' not in lt.packages: + lt.packages.append('bbm') + + def __init__(self,size, *, styles=None): + ''' + Denote the set of linear maps that map from and to the given + vectors spaces. + ''' + Function.__init__(self, Identity._operator_, size, + styles=styles) + + def string(self, **kwargs): + return self.operator.string() + '_' + ( + self.operand.string(fence=True)) + + def latex(self, **kwargs): + return self.operator.latex() + '_{' + ( + self.operand.latex(fence=True) + '}') From d245d4ed4da6dec24bb8fda13a9358455bd16a95 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 24 Feb 2024 09:21:04 +0530 Subject: [PATCH 04/29] quantum.algebra: no_cloning and adjoint_binary_distribution theorem added We updated in Qmult.py : added methods are adjoint_distribution and projection --- .../quantum/algebra/_theory_nbs_/axioms.ipynb | 44 ++- .../algebra/_theory_nbs_/demonstrations.ipynb | 264 +++++++++++++++++- .../thm_proof.ipynb | 47 ++++ .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../bra_is_linmap/allowed_presumptions.txt | 0 .../bra_is_linmap/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../ket_one_norm/allowed_presumptions.txt | 0 .../ket_one_norm/disallowed_presumptions.txt | 0 .../ket_self_projection/thm_proof.ipynb | 47 ++++ .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../ket_zero_norm/allowed_presumptions.txt | 0 .../ket_zero_norm/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../proofs/num_ket0/allowed_presumptions.txt | 0 .../num_ket0/disallowed_presumptions.txt | 0 .../proofs/num_ket1/allowed_presumptions.txt | 0 .../num_ket1/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../num_ket_neq/allowed_presumptions.txt | 0 .../num_ket_neq/disallowed_presumptions.txt | 0 .../num_ket_norm/allowed_presumptions.txt | 0 .../num_ket_norm/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../qmult_ket_is_ket/allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../qmult_of_bra/allowed_presumptions.txt | 0 .../qmult_of_bra/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../qmult_of_complex/allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../algebra/_theory_nbs_/theorems.ipynb | 81 +++++- 149 files changed, 456 insertions(+), 27 deletions(-) create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/adjoint_binary_distribution/thm_proof.ipynb delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/disallowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/disallowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/allowed_presumptions.txt delete mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/disallowed_presumptions.txt diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/axioms.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/axioms.ipynb index d16bc03e11eb..e42429689e99 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/axioms.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/axioms.ipynb @@ -121,15 +121,39 @@ "metadata": {}, "outputs": [], "source": [ - "bra_def = Forall( \n", - " Hspace, \n", - " Forall(\n", - " varphi, Equals(\n", - " bra_varphi, \n", - " Lambda(var_ket_psi,\n", - " Conditional(InnerProd(ket_varphi, var_ket_psi),\n", - " InSet(var_ket_psi, Hspace)))),\n", - " condition=InSet(ket_varphi, Hspace)),\n", + "#bra_def = Forall( \n", + "# Hspace, \n", + "# Forall(\n", + "# varphi, Equals(\n", + "# bra_varphi, \n", + "# Lambda(var_ket_psi,\n", + "# Conditional(InnerProd(ket_varphi, var_ket_psi),\n", + "# InSet(var_ket_psi, Hspace)))),\n", + "# condition=InSet(ket_varphi, Hspace)),\n", + "# domain=HilbertSpaces)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "A 'bra' acts as an operator defined by the inner product. The order in the inner product is reversed to compensate for the different conventions between Physicists and Mathematicians (whether the inner product is linear versus conjugate-linear on the left or right)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def = Forall(\n", + " Hspace, Forall(\n", + " varphi, Equals(\n", + " Bra(varphi), \n", + " Lambda(var_ket_psi,\n", + " Conditional(InnerProd(var_ket_psi, ket_varphi),\n", + " InSet(var_ket_psi, Hspace)))),\n", + " condition=InSet(Ket(varphi), Hspace)),\n", " domain=HilbertSpaces)" ] }, @@ -443,7 +467,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb index 63b39a946c96..0d9b353febe1 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb @@ -16,16 +16,22 @@ "source": [ "import proveit\n", "from proveit import defaults\n", - "from proveit import alpha, beta, gamma, delta, j, m, n, b, c, A, B, C, D\n", + "from proveit import alpha, beta, gamma, delta, j, m, n, b, c, A, B, C, D,H,a,X,Y\n", "from proveit.core_expr_types import b_1_to_j, f__b_1_to_j, Q__b_1_to_j\n", - "from proveit.logic import Forall, InSet, CartExp, InClass\n", - "from proveit.numbers import Complex, NaturalPos\n", - "from proveit.linear_algebra import VecAdd, MatrixSpace\n", + "from proveit.logic import Forall, InSet, CartExp, InClass,Equals\n", + "from proveit.numbers import Complex, NaturalPos,one\n", + "from proveit.linear_algebra import VecAdd, MatrixSpace, Hspace\n", "from proveit.linear_algebra.addition import vec_summation_b1toj_fQ\n", "from proveit.physics.quantum import Qmult, Bra, Ket\n", "from proveit.physics.quantum import (\n", - " psi, bra_psi, ket_psi, varphi, bra_varphi, ket_varphi)\n", + " psi, bra_psi, ket_psi, varphi, bra_varphi, ket_varphi,var_ket_psi)\n", "from proveit.physics.quantum.algebra import QmultCodomain\n", + "from proveit.physics.quantum.algebra import qmult_of_bra_as_map\n", + "from proveit.linear_algebra import (\n", + " VecSpaces, HilbertSpaces, Hspace, VecZero, LinMap, Commutator,\n", + " MatrixSpace, MatrixMult, Unitary, Diagonal, ScalarMult, TensorProd, Identity,\n", + " VecAdd, VecSum, InnerProd, InnerProdSpaces, Norm, OrthoProj, Adj, OrthoNormBases, Dim)\n", + "from proveit.physics.quantum.algebra import adjoint_binary_distribution\n", "%begin demonstrations" ] }, @@ -47,6 +53,51 @@ " condition=Q__b_1_to_j)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "LinMap(Hspace,X)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Hspace" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "LinMap(X,Y)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(X,HilbertSpaces)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(Y,HilbertSpaces)" + ] + }, { "cell_type": "code", "execution_count": null, @@ -58,17 +109,156 @@ " InSet(gamma, Complex), InSet(delta, Complex),\n", " InSet(j, NaturalPos),\n", " InSet(m, NaturalPos), InSet(n, NaturalPos),\n", - " InSet(ket_psi, CartExp(Complex, m)),\n", + " InSet(ket_psi, CartExp(Complex, n)),\n", " InSet(A, MatrixSpace(Complex, n, m)),\n", " InSet(B, MatrixSpace(Complex, n, m)),\n", " InSet(C, MatrixSpace(Complex, n, m)),\n", " InSet(D, MatrixSpace(Complex, m, n)),\n", " InSet(ket_varphi, CartExp(Complex, n)),\n", " all_instances_in_C_nxm,\n", - " Q__b_1_to_j.basic_replaced({b:c})\n", + " Q__b_1_to_j.basic_replaced({b:c}),\n", + " InSet(Ket(a), CartExp(Complex, n)),\n", + " InSet(Ket(b), CartExp(Complex, n)),\n", + " Equals(Norm(ket_psi),one),\n", + " InClass(X,HilbertSpaces),\n", + " InClass(Y,HilbertSpaces),\n", + " InClass(H,HilbertSpaces)\n", " ]" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "adjoint_binary_distribution.instantiate({Hspace:H,X:X,Y:Y})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(A,B)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "var_ket_psi" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Ket(psi)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(ket_varphi.operand), ket_psi).projection()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(a), Ket(a)).projection()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(ket_varphi.operand), ket_varphi).projection()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(ket_psi.operand), ket_psi).evaluation()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(varphi),Ket(a)).projection()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(ket_psi.operand)).linmap_reduction()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(varphi)).linmap_reduction()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Qmult(Bra(psi),Ket(psi))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Bra(psi)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_as_map.instantiate({Hspace:CartExp(Complex, n),varphi:varphi})" + ] + }, { "cell_type": "code", "execution_count": null, @@ -269,7 +459,25 @@ "metadata": {}, "outputs": [], "source": [ - "InClass(Qmult(ket_varphi, bra_psi), QmultCodomain).prove()" + "InClass(Qmult(ket_varphi, bra_psi), QmultCodomain).conclude()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "QmultCodomain.membership_object(Qmult(ket_varphi, bra_psi)).conclude()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InClass(Qmult(ket_varphi, bra_psi), QmultCodomain).membership_object._readily_provable()" ] }, { @@ -308,6 +516,28 @@ "InClass(Qmult(bra_varphi, ket_varphi, gamma), QmultCodomain).prove()" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = [\n", + " InSet(alpha, Complex), InSet(beta, Complex),\n", + " InSet(gamma, Complex), InSet(delta, Complex),\n", + " InSet(j, NaturalPos),\n", + " InSet(m, NaturalPos), InSet(n, NaturalPos),\n", + " InSet(ket_psi, CartExp(Complex, m)),\n", + " InSet(A, MatrixSpace(Complex, n, m)),\n", + " InSet(B, MatrixSpace(Complex, n, m)),\n", + " InSet(C, MatrixSpace(Complex, n, m)),\n", + " InSet(D, MatrixSpace(Complex, m, n)),\n", + " InSet(ket_varphi, CartExp(Complex, n)),\n", + " all_instances_in_C_nxm,\n", + " Q__b_1_to_j.basic_replaced({b:c})\n", + " ]" + ] + }, { "cell_type": "code", "execution_count": null, @@ -317,6 +547,15 @@ "qmult1" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions" + ] + }, { "cell_type": "code", "execution_count": null, @@ -683,6 +922,13 @@ "qmult4.simplification()" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -695,7 +941,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/adjoint_binary_distribution/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/adjoint_binary_distribution/thm_proof.ipynb new file mode 100644 index 000000000000..11622c7c52e1 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/adjoint_binary_distribution/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.physics.quantum.algebra.adjoint_binary_distribution theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving adjoint_binary_distribution" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_in_qubit_space/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_one_norm/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb new file mode 100644 index 000000000000..a45c58402bf9 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.physics.quantum.algebra.ket_self_projection theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving ket_self_projection" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_are_orthogonal/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_and_one_have_zero_inner_prod/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_in_qubit_space/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_zero_norm/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_left_polar_decomposition/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_right_polar_decomposition/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_singular_value_decomposition/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/matrix_spectral_decomposition_as_outer_prods/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/normalization_preservation/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_bra_is_lin_map/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket0/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket1/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_in_register_space/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_neq/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/num_ket_norm/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/op_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/operator_function/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_norm_bases_form_unitary_matrix/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ortho_projector_from_completion/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/output_prod_operator_repr/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_one_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/prepend_num_ket_with_zero_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_association/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_complex_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_ket_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_left_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_op_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_complex_right_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_disassociation/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_add/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_distribution_over_summation/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_bra_is_op/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_complex_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_is_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_ket_ket_is_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_matrix_is_linmap/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_nested_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_complex/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_complex_closure/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_is_linmap/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_ket_is_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_in_QmultCodomain/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_op_op_is_op/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalar_out_front/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_pulling_scalars_out_front/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_scalar_association/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_absorption/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/scalar_mult_factorization/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/schmidt_decomposition/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/simultaneous_diagonalization_as_outer_prods/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/single_qubit_num_ket/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/spectral_decomposition_as_outer_prods/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/state_space_preservation/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitarity_by_ortho_norm_bases_elements/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/allowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/unitary_matrices_transform_ortho_norm_bases/disallowed_presumptions.txt deleted file mode 100644 index e69de29bb2d1..000000000000 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb index 198bbc1e4e6f..f797f4a41ddb 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb @@ -20,15 +20,15 @@ "\n", "from proveit import (Function, Lambda, Conditional, Composition,\n", " ExprTuple, ExprRange, IndexedVar)\n", - "from proveit import (a, b, c, f, i, j, k, l, m, n, x, A, B, D, M, P, Q, U, V, W, X, Y,\n", + "from proveit import (a, b, c, f, i, j, k, l, m, n, x, A, B, D,K,M, P, Q, U, V, W, X, Y,\n", " alpha)\n", - "from proveit.core_expr_types import (\n", - " a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, b_1_to_j, \n", + "from proveit.core_expr_types import (A_i,V_i,W_i,\n", + " a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, b_1_to_j,v_1_to_n, \n", " x_i, x_1_to_n, v_i, v_j, w_i, w_j, v_1_to_n, v_1_to_m, w_1_to_n, \n", - " A_1_to_l, A_1_to_m, B_1_to_i, B_1_to_j, B_1_to_m, C_1_to_n, lambda_i)\n", + " A_1_to_l,A_1_to_n, A_1_to_m, B_1_to_i, B_1_to_j, B_1_to_m, C_1_to_n,V_1_to_n, W_1_to_n, lambda_i)\n", "from proveit.logic import (And, Implies, Iff, Or, Forall, Exists, Equals, NotEquals,\n", - " Set, InSet, SubsetEq, InClass, CartExp, Functions)\n", - "from proveit.numbers import (zero, one, two, Natural, NaturalPos, \n", + " Set, InSet, SubsetEq, InClass, CartExp, Functions,NotInSet,NotExists)\n", + "from proveit.numbers import (zero, one, two,four, Natural, NaturalPos, \n", " RealNonNeg, Complex, Interval, Min, KroneckerDelta)\n", "from proveit.numbers import Add, subtract, Mult, Exp, sqrd, sqrt\n", "from proveit.linear_algebra import (\n", @@ -42,7 +42,8 @@ " var_ket_psi, var_ket_varphi, var_ket_v, QubitSpace, QubitRegisterSpace)\n", "from proveit.physics.quantum.algebra import (\n", " QmultCodomain, n_bit_interval, a_1_to_m_kets, b_1_to_n_kets,\n", - " v_1_to_m_kets, v_1_to_n_kets, w_1_to_n_kets, x_1_to_n_kets)" + " v_1_to_m_kets, v_1_to_n_kets, w_1_to_n_kets, x_1_to_n_kets)\n", + "from proveit.numbers import Mult, Exp" ] }, { @@ -61,6 +62,17 @@ "### Completeness relation and properties of orthogonal projectors" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "no_cloning=NotExists(U,Forall((a,b),Equals(Qmult(U,TensorProd(a,b)),TensorProd(a,a)),\n", + " domain=QubitSpace,conditions=(Equals(Norm(a),one),Equals(Norm(b),one))),\n", + " domain=Unitary(four))" + ] + }, { "cell_type": "code", "execution_count": null, @@ -893,6 +905,17 @@ " domain=HilbertSpaces)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "ket_self_projection=Forall(\n", + " Hspace,Forall(\n", + " psi,Equals(Qmult(Bra(psi),Ket(psi)),Exp(Norm(Ket(psi)),two)),condition=InSet(Ket(psi), Hspace)),domain=HilbertSpaces)" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -1154,6 +1177,41 @@ " domain=HilbertSpaces)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "adjoint_binary_distribution=Forall(\n", + " (Hspace, X, Y), Forall(\n", + " (A, B),Equals(Adj(Qmult(A,B)),Qmult(Adj(B),Adj(A))),\n", + " conditions=[InSet(Qmult(A), LinMap(X, Y)),\n", + " InSet(Qmult(B), LinMap(Hspace, X))]),\n", + " domain=HilbertSpaces)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_linear_maps = Forall(\n", + " K, Forall(\n", + " n, Forall(\n", + " (V_1_to_n, W_1_to_n), Forall(\n", + " A_1_to_n, Forall(\n", + " v_1_to_n,\n", + " Equals(Qmult(TensorProd(A_1_to_n),\n", + " TensorProd(v_1_to_n)),\n", + " TensorProd(ExprRange(i, Qmult(A_i, v_i), one, n))),\n", + " domains=[V_1_to_n]).with_wrapping(),\n", + " domains=[ExprRange(i, LinMap(V_i, W_i), one, n)]).with_wrapping(),\n", + " domain=VecSpaces(K)).with_wrapping(),\n", + " domain=NaturalPos))" + ] + }, { "cell_type": "code", "execution_count": null, @@ -1315,6 +1373,13 @@ " domain=NaturalPos)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -1334,7 +1399,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } From 11d34e765a6400289a607ebf81602672b3020200 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 24 Feb 2024 09:40:24 +0530 Subject: [PATCH 05/29] linear_algebra.matrices: update imports Unitary and SpecialUnitary class move to new sub theory transposition from unitary_group package --- packages/proveit/linear_algebra/matrices/__init__.py | 5 ++++- packages/proveit/linear_algebra/matrices/_sub_theories_.txt | 1 + 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/packages/proveit/linear_algebra/matrices/__init__.py b/packages/proveit/linear_algebra/matrices/__init__.py index d668fcb79118..c09e6e276119 100644 --- a/packages/proveit/linear_algebra/matrices/__init__.py +++ b/packages/proveit/linear_algebra/matrices/__init__.py @@ -1,8 +1,11 @@ from .matrix_space import MatrixSpace from .multiplication import MatrixMult from .exponentiation import MatrixExp -from .unitary_group import Unitary, SpecialUnitary +#from .unitary_group import Unitary, SpecialUnitary +from .transposition import Unitary, SpecialUnitary from .diagonal_group import Diagonal +from .identity import Identity +#from .identity import Identity # KEEP THE FOLLOWING IN __init__.py FOR THEORY PACKAGES. # Make additions above, or add to sys.modules[__name__].__dict__ below. diff --git a/packages/proveit/linear_algebra/matrices/_sub_theories_.txt b/packages/proveit/linear_algebra/matrices/_sub_theories_.txt index df6f18032e98..de9b6baec519 100644 --- a/packages/proveit/linear_algebra/matrices/_sub_theories_.txt +++ b/packages/proveit/linear_algebra/matrices/_sub_theories_.txt @@ -1,3 +1,4 @@ addition multiplication exponentiation +transposition From 0cda770d18c79913a6ac0b9d1783087cac526dca Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Sat, 16 Mar 2024 08:17:04 +0530 Subject: [PATCH 06/29] linear_algebra : added Adj.distribution method --- packages/proveit/linear_algebra/inner_products/adjoint.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/packages/proveit/linear_algebra/inner_products/adjoint.py b/packages/proveit/linear_algebra/inner_products/adjoint.py index 6183c338c773..bfd7ea195272 100644 --- a/packages/proveit/linear_algebra/inner_products/adjoint.py +++ b/packages/proveit/linear_algebra/inner_products/adjoint.py @@ -1,4 +1,4 @@ -from proveit import Function, Literal +from proveit import Function, Literal,equality_prover class Adj(Function): @@ -18,3 +18,8 @@ def string(self, **kwargs): def latex(self, **kwargs): return self.operand.string(fence=True) + r'^{\dagger}' + ##### newly added + @equality_prover('distributed', 'distribute') + def distribution(self,**defaults_config): + if hasattr(self.operand, 'adjoint_distribution'): + return self.operand.adjoint_distribution() From 3bf6e9a09b14eea05b3b12ae3fe12364e157ba44 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Wed, 1 May 2024 15:28:13 +0530 Subject: [PATCH 07/29] changes according to issue 313 --- build.py | 8 +- build_alt.py | 6 +- .../expression/composite/_sub_theories_.txt | 0 .../expression/conditional/_sub_theories_.txt | 0 .../expression/label/_sub_theories_.txt | 0 .../expression/lambda_expr/_sub_theories_.txt | 0 .../expression/operation/_sub_theories_.txt | 0 .../_theory_nbs_/theorems.ipynb | 13 ++- .../inner_products/_theory_nbs_/axioms.ipynb | 2 +- .../thm_proof.ipynb | 47 ++++++++ .../thm_proof.ipynb | 47 ++++++++ .../_theory_nbs_/theorems.ipynb | 26 ++++- .../inner_products/inner_prod.py | 3 + .../inner_products/inner_prod_spaces.py | 22 ++-- .../physics/quantum/_theory_nbs_/common.ipynb | 2 +- .../allowed_presumptions.txt | 6 + .../disallowed_presumptions.txt | 0 .../ket_self_projection/thm_proof.ipynb | 106 +++++++++++++++++- .../proofs/no_cloning/thm_proof.ipynb | 47 ++++++++ .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../qmult_of_linear_maps/thm_proof.ipynb | 47 ++++++++ .../proveit/physics/quantum/algebra/qmult.py | 2 +- 25 files changed, 355 insertions(+), 29 deletions(-) create mode 100644 packages/proveit/_core_/expression/composite/_sub_theories_.txt create mode 100644 packages/proveit/_core_/expression/conditional/_sub_theories_.txt create mode 100644 packages/proveit/_core_/expression/label/_sub_theories_.txt create mode 100644 packages/proveit/_core_/expression/lambda_expr/_sub_theories_.txt create mode 100644 packages/proveit/_core_/expression/operation/_sub_theories_.txt create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/allowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/disallowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/thm_proof.ipynb diff --git a/build.py b/build.py index 5b680fc2f0ea..9b9b41b0e17e 100644 --- a/build.py +++ b/build.py @@ -10,8 +10,8 @@ import itertools import re import time -import lxml # Comment in for Python 3 -from lxml import etree # Comment in for Python 3 +#import lxml # Comment in for Python 3 +#from lxml import etree # Comment in for Python 3 import shutil import argparse import nbformat @@ -23,8 +23,8 @@ import base64 import datetime import tarfile -# import urllib#Comment out for Python 3 -import urllib.request # Comment in for Python 3 +import urllib#Comment out for Python 3 +#import urllib.request # Comment in for Python 3 import zmq # to catch ZMQError which randomly occurs when starting a Jupyter kernel import proveit from proveit import Theory diff --git a/build_alt.py b/build_alt.py index cfbc73ec5aca..c78b19987a8d 100644 --- a/build_alt.py +++ b/build_alt.py @@ -16,15 +16,15 @@ import argparse import nbformat from nbconvert.preprocessors import Preprocessor, ExecutePreprocessor -#from nbconvert.preprocessors.execute import executenb +from nbconvert.preprocessors.execute import executenb from nbconvert import HTMLExporter import IPython from IPython.lib.latextools import LaTeXTool import base64 import datetime import tarfile -# import urllib#Comment out for Python 3 -import urllib.request # Comment in for Python 3 +import urllib#Comment out for Python 3 +#import urllib.request # Comment in for Python 3 import zmq # to catch ZMQError which randomly occurs when starting a Jupyter kernel import proveit from proveit import Theory diff --git a/packages/proveit/_core_/expression/composite/_sub_theories_.txt b/packages/proveit/_core_/expression/composite/_sub_theories_.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/_core_/expression/conditional/_sub_theories_.txt b/packages/proveit/_core_/expression/conditional/_sub_theories_.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/_core_/expression/label/_sub_theories_.txt b/packages/proveit/_core_/expression/label/_sub_theories_.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/_core_/expression/lambda_expr/_sub_theories_.txt b/packages/proveit/_core_/expression/lambda_expr/_sub_theories_.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/_core_/expression/operation/_sub_theories_.txt b/packages/proveit/_core_/expression/operation/_sub_theories_.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/linear_algebra/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/_theory_nbs_/theorems.ipynb index 6fea4d707b84..207123013111 100644 --- a/packages/proveit/linear_algebra/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/linear_algebra/_theory_nbs_/theorems.ipynb @@ -18,10 +18,10 @@ "# Prepare this notebook for defining the theorems of a theory:\n", "%theorems_notebook # Keep this at the top following 'import proveit'.\n", "\n", - "from proveit import n\n", + "from proveit import n, K,H\n", "from proveit.logic import Forall, InSet, CartExp, InClass\n", "from proveit.numbers import NaturalPos, Rational, Real, Complex\n", - "from proveit.linear_algebra import VecSpaces" + "from proveit.linear_algebra import VecSpaces,InnerProdSpaces" ] }, { @@ -51,6 +51,13 @@ " domain = NaturalPos)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -119,7 +126,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb index 143bdb550e32..38537fe0c781 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb @@ -157,7 +157,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb new file mode 100644 index 000000000000..a3dd2a19b29e --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.linear_algebra.inner_products.inner_prod_complex_membership theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving inner_prod_complex_membership" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb new file mode 100644 index 000000000000..13cb778db433 --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.linear_algebra.inner_products.inner_prod_field_membership theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving inner_prod_field_membership" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb index 27947a3f4f19..0e1dce04572c 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb @@ -23,7 +23,7 @@ "from proveit.core_expr_types import (a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, x_i, x_1_to_n,\n", " lambda_i)\n", "from proveit.logic import (\n", - " And, Forall, Exists, Iff, InSet, Set, SubsetEq, CartExp, InClass, Equals, NotEquals)\n", + " And, Forall, Exists, Iff, InSet, Set, SubsetEq, CartExp, InClass, Equals, NotEquals,Implies)\n", "from proveit.numbers import zero, one, NaturalPos, Rational, Real, RealNonNeg, Complex, Conjugate\n", "from proveit.numbers import Interval, Add, Mult, Abs, LessEq, greater, Min, sqrd, sqrt\n", "from proveit.linear_algebra import (\n", @@ -51,6 +51,28 @@ " domain=InnerProdSpaces(K)))" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_field_membership=Forall(\n", + " (K,H),\n", + " Forall((x,y),InSet(InnerProd(x,y),K)),condition=InClass(H,InnerProdSpaces(K)))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_complex_membership=Forall(\n", + " H,\n", + " Forall((x,y),InSet(InnerProd(x,y),Complex)),condition=InClass(H,HilbertSpaces))" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -628,7 +650,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod.py b/packages/proveit/linear_algebra/inner_products/inner_prod.py index 20861e5bfe14..2a20e09286b4 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod.py @@ -63,4 +63,7 @@ def shallow_simplification(self, *, must_evaluate=False, if must_evaluate and not is_irreducible_value(simp.rhs): return simp.inner_expr().rhs.evaluate() return simp + + + diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index 1fd23a21c65f..d0fcc2db124f 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -35,7 +35,7 @@ def __init__(self, field, *, styles=None, _operator=None): if _operator is None: _operator = InnerProdSpaces._operator_ VecSpaces.__init__(self, field, styles=styles, _operator=_operator) - + def membership_object(self, element): return InnerProdSpacesMembership(element, self) @@ -179,16 +179,16 @@ def deduce_as_inner_prod_space(expr, *, field=None, # If there is a 'deduce_as_inner_prod_space' class method for # the expression, try that. membership = expr.deduce_as_inner_prod_space() - if membership is not None: - InClass.check_proven_class_membership( - membership, expr, InnerProdSpaces) - if field is not None and membership.domain.field != field: - raise ValueError("'deduce_as_inner_prod_space' proved membership " - "in inner product spaces over %s, not over " - "the requested %s field" - %(membership.domain.field, field)) - - return membership + if membership is not None: + InClass.check_proven_class_membership( + membership, expr, InnerProdSpaces) + if field is not None and membership.domain.field != field: + raise ValueError("'deduce_as_inner_prod_space' proved membership " + "in inner product spaces over %s, not over " + "the requested %s field" + %(membership.domain.field, field)) + + return membership raise NotImplementedError( "'deduce_as_inner_prod_space' is only implemented when " "the element is a CartExp expression or has a " diff --git a/packages/proveit/physics/quantum/_theory_nbs_/common.ipynb b/packages/proveit/physics/quantum/_theory_nbs_/common.ipynb index 7805600da9ea..b91c0164e49b 100644 --- a/packages/proveit/physics/quantum/_theory_nbs_/common.ipynb +++ b/packages/proveit/physics/quantum/_theory_nbs_/common.ipynb @@ -459,7 +459,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/allowed_presumptions.txt new file mode 100644 index 000000000000..551d72b19a25 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/allowed_presumptions.txt @@ -0,0 +1,6 @@ +proveit.linear_algebra.inner_products.hilbert_space_is_inner_prod_space +proveit.core_expr_types.conditionals.satisfied_condition_reduction +proveit.linear_algebra.inner_products.complex_set_is_hilbert_space +proveit.logic.equality.sub_right_side_into +proveit.physics.quantum.algebra.qmult_bra_is_linmap +proveit.physics.quantum.algebra.qmult_of_bra_as_map diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb index a45c58402bf9..9cec79bdcf6c 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb @@ -15,7 +15,15 @@ "outputs": [], "source": [ "import proveit\n", - "theory = proveit.Theory() # the theorem's theory" + "theory = proveit.Theory() # the theorem's theory\n", + "from proveit.linear_algebra.inner_products import norm_def\n", + "from proveit.physics.quantum.algebra import bra_def\n", + "from proveit.physics.quantum import psi, varphi,ket_psi\n", + "from proveit.linear_algebra import Hspace\n", + "from proveit import x,K,H\n", + "from proveit.numbers import Complex\n", + "from proveit.logic import InSet\n", + "from proveit import defaults" ] }, { @@ -32,12 +40,104 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "defaults.assumptions=ket_self_projection.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "lhs=ket_self_projection.instance_expr.instance_expr.lhs" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def_inst=bra_def.instantiate({varphi:psi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "lhs.projection()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def_inst.substitution(lhs)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def_inst=norm_def.instantiate({x:ket_psi,K:Complex,H:Hspace})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InSet(norm_def_inst.lhs,Complex)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def_inst.square_both_sides()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb new file mode 100644 index 000000000000..17dbe40a0b54 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.physics.quantum.algebra.no_cloning theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving no_cloning" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/allowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_bra_is_linmap/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/thm_proof.ipynb new file mode 100644 index 000000000000..32b46da61ee7 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.physics.quantum.algebra.qmult_of_linear_maps theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving qmult_of_linear_maps" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/physics/quantum/algebra/qmult.py b/packages/proveit/physics/quantum/algebra/qmult.py index 1440dedc73f6..14562034105e 100644 --- a/packages/proveit/physics/quantum/algebra/qmult.py +++ b/packages/proveit/physics/quantum/algebra/qmult.py @@ -200,7 +200,7 @@ def projection(self,**defaults_config): # pass yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces for _Hspace in yield_known_hilbert_spaces(ket): - if isinstance(M, Bra) and M.operand==ket.operand: + if isinstance(M, Bra) and M.operand==ket.operand and ket_self_projection.is_usable(): #if M.operand==ket.operand: #print("same") self_proj_eq=ket_self_projection.instantiate({Hspace: _Hspace, psi:ket.operand}) From 54ba27fd227baa2f20ed37ce83fbaf405e43c294 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Tue, 16 Jul 2024 08:36:15 +0530 Subject: [PATCH 08/29] update in inner_product_spaces.py last update --- .../_theory_nbs_/demonstrations.ipynb | 33 ++++++- .../_theory_nbs_/theorems.ipynb | 7 ++ .../inner_products/hilbert_spaces.py | 4 + .../inner_products/inner_prod.py | 57 ++++++++++-- .../inner_products/inner_prod_spaces.py | 22 ++++- .../proofs/fold_not_equals/thm_proof.ipynb | 2 +- .../equality/_theory_nbs_/theorems.ipynb | 2 +- .../algebra/_theory_nbs_/demonstrations.ipynb | 89 ++++++++++++++++++- .../ket_self_projection/thm_proof.ipynb | 36 +++++++- .../qmult_of_bra/allowed_presumptions.txt | 0 .../qmult_of_bra/disallowed_presumptions.txt | 0 .../allowed_presumptions.txt | 3 + .../qmult_of_bra_as_map/thm_proof.ipynb | 85 +++++++++++++++++- 13 files changed, 324 insertions(+), 16 deletions(-) create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb index 306537fbc558..1e6998074653 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb @@ -15,6 +15,15 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.numbers import Complex\n", + "from proveit.linear_algebra import (\n", + " VecSpaces, InnerProdSpaces, HilbertSpaces, Hspace, VecAdd, VecZero, VecSum, LinMap, Identity, Commutator,\n", + " ScalarMult, InnerProd, Norm, Adj, OrthoProj, Span, OrthoNormBases, Dim, TensorProd)\n", + "from proveit import n, a, b, i, m, n, v, w, x, y, z, A, B, K, H, M, P, U, X, alpha\n", + "from proveit.linear_algebra.inner_products import inner_prod_field_membership,inner_prod_complex_membership\n", + "from proveit.logic import (\n", + " And, Forall, Exists, Iff, InSet, Set, SubsetEq, CartExp, InClass, Equals, NotEquals,Implies)\n", "%begin demonstrations" ] }, @@ -23,7 +32,27 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "defaults.assumptions=[InClass(P,InnerProdSpaces(K)),InClass(U,HilbertSpaces)]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_field_membership.instantiate({H:P,x:n,y:w})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_complex_membership.instantiate({H:U,x:n,y:w})" + ] }, { "cell_type": "code", @@ -37,7 +66,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb index 0e1dce04572c..cdf25e36bebc 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb @@ -646,6 +646,13 @@ "source": [ "%end theorems" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/packages/proveit/linear_algebra/inner_products/hilbert_spaces.py b/packages/proveit/linear_algebra/inner_products/hilbert_spaces.py index 0b6ec5ad2d22..e7ef1bafd601 100644 --- a/packages/proveit/linear_algebra/inner_products/hilbert_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/hilbert_spaces.py @@ -16,6 +16,10 @@ def __init__(self, *, styles=None): self, string_format='HilbertSpaces', latex_format=r'\textrm{HilbertSpaces}', styles=styles) + + @property + def field(self): + return Complex def membership_object(self, element): return HilbertSpacesMembership(element, self) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod.py b/packages/proveit/linear_algebra/inner_products/inner_prod.py index 2a20e09286b4..0d9a25cbf7ae 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod.py @@ -1,5 +1,5 @@ from proveit import (Operation, Literal, UnsatisfiedPrerequisites, - equality_prover) + equality_prover,relation_prover) from proveit import a, b, x, y, z, H, K from proveit.logic import is_irreducible_value @@ -21,6 +21,7 @@ def latex(self, **kwargs): return (r'\left \langle ' + _a.latex() + ', ' + _b.latex() + r'\right \rangle') + @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): @@ -63,7 +64,53 @@ def shallow_simplification(self, *, must_evaluate=False, if must_evaluate and not is_irreducible_value(simp.rhs): return simp.inner_expr().rhs.evaluate() return simp - - - - + + @relation_prover + def deduce_membership(self, K, **defaults_config,): + from . import inner_prod_field_membership,inner_prod_complex_membership + from proveit.linear_algebra import InnerProdSpaces, HilbertSpaces + from proveit.numbers import Complex + _x,_y=self.operands + inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) + inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) + inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) + fields=set() + for inner_prod_space in inner_prod_spaces: + if inner_prod_space.field == K: + return True + fields.add(inner_prod_space.field) + if K==Complex: + yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces + for _Hspace in yield_known_hilbert_spaces(K): + return inner_prod_complex_membership.instantiate({H:_Hspace,x:_x,y:_y}) + else: + yield_known_inner_prod_spaces=InnerProdSpaces.yield_known_inner_prod_spaces + for _ISpace in yield_known_inner_prod_spaces(K): + return inner_prod_field_membership.instantiate({H:_ISpace,x:_x,y:_y}) + raise UnsatisfiedPrerequisites( + "No known Hilbert space containing %s"%self + ) + + def readily_provable_membership(self, K): + ''' + Return True iff we can readily prove that this InnerProd + evaluates to something in set K. + ''' + from proveit.linear_algebra import InnerProdSpaces + _x,_y=self.operands + inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) + inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) + inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) + fields=set() + for inner_prod_space in inner_prod_spaces: + if inner_prod_space.field == K: + return True + fields.add(inner_prod_space.field) + for field in fields: + if hasattr(field, 'readily_includes') and field.readily_includes(K): + return True + return False + + @property + def field(self): + return Complex \ No newline at end of file diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index d0fcc2db124f..536ce03ff3d0 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -107,7 +107,27 @@ def known_inner_prod_spaces(vecs, *, field=None): return [VecSpaces.known_inner_prod_space(operand, field=field) for operand in vecs] - + @staticmethod + def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): + if isinstance(vec_or_vecs, Expression): + for space in InnerProdSpaces._yield_known_inner_prod_spaces_of_vec(vec_or_vecs): + space_field = space.field + if space_field == K or (hasattr(space_field, ‘readily_includes’) and space_field.readily_includes(K)): + yield space + else: + space_intersection = set() + for vec in vec_or_vecs: + spaces = set() + for space in InnerProdSpaces.yield_readily_provable_inner_prod_spaces (vec, field=field) + spaces.add(space) + + inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) + inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) + inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) + fields=set() + # exercise for Sudhindu + # yield appropriate spaces + # exercise for Sudhindu class InnerProdSpacesMembership(ClassMembership): def __init__(self, element, domain): diff --git a/packages/proveit/logic/equality/_theory_nbs_/proofs/fold_not_equals/thm_proof.ipynb b/packages/proveit/logic/equality/_theory_nbs_/proofs/fold_not_equals/thm_proof.ipynb index 87968c4a11bd..6698b83ee827 100644 --- a/packages/proveit/logic/equality/_theory_nbs_/proofs/fold_not_equals/thm_proof.ipynb +++ b/packages/proveit/logic/equality/_theory_nbs_/proofs/fold_not_equals/thm_proof.ipynb @@ -76,7 +76,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/logic/equality/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/equality/_theory_nbs_/theorems.ipynb index c7429b44c757..c6e1e0821e40 100644 --- a/packages/proveit/logic/equality/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/logic/equality/_theory_nbs_/theorems.ipynb @@ -373,7 +373,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb index 0d9b353febe1..c026d4bd394a 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb @@ -26,7 +26,7 @@ "from proveit.physics.quantum import (\n", " psi, bra_psi, ket_psi, varphi, bra_varphi, ket_varphi,var_ket_psi)\n", "from proveit.physics.quantum.algebra import QmultCodomain\n", - "from proveit.physics.quantum.algebra import qmult_of_bra_as_map\n", + "from proveit.physics.quantum.algebra import qmult_of_bra_as_map,bra_def,qmult_of_bra\n", "from proveit.linear_algebra import (\n", " VecSpaces, HilbertSpaces, Hspace, VecZero, LinMap, Commutator,\n", " MatrixSpace, MatrixMult, Unitary, Diagonal, ScalarMult, TensorProd, Identity,\n", @@ -131,7 +131,9 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "adjoint_binary_distribution.instantiate({Hspace:H,X:X,Y:Y})" + ] }, { "cell_type": "code", @@ -139,7 +141,7 @@ "metadata": {}, "outputs": [], "source": [ - "adjoint_binary_distribution.instantiate({Hspace:H,X:X,Y:Y})" + "Qmult(A,B)" ] }, { @@ -148,7 +150,7 @@ "metadata": {}, "outputs": [], "source": [ - "Qmult(A,B)" + "CartExp(Complex, n)" ] }, { @@ -250,6 +252,78 @@ "Bra(psi)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_as_map" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def.instantiate({Hspace:H,varphi:varphi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra.instantiate({Hspace:H,varphi:varphi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_as_map.instantiate({Hspace:H,varphi:varphi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" + ] + }, { "cell_type": "code", "execution_count": null, @@ -937,6 +1011,13 @@ "source": [ "%end demonstrations" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb index 9cec79bdcf6c..4b3e06c82fb2 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb @@ -113,7 +113,34 @@ "metadata": {}, "outputs": [], "source": [ - "InSet(norm_def_inst.lhs,Complex)" + "InSet(norm_def_inst.rhs,Complex).readily_provable()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "dir(norm_def_inst)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def_inst.rhs.base.operands" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def_inst.rhs.base.deduce_membership(Complex)" ] }, { @@ -125,6 +152,13 @@ "norm_def_inst.square_both_sides()" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/allowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt index e69de29bb2d1..8c6f642dfcd6 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/allowed_presumptions.txt @@ -0,0 +1,3 @@ +proveit.physics.quantum.algebra.qmult_of_bra +proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space +proveit.logic.equality.sub_left_side_into diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb index db034d2bc17b..c4a4684dd47e 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb @@ -15,6 +15,17 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.physics.quantum.algebra import qmult_of_bra_as_map,qmult_of_bra,bra_def\n", + "from proveit.physics.quantum import (\n", + " Qmult, Bra, Ket, NumBra, NumKet, ket0, ket1, bra0, bra1, m_ket_domain,\n", + " psi, varphi, ket_psi, ket_varphi, bra_varphi, \n", + " var_ket_psi, var_ket_varphi, var_ket_v, QubitSpace, QubitRegisterSpace)\n", + "from proveit.linear_algebra import VecAdd, MatrixSpace, Hspace\n", + "from proveit import alpha, beta, gamma, delta, j, m, n, b, c, A, B, C, D,H,a,X,Y\n", + "from proveit.logic import Forall, InSet, CartExp, InClass,Equals\n", + "from proveit.numbers import Complex, NaturalPos,one\n", + "\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +38,78 @@ "%proving qmult_of_bra_as_map" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions=qmult_of_bra_as_map.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions+=[InSet(n, NaturalPos),InSet(ket_varphi, CartExp(Complex, n))]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "bra_def_instance=bra_def.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_instance=qmult_of_bra.instantiate({Hspace:CartExp(Complex,n),varphi:varphi},auto_simplify=False)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_instance.apply_transitivities([bra_def_instance])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +120,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } From 09ef43730b11dfbf16a7003f27142400a81bee62 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Wed, 24 Jul 2024 12:22:44 -0500 Subject: [PATCH 09/29] Update an InnerProdSpaces method 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. --- .../inner_products/inner_prod_spaces.py | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index 536ce03ff3d0..5d53d209252d 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -109,25 +109,32 @@ def known_inner_prod_spaces(vecs, *, field=None): @staticmethod def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): + ''' + For the given list vec_or_vecs of vectors, yield the set of + inner product spaces (aka Hilbert spaces) which the vectors + have in common. + ''' if isinstance(vec_or_vecs, Expression): - for space in InnerProdSpaces._yield_known_inner_prod_spaces_of_vec(vec_or_vecs): + for space in InnerProdSpaces._yield_known_inner_prod_spaces_of_vec( + vec_or_vecs): space_field = space.field - if space_field == K or (hasattr(space_field, ‘readily_includes’) and space_field.readily_includes(K)): + if (space_field == field or + (hasattr(space_field, 'readily_includes') + and space_field.readily_includes(field))): yield space - else: - space_intersection = set() + else: + # assuming our list of vectors and each related set of + # inner prod spaces isn't very large + list_of_space_sets = [] for vec in vec_or_vecs: spaces = set() - for space in InnerProdSpaces.yield_readily_provable_inner_prod_spaces (vec, field=field) + for space in (InnerProdSpaces. + yield_readily_provable_inner_prod_spaces( + vec, field=field)): spaces.add(space) - - inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) - inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) - inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) - fields=set() - # exercise for Sudhindu - # yield appropriate spaces - # exercise for Sudhindu + list_of_space_sets.add(spaces) + space_intersection = set.intersection(*list_of_space_sets) + yield space_intersection class InnerProdSpacesMembership(ClassMembership): def __init__(self, element, domain): From 4c36f8f8b5d782206fd6c4668cc914523837b9f2 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 26 Jul 2024 09:25:51 -0600 Subject: [PATCH 10/29] Update some quantum/algebra/demos assumptions 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: #313. --- .../quantum/algebra/_theory_nbs_/demonstrations.ipynb | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb index c026d4bd394a..0a91f8dd9fcc 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/demonstrations.ipynb @@ -285,7 +285,7 @@ "metadata": {}, "outputs": [], "source": [ - "bra_def.instantiate({Hspace:H,varphi:varphi})" + "bra_def.instantiate({Hspace:H,varphi:varphi}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" ] }, { @@ -294,7 +294,7 @@ "metadata": {}, "outputs": [], "source": [ - "qmult_of_bra.instantiate({Hspace:H,varphi:varphi})" + "qmult_of_bra.instantiate({Hspace:H,varphi:varphi}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" ] }, { @@ -303,7 +303,7 @@ "metadata": {}, "outputs": [], "source": [ - "qmult_of_bra_as_map.instantiate({Hspace:H,varphi:varphi})" + "qmult_of_bra_as_map.instantiate({Hspace:H,varphi:varphi}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" ] }, { From aa2733f1e99b9c7a1a82804ebcbec4c60c1b6aea Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 26 Jul 2024 10:39:47 -0600 Subject: [PATCH 11/29] Clean up proof of quantum/algebra qmult_of_bra_as_map thm 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: #313 . --- .../qmult_of_bra_as_map/thm_proof.ipynb | 65 +------------------ 1 file changed, 1 insertion(+), 64 deletions(-) diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb index c4a4684dd47e..ca20b775ed54 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb @@ -15,16 +15,7 @@ "outputs": [], "source": [ "import proveit\n", - "from proveit import defaults\n", - "from proveit.physics.quantum.algebra import qmult_of_bra_as_map,qmult_of_bra,bra_def\n", - "from proveit.physics.quantum import (\n", - " Qmult, Bra, Ket, NumBra, NumKet, ket0, ket1, bra0, bra1, m_ket_domain,\n", - " psi, varphi, ket_psi, ket_varphi, bra_varphi, \n", - " var_ket_psi, var_ket_varphi, var_ket_v, QubitSpace, QubitRegisterSpace)\n", - "from proveit.linear_algebra import VecAdd, MatrixSpace, Hspace\n", - "from proveit import alpha, beta, gamma, delta, j, m, n, b, c, A, B, C, D,H,a,X,Y\n", - "from proveit.logic import Forall, InSet, CartExp, InClass,Equals\n", - "from proveit.numbers import Complex, NaturalPos,one\n", + "from proveit.physics.quantum.algebra import bra_def\n", "\n", "theory = proveit.Theory() # the theorem's theory" ] @@ -38,24 +29,6 @@ "%proving qmult_of_bra_as_map" ] }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "defaults.assumptions=qmult_of_bra_as_map.all_conditions()" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "defaults.assumptions+=[InSet(n, NaturalPos),InSet(ket_varphi, CartExp(Complex, n))]" - ] - }, { "cell_type": "code", "execution_count": null, @@ -65,42 +38,6 @@ "bra_def" ] }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "qmult_of_bra" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "bra_def_instance=bra_def.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "qmult_of_bra_instance=qmult_of_bra.instantiate({Hspace:CartExp(Complex,n),varphi:varphi},auto_simplify=False)" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - "qmult_of_bra_instance.apply_transitivities([bra_def_instance])" - ] - }, { "cell_type": "code", "execution_count": null, From a457184cfcd486b9d71af9f888033a6e3791236c Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 26 Jul 2024 19:44:23 -0600 Subject: [PATCH 12/29] Update InnerProdSpaces.yield_readily... method 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 #313 . --- .../linear_algebra/inner_products/inner_prod_spaces.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index 5d53d209252d..8ca58f5ba328 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -114,7 +114,9 @@ def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): inner product spaces (aka Hilbert spaces) which the vectors have in common. ''' - if isinstance(vec_or_vecs, Expression): + if (isinstance(vec_or_vecs, Expression) + and not isinstance(vec_or_vecs, ExprTuple)): + # we have a single vector to consider for space in InnerProdSpaces._yield_known_inner_prod_spaces_of_vec( vec_or_vecs): space_field = space.field @@ -123,8 +125,7 @@ def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): and space_field.readily_includes(field))): yield space else: - # assuming our list of vectors and each related set of - # inner prod spaces isn't very large + # we have a list of vectors list_of_space_sets = [] for vec in vec_or_vecs: spaces = set() From 9ba53e2a16aba3a5b3cdbd0127475340cc46cfa0 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 18:57:07 -0600 Subject: [PATCH 13/29] Establish proof of linear_algebra/inner_products/inner_prod_field_membership 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: #314. --- .../allowed_presumptions.txt | 3 ++ .../disallowed_presumptions.txt | 0 .../thm_proof.ipynb | 50 ++++++++++++++++++- 3 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/allowed_presumptions.txt create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/disallowed_presumptions.txt diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/allowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/allowed_presumptions.txt new file mode 100644 index 000000000000..e2ae1702f707 --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/allowed_presumptions.txt @@ -0,0 +1,3 @@ +proveit.logic.equality.equals_reversal +proveit.logic.booleans.conjunction.right_from_and +proveit.logic.equality.rhs_via_equality diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/disallowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb index 13cb778db433..f59becde04f6 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb @@ -15,6 +15,9 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.linear_algebra.inner_products import inner_prod_space_def\n", + "\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +30,51 @@ "%proving inner_prod_field_membership" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = inner_prod_field_membership.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def_inst = inner_prod_space_def.instantiate()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def_inst.derive_right_via_equality()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +85,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } From 3f0fe9c638314309f7b155b0dbe99dbbc186e4a3 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:01:01 -0600 Subject: [PATCH 14/29] Establish proof of linear_algebra/inner_products/inner_prod_complex_membership 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: #314. --- .../allowed_presumptions.txt | 2 + .../disallowed_presumptions.txt | 0 .../thm_proof.ipynb | 46 ++++++++++++++++++- 3 files changed, 46 insertions(+), 2 deletions(-) create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/allowed_presumptions.txt create mode 100644 packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/disallowed_presumptions.txt diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/allowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/allowed_presumptions.txt new file mode 100644 index 000000000000..c54fd75649cc --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/allowed_presumptions.txt @@ -0,0 +1,2 @@ +proveit.linear_algebra.inner_products.inner_prod_field_membership +proveit.linear_algebra.inner_products.hilbert_space_is_inner_prod_space diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/disallowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb index a3dd2a19b29e..bf4208fed0a8 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb @@ -15,6 +15,10 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults, K\n", + "from proveit.numbers import Complex\n", + "from proveit.linear_algebra.inner_products import hilbert_space_def, inner_prod_field_membership\n", + "\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -32,12 +36,50 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "defaults.assumptions = inner_prod_complex_membership.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hilbert_space_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_field_membership" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_field_membership.instantiate({K:Complex})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } From 388d0adb176d542751ba33d52a969dfeea32ce46 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:39:57 -0600 Subject: [PATCH 15/29] Incremental upgrades to linear_algebra/inner_products/inner_prod_spaces.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). --- .../inner_products/inner_prod_spaces.py | 24 ++++++++++++++----- 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index 8ca58f5ba328..4d3a09223bfd 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -35,6 +35,7 @@ def __init__(self, field, *, styles=None, _operator=None): if _operator is None: _operator = InnerProdSpaces._operator_ VecSpaces.__init__(self, field, styles=styles, _operator=_operator) + # self.field = field ?? Do we already have a self.field? See further below. def membership_object(self, element): return InnerProdSpacesMembership(element, self) @@ -65,9 +66,10 @@ def yield_known_inner_prod_spaces(vec, *, field=None): yield vec_space else: try: - yield deduce_as_inner_prod_space(vec_space) + deduce_as_inner_prod_space(vec_space) + yield vec_space except NotImplementedError: - # Not known you to prove 'vec_space' is an inner + # Not known how to prove 'vec_space' is an inner # product space. pass @@ -111,14 +113,24 @@ def known_inner_prod_spaces(vecs, *, field=None): def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): ''' For the given list vec_or_vecs of vectors, yield the set of - inner product spaces (aka Hilbert spaces) which the vectors - have in common. + inner product spaces (i.e. the vector spaces equipped with + an inner product) which the vectors have in common. ''' + from proveit import Expression, ExprTuple if (isinstance(vec_or_vecs, Expression) and not isinstance(vec_or_vecs, ExprTuple)): # we have a single vector to consider - for space in InnerProdSpaces._yield_known_inner_prod_spaces_of_vec( + for space in InnerProdSpaces.yield_known_inner_prod_spaces( vec_or_vecs): + try: + # unfortunately, the following does NOT guarantee + # that 'space' is an actual VecSpace w/assoc'd field + space = space.deduce_as_vec_space().rhs + # print(f'space = {space}') + except Exception: + print(f'Exception') + pass + # we are still not guaranteed that space.field exists! space_field = space.field if (space_field == field or (hasattr(space_field, 'readily_includes') @@ -133,7 +145,7 @@ def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): yield_readily_provable_inner_prod_spaces( vec, field=field)): spaces.add(space) - list_of_space_sets.add(spaces) + list_of_space_sets.append(spaces) space_intersection = set.intersection(*list_of_space_sets) yield space_intersection From f6f494a5a7173d35244c4f3ffd367da005dbfc55 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:43:55 -0600 Subject: [PATCH 16/29] Incremental upgrades to linear_algebra/inner_products/inner_prod.py 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). --- .../inner_products/inner_prod.py | 42 +++++++++++++------ 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod.py b/packages/proveit/linear_algebra/inner_products/inner_prod.py index 0d9a25cbf7ae..dc2eeb154bf2 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod.py @@ -70,21 +70,28 @@ def deduce_membership(self, K, **defaults_config,): from . import inner_prod_field_membership,inner_prod_complex_membership from proveit.linear_algebra import InnerProdSpaces, HilbertSpaces from proveit.numbers import Complex - _x,_y=self.operands - inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) - inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) - inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) - fields=set() + from proveit.logic import CartExp + _x, _y = self.operands + # inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) + # inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) + # inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) + # attempted replacement + inner_prod_spaces = ( + InnerProdSpaces. + yield_readily_provable_inner_prod_spaces((_x, _y), field=K)) + fields = set() for inner_prod_space in inner_prod_spaces: + # if isinstance(inner_prod_space, CartExp): + # print(f'{inner_prod_space} is a CartExp expression!') if inner_prod_space.field == K: - return True + return True # this is weird -- returning a boolean? some left-over garbage here. fields.add(inner_prod_space.field) - if K==Complex: + if K == Complex: yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces for _Hspace in yield_known_hilbert_spaces(K): return inner_prod_complex_membership.instantiate({H:_Hspace,x:_x,y:_y}) else: - yield_known_inner_prod_spaces=InnerProdSpaces.yield_known_inner_prod_spaces + yield_known_inner_prod_spaces = InnerProdSpaces.yield_known_inner_prod_spaces for _ISpace in yield_known_inner_prod_spaces(K): return inner_prod_field_membership.instantiate({H:_ISpace,x:_x,y:_y}) raise UnsatisfiedPrerequisites( @@ -96,13 +103,22 @@ def readily_provable_membership(self, K): Return True iff we can readily prove that this InnerProd evaluates to something in set K. ''' + # print(f'Entering InnerProd.readily_provable_membership() with self = {self}') from proveit.linear_algebra import InnerProdSpaces - _x,_y=self.operands - inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) - inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) - inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) - fields=set() + _x, _y = self.operands + # the next 3 lines to be replaced with a call to the static method + # InnerProdSpaces.yield_readily_provable_inner_prod_spaces() + # inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) + # inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) + # inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) + # attempted replacement + inner_prod_spaces = ( + InnerProdSpaces. + yield_readily_provable_inner_prod_spaces((_x, _y), field=K)) + fields = set() for inner_prod_space in inner_prod_spaces: + # if isinstance(inner_prod_space, CartExp): + # print(f'{inner_prod_space} is a CartExp expression!') if inner_prod_space.field == K: return True fields.add(inner_prod_space.field) From 55e2ddfbd308a1d1684832ef1f3601fdac396bbe Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:46:32 -0600 Subject: [PATCH 17/29] Update descriptive/explanatory comments in linear_algebra/matrices/identity.py Update descriptive/explanatory comments in linear_algebra/matrices/identity.py and provide some trivial reformatting for line length standards. --- .../proveit/linear_algebra/matrices/identity.py | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/packages/proveit/linear_algebra/matrices/identity.py b/packages/proveit/linear_algebra/matrices/identity.py index d9a43537c6ce..57b26bf52531 100644 --- a/packages/proveit/linear_algebra/matrices/identity.py +++ b/packages/proveit/linear_algebra/matrices/identity.py @@ -2,20 +2,25 @@ class Identity(Function): ''' - The identity map of a vector space is a linear map that maps - any element to itself. + Represents the n x n identity matrix associated with the identity + map of a vector space. The identity map is a linear map that maps + any any element of a vector space to itself. ''' - _operator_ = Literal(string_format='1',latex_format=r'\mathbbm{1}', theory=__file__) + _operator_ = Literal(string_format='1', + latex_format=r'\mathbbm{1}', theory=__file__) def _config_latex_tool(self, lt): if 'bbm' not in lt.packages: lt.packages.append('bbm') - def __init__(self,size, *, styles=None): + def __init__(self, size, *, styles=None): ''' - Denote the set of linear maps that map from and to the given - vectors spaces. + Initialize a representation of a (size x size) identity matrix + associated with the identity map on a vector space. + For example, the 3 x 3 identity matrix on R^3 could be + intialized with Identity(num(3)). + ''' Function.__init__(self, Identity._operator_, size, styles=styles) From 25c78c17c847dcf468d7c3a48b3a1fe2b2d3f1d7 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:47:48 -0600 Subject: [PATCH 18/29] Augment descriptive comments in linear_algebra/matrices/transposition/unitary_group.py --- .../linear_algebra/matrices/transposition/unitary_group.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/packages/proveit/linear_algebra/matrices/transposition/unitary_group.py b/packages/proveit/linear_algebra/matrices/transposition/unitary_group.py index d3ca6b256cd2..cc5631242fb2 100644 --- a/packages/proveit/linear_algebra/matrices/transposition/unitary_group.py +++ b/packages/proveit/linear_algebra/matrices/transposition/unitary_group.py @@ -15,7 +15,8 @@ class Unitary(Function): def __init__(self, n, *, styles=None): ''' - Create some U(n), the unitary group of degree n. + Create some U(n), the unitary group of degree n, consisting + of (the group of) all n x n unitary matrices. ''' Function.__init__(self, Unitary._operator_, n, styles=styles) # self.operand = n @@ -49,7 +50,9 @@ class SpecialUnitary(Function): def __init__(self, n, *, styles=None): ''' - Create some SU(n), the special unitary group of degree n. + Create some SU(n), the special unitary group of degree n, + consisting of (the group of) all n x n unitary matrices with + determinant 1. ''' Function.__init__(self, SpecialUnitary._operator_, n, styles=styles) # self.operand = n From c4159712a2195ad97905d985b125e2cc70b7d3be Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:49:43 -0600 Subject: [PATCH 19/29] Incremental augmentation of demos nb in linear_algebra/inner_products --- .../_theory_nbs_/demonstrations.ipynb | 148 +++++++++++++++++- 1 file changed, 140 insertions(+), 8 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb index 1e6998074653..fc4b37a046a7 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb @@ -16,14 +16,11 @@ "source": [ "import proveit\n", "from proveit import defaults\n", - "from proveit.numbers import Complex\n", - "from proveit.linear_algebra import (\n", - " VecSpaces, InnerProdSpaces, HilbertSpaces, Hspace, VecAdd, VecZero, VecSum, LinMap, Identity, Commutator,\n", - " ScalarMult, InnerProd, Norm, Adj, OrthoProj, Span, OrthoNormBases, Dim, TensorProd)\n", - "from proveit import n, a, b, i, m, n, v, w, x, y, z, A, B, K, H, M, P, U, X, alpha\n", - "from proveit.linear_algebra.inner_products import inner_prod_field_membership,inner_prod_complex_membership\n", - "from proveit.logic import (\n", - " And, Forall, Exists, Iff, InSet, Set, SubsetEq, CartExp, InClass, Equals, NotEquals,Implies)\n", + "from proveit.numbers import Complex, NaturalPos, Real\n", + "from proveit.linear_algebra import VecSpaces, InnerProdSpaces, HilbertSpaces, InnerProd\n", + "from proveit import m, n, v, w, x, y, K, H, P, U\n", + "from proveit.linear_algebra.inner_products import inner_prod_field_membership, inner_prod_complex_membership\n", + "from proveit.logic import CartExp, Equals, InClass, InSet\n", "%begin demonstrations" ] }, @@ -36,6 +33,13 @@ "defaults.assumptions=[InClass(P,InnerProdSpaces(K)),InClass(U,HilbertSpaces)]" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Testing the instantiation of some theorems underlying important `InnerProd` methods." + ] + }, { "cell_type": "code", "execution_count": null, @@ -54,6 +58,134 @@ "inner_prod_complex_membership.instantiate({H:U,x:n,y:w})" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Testing `InnerProd` and `InnerProdSpaces` methods." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = [InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "vec_space_claim = CartExp(Complex, n).deduce_as_vec_space()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "vec_space_claim.rhs.field" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from proveit.linear_algebra.vector_spaces import including_vec_space\n", + "supposed_vec_space = including_vec_space(CartExp(Complex, n), field=Complex)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# WW thought this would lead to an error without more work in the including_vec_space() method\n", + "supposed_vec_space_Rn = including_vec_space(CartExp(Real, n), field=Complex)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# notice here that the supposed vec space is just a set without any associated field:\n", + "try:\n", + " some_field = supposed_vec_space.field\n", + "except Exception as the_exception:\n", + " print(f'{the_exception}')" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InnerProd(v, w)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = [InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "set(VecSpaces.yield_known_vec_spaces(v))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "set(VecSpaces.yield_known_vec_spaces(w))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "list(InnerProdSpaces.yield_known_inner_prod_spaces(v))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# and we continue to get into trouble trying to get a field from a set, even\n", + "# if the set is acknowledged to be (in some sense) a VecSpace\n", + "try:\n", + " InnerProd(v, w).deduce_membership(\n", + " Complex,\n", + " assumptions=[InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))])\n", + "except Exception as the_exception:\n", + " print(f'{the_exception}')" + ] + }, { "cell_type": "code", "execution_count": null, From a390a1b3bd8ad26f6f11e4eaf8d5fb4a4d248f13 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:51:26 -0600 Subject: [PATCH 20/29] Incremental update of demos nb in linear_algebra/matrices/transposition --- .../_theory_nbs_/demonstrations.ipynb | 37 +++++++++++++++---- 1 file changed, 29 insertions(+), 8 deletions(-) diff --git a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb index fb349d68e61c..5ed8297fa6eb 100644 --- a/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb @@ -15,19 +15,34 @@ "outputs": [], "source": [ "import proveit\n", - "from proveit import n,c, x, y, A, B, K, P, V, W, Px, Py,N,C,U\n", - "from proveit.numbers import one,two\n", - "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices,unitary_unitary_dag,unitary_dag_unitary\n", + "from proveit import n\n", + "from proveit.numbers import two\n", + "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices, unitary_unitary_dag, unitary_dag_unitary\n", "%begin demonstrations" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The unitary group $U(n)$ is the group of $n \\times n$ unitary matrices, with the group operation being the usual matrix multiplication.
\n", + "$U(n)$ is a subset of the set $\\mathbb{C}^{2 \\times 2}$ of all $n \\times n$ complex matrices." + ] + }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ - "x=unitaries_are_matrices.instantiate({n:two})" + "unitaries_are_matrices" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For example, the group of $2 \\times 2$ unitary matrices is a subset of the set of all $2 \\times 2$ complex matrices:" ] }, { @@ -36,7 +51,14 @@ "metadata": {}, "outputs": [], "source": [ - "unitary_unitary_dag.instantiate({n:two})" + "unitaries_are_matrices.instantiate({n:two})" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By definition, the adjoint of unitary $U$ is the inverse of $U$, giving $UU^{\\dagger} = U^{\\dagger}U = \\mathbb{1}_{n}$. For $n = 2$, we have:" ] }, { @@ -45,7 +67,7 @@ "metadata": {}, "outputs": [], "source": [ - "unitary_dag_unitary.instantiate({n:two})" + "unitary_unitary_dag.instantiate({n:two})" ] }, { @@ -54,8 +76,7 @@ "metadata": {}, "outputs": [], "source": [ - "for i in range(3,6):\n", - " print(i)" + "unitary_dag_unitary.instantiate({n:two})" ] }, { From 3da74577aa355bb8192de5d17a6340dfe47edbd0 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Fri, 2 Aug 2024 19:52:52 -0600 Subject: [PATCH 21/29] Augment and clean up demos nb in linear_algebra/matrices --- .../_theory_nbs_/demonstrations.ipynb | 62 ++++++++++++++++++- 1 file changed, 59 insertions(+), 3 deletions(-) diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb index 79f4aee8c7d0..ca364a0476a0 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb @@ -15,12 +15,36 @@ "outputs": [], "source": [ "import proveit\n", - "from proveit import n,c, x, y, A, B, K, P, V, W, Px, Py,N,C\n", - "from proveit.numbers import one,two\n", - "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices,Unitary_Unitary_dag\n", + "from proveit import n\n", + "from proveit.numbers import one, two, three\n", + "from proveit.linear_algebra.matrices import Identity\n", + "from proveit.linear_algebra.matrices.transposition import unitaries_are_matrices, unitary_unitary_dag\n", "%begin demonstrations" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "$n \\times n$ identity matrices are represented using `Identity(n)` and appear as $\\mathbb{1}_{n}$:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "I_1, I_2, I_n = Identity(two), Identity(three), Identity(n)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Unitaries are complex square matrices:" + ] + }, { "cell_type": "code", "execution_count": null, @@ -30,6 +54,38 @@ "unitaries_are_matrices.instantiate({n:two})" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By definition, the adjoint of unitary $U$ is the inverse of $U$:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_unitary_dag" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "For example, if $U$ is a $2 \\times 2$ unitary, then $UU^{\\dagger} = \\mathbb{1}_{2}$:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "unitary_unitary_dag.instantiate({n:two})" + ] + }, { "cell_type": "code", "execution_count": null, From b03a1d603f17879118f638b151ff4f6ae4ca6636 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Mon, 5 Aug 2024 14:34:54 -0600 Subject: [PATCH 22/29] Update inner_prod_space_def axiom to include vector domain 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). --- .../linear_algebra/inner_products/_theory_nbs_/axioms.ipynb | 2 +- .../linear_algebra/inner_products/_theory_nbs_/theorems.ipynb | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb index 38537fe0c781..f03e1b0b8964 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb @@ -53,7 +53,7 @@ " (K, H), Equals(\n", " InClass(H, InnerProdSpaces(K)),\n", " And(InClass(H, VecSpaces(K)),\n", - " Forall((x, y), InSet(InnerProd(x, y), K)))))" + " Forall((x, y), InSet(InnerProd(x, y), K), domain=H))))" ] }, { diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb index cdf25e36bebc..b8a6465a30df 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/theorems.ipynb @@ -59,7 +59,7 @@ "source": [ "inner_prod_field_membership=Forall(\n", " (K,H),\n", - " Forall((x,y),InSet(InnerProd(x,y),K)),condition=InClass(H,InnerProdSpaces(K)))" + " Forall((x,y),InSet(InnerProd(x,y),K), domain=H),condition=InClass(H,InnerProdSpaces(K)))" ] }, { @@ -70,7 +70,7 @@ "source": [ "inner_prod_complex_membership=Forall(\n", " H,\n", - " Forall((x,y),InSet(InnerProd(x,y),Complex)),condition=InClass(H,HilbertSpaces))" + " Forall((x,y),InSet(InnerProd(x,y),Complex), domain=H),condition=InClass(H,HilbertSpaces))" ] }, { From efb142877609a2c886f17c60fc1655cd074e80d5 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Thu, 8 Aug 2024 17:40:29 -0600 Subject: [PATCH 23/29] Update InnerProdSpaces.yield_readily_provable_inner_prod_spaces() method 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). --- .../inner_products/inner_prod_spaces.py | 23 ++++++++----------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py index 4d3a09223bfd..aa28663a4257 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod_spaces.py @@ -113,25 +113,17 @@ def known_inner_prod_spaces(vecs, *, field=None): def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): ''' For the given list vec_or_vecs of vectors, yield the set of - inner product spaces (i.e. the vector spaces equipped with - an inner product) which the vectors have in common. + known or readily provable inner product spaces (i.e. the vector + spaces equipped with an inner product) which the vectors have + in common. ''' from proveit import Expression, ExprTuple if (isinstance(vec_or_vecs, Expression) and not isinstance(vec_or_vecs, ExprTuple)): # we have a single vector to consider for space in InnerProdSpaces.yield_known_inner_prod_spaces( - vec_or_vecs): - try: - # unfortunately, the following does NOT guarantee - # that 'space' is an actual VecSpace w/assoc'd field - space = space.deduce_as_vec_space().rhs - # print(f'space = {space}') - except Exception: - print(f'Exception') - pass - # we are still not guaranteed that space.field exists! - space_field = space.field + vec_or_vecs, field=field): + space_field = space.deduce_as_vec_space().rhs.field if (space_field == field or (hasattr(space_field, 'readily_includes') and space_field.readily_includes(field))): @@ -146,8 +138,11 @@ def yield_readily_provable_inner_prod_spaces(vec_or_vecs, *, field=None): vec, field=field)): spaces.add(space) list_of_space_sets.append(spaces) + + # e.g. list_of_space_sets = [{C^3}, {C^3, R^3}, {C^3}] space_intersection = set.intersection(*list_of_space_sets) - yield space_intersection + for space in space_intersection: + yield space class InnerProdSpacesMembership(ClassMembership): def __init__(self, element, domain): From fc3ebdb516227d629b7d1418160a92d44c88cef5 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Thu, 8 Aug 2024 17:44:32 -0600 Subject: [PATCH 24/29] Update InnerProd.deduce_membership() method 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. --- .../inner_products/inner_prod.py | 63 ++++++++----------- 1 file changed, 25 insertions(+), 38 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/inner_prod.py b/packages/proveit/linear_algebra/inner_products/inner_prod.py index dc2eeb154bf2..33bcf43c1040 100644 --- a/packages/proveit/linear_algebra/inner_products/inner_prod.py +++ b/packages/proveit/linear_algebra/inner_products/inner_prod.py @@ -66,62 +66,49 @@ def shallow_simplification(self, *, must_evaluate=False, return simp @relation_prover - def deduce_membership(self, K, **defaults_config,): + def deduce_membership(self, field, **defaults_config,): + ''' + Deduce and return a judgment that the InnerProd object would + evaluate to a member of the field K. For example, for vectors + v, w in an inner product space over the field of complex + numbers, calling .deduce_membership(Complex) + should return: |- in Complex. + ''' from . import inner_prod_field_membership,inner_prod_complex_membership - from proveit.linear_algebra import InnerProdSpaces, HilbertSpaces + from proveit.linear_algebra import InnerProdSpaces from proveit.numbers import Complex - from proveit.logic import CartExp _x, _y = self.operands - # inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) - # inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) - # inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) - # attempted replacement - inner_prod_spaces = ( - InnerProdSpaces. - yield_readily_provable_inner_prod_spaces((_x, _y), field=K)) - fields = set() - for inner_prod_space in inner_prod_spaces: - # if isinstance(inner_prod_space, CartExp): - # print(f'{inner_prod_space} is a CartExp expression!') - if inner_prod_space.field == K: - return True # this is weird -- returning a boolean? some left-over garbage here. - fields.add(inner_prod_space.field) - if K == Complex: - yield_known_hilbert_spaces = HilbertSpaces.yield_known_hilbert_spaces - for _Hspace in yield_known_hilbert_spaces(K): - return inner_prod_complex_membership.instantiate({H:_Hspace,x:_x,y:_y}) - else: - yield_known_inner_prod_spaces = InnerProdSpaces.yield_known_inner_prod_spaces - for _ISpace in yield_known_inner_prod_spaces(K): - return inner_prod_field_membership.instantiate({H:_ISpace,x:_x,y:_y}) + yield_spaces = ( + InnerProdSpaces.yield_readily_provable_inner_prod_spaces) + for _inner_prod_space in yield_spaces((_x, _y), field=field): + if field == Complex: + return (inner_prod_complex_membership. + instantiate({H:_inner_prod_space, x:_x, y:_y})) + return (inner_prod_field_membership. + instantiate({H:_inner_prod_space, K:field, x:_x,y:_y})) raise UnsatisfiedPrerequisites( - "No known Hilbert space containing %s"%self + f'No known Hilbert space over field {field} containing {self}.' ) def readily_provable_membership(self, K): ''' Return True iff we can readily prove that this InnerProd - evaluates to something in set K. + evaluates to something in field set K. ''' - # print(f'Entering InnerProd.readily_provable_membership() with self = {self}') from proveit.linear_algebra import InnerProdSpaces _x, _y = self.operands - # the next 3 lines to be replaced with a call to the static method - # InnerProdSpaces.yield_readily_provable_inner_prod_spaces() - # inner_prod_spaces1 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_x)) - # inner_prod_spaces2 = set(InnerProdSpaces.yield_known_inner_prod_spaces(_y)) - # inner_prod_spaces = inner_prod_spaces1.intersection(inner_prod_spaces2) - # attempted replacement inner_prod_spaces = ( InnerProdSpaces. yield_readily_provable_inner_prod_spaces((_x, _y), field=K)) fields = set() for inner_prod_space in inner_prod_spaces: - # if isinstance(inner_prod_space, CartExp): - # print(f'{inner_prod_space} is a CartExp expression!') - if inner_prod_space.field == K: + # The inner_prod_space might appear as a simple set, + # such as R^{n} or C^{n}, so we perform some extra work to + # guarantee we can access the associated field + _space_field = inner_prod_space.deduce_as_vec_space().rhs.field + if _space_field == K: return True - fields.add(inner_prod_space.field) + fields.add(_space_field) for field in fields: if hasattr(field, 'readily_includes') and field.readily_includes(K): return True From 50685e287ebd4ba9e1b7d324d59187b254d815e7 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Thu, 8 Aug 2024 17:47:56 -0600 Subject: [PATCH 25/29] Update demonstrations notebook for linear_algebra/inner_products package 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. --- .../_theory_nbs_/demonstrations.ipynb | 94 +++++++++++++------ 1 file changed, 66 insertions(+), 28 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb index fc4b37a046a7..c9b3bffebbf7 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb @@ -17,10 +17,10 @@ "import proveit\n", "from proveit import defaults\n", "from proveit.numbers import Complex, NaturalPos, Real\n", - "from proveit.linear_algebra import VecSpaces, InnerProdSpaces, HilbertSpaces, InnerProd\n", - "from proveit import m, n, v, w, x, y, K, H, P, U\n", + "from proveit.linear_algebra import InnerProdSpaces, HilbertSpaces, InnerProd\n", + "from proveit import n, v, w, x, y, K, H, U, V\n", "from proveit.linear_algebra.inner_products import inner_prod_field_membership, inner_prod_complex_membership\n", - "from proveit.logic import CartExp, Equals, InClass, InSet\n", + "from proveit.logic import CartExp, InClass, InSet\n", "%begin demonstrations" ] }, @@ -30,7 +30,9 @@ "metadata": {}, "outputs": [], "source": [ - "defaults.assumptions=[InClass(P,InnerProdSpaces(K)),InClass(U,HilbertSpaces)]" + "defaults.assumptions=[InClass(U,HilbertSpaces),\n", + " InClass(V, InnerProdSpaces(K)), InClass(H, HilbertSpaces),\n", + " InSet(v, V), InSet(w, V), InSet(x, H), InSet(y, H)]" ] }, { @@ -46,7 +48,7 @@ "metadata": {}, "outputs": [], "source": [ - "inner_prod_field_membership.instantiate({H:P,x:n,y:w})" + "inner_prod_field_membership.instantiate({H:V,x:v,y:w})" ] }, { @@ -55,14 +57,21 @@ "metadata": {}, "outputs": [], "source": [ - "inner_prod_complex_membership.instantiate({H:U,x:n,y:w})" + "inner_prod_complex_membership.instantiate({H:H,x:x,y:y})" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "#### Testing `InnerProd` and `InnerProdSpaces` methods." + "#### Testing some `InnerProd` and `InnerProdSpaces` methods and related `VecSpaces` methods." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### Some new default assumptions:" ] }, { @@ -71,7 +80,16 @@ "metadata": {}, "outputs": [], "source": [ - "defaults.assumptions = [InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))]" + "defaults.assumptions = [\n", + " InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n)),\n", + " InSet(x, CartExp(Real, n)), InSet(y, CartExp(Real, n))]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### Notice that we can deduce that the Cartesian products $C^{n}$ and $R^{n}$ are contained in the appropriate classes of vector spaces:" ] }, { @@ -80,7 +98,7 @@ "metadata": {}, "outputs": [], "source": [ - "vec_space_claim = CartExp(Complex, n).deduce_as_vec_space()" + "Cn_vec_space_claim = CartExp(Complex, n).deduce_as_vec_space()" ] }, { @@ -89,7 +107,14 @@ "metadata": {}, "outputs": [], "source": [ - "vec_space_claim.rhs.field" + "Rn_vec_space_claim = CartExp(Real, n).deduce_as_vec_space()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### We can find a specific “including” vector space for our Cartesian products as well, though in the case of Cartesian products we get a Cartesian product back again and not technically a vector space with an associated field attribute:" ] }, { @@ -99,7 +124,7 @@ "outputs": [], "source": [ "from proveit.linear_algebra.vector_spaces import including_vec_space\n", - "supposed_vec_space = including_vec_space(CartExp(Complex, n), field=Complex)" + "Cn_including_vec_space = including_vec_space(CartExp(Complex, n), field=Complex)" ] }, { @@ -108,8 +133,14 @@ "metadata": {}, "outputs": [], "source": [ - "# WW thought this would lead to an error without more work in the including_vec_space() method\n", - "supposed_vec_space_Rn = including_vec_space(CartExp(Real, n), field=Complex)" + "Rn_including_vec_space = including_vec_space(CartExp(Real, n), field=Real)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### Notice that the “including” vector space returned in the case of a Cartesian product is just the Cartesian product itself and not an explicit vector space with associated field attribute:" ] }, { @@ -118,13 +149,19 @@ "metadata": {}, "outputs": [], "source": [ - "# notice here that the supposed vec space is just a set without any associated field:\n", "try:\n", - " some_field = supposed_vec_space.field\n", + " some_field = Cn_including_vec_space.field\n", "except Exception as the_exception:\n", " print(f'{the_exception}')" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### We can form the inner product of two vectors:" + ] + }, { "cell_type": "code", "execution_count": null, @@ -135,12 +172,10 @@ ] }, { - "cell_type": "code", - "execution_count": null, + "cell_type": "markdown", "metadata": {}, - "outputs": [], "source": [ - "defaults.assumptions = [InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))]" + "##### And we can deduce the inner product's membership in a specified field:" ] }, { @@ -149,7 +184,7 @@ "metadata": {}, "outputs": [], "source": [ - "set(VecSpaces.yield_known_vec_spaces(v))" + "InnerProd(v, w).deduce_membership(Complex)" ] }, { @@ -158,7 +193,7 @@ "metadata": {}, "outputs": [], "source": [ - "set(VecSpaces.yield_known_vec_spaces(w))" + "InnerProd(x, y).deduce_membership(Real)" ] }, { @@ -167,7 +202,14 @@ "metadata": {}, "outputs": [], "source": [ - "list(InnerProdSpaces.yield_known_inner_prod_spaces(v))" + "InnerProd(v, x).deduce_membership(Complex)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### We see an (expected) error if we try to deduce that an inner product is Real when one vector is in $\\mathbb{R}^{n}$ while the other vector is in $\\mathbb{C}^{n}$:" ] }, { @@ -176,14 +218,10 @@ "metadata": {}, "outputs": [], "source": [ - "# and we continue to get into trouble trying to get a field from a set, even\n", - "# if the set is acknowledged to be (in some sense) a VecSpace\n", "try:\n", - " InnerProd(v, w).deduce_membership(\n", - " Complex,\n", - " assumptions=[InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n))])\n", + " InnerProd(v, x).deduce_membership(Real)\n", "except Exception as the_exception:\n", - " print(f'{the_exception}')" + " print(f'Exception: {the_exception}')" ] }, { From d891e37e4b8d9ab4f62fe4875e9ebd8a1b6c6010 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Thu, 8 Aug 2024 17:51:41 -0600 Subject: [PATCH 26/29] Prove three simple theorems in linear_algebra/inner_products package 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 --- .../allowed_presumptions.txt | 1 + .../thm_proof.ipynb | 40 ++++++++++++++- .../allowed_presumptions.txt | 2 + .../thm_proof.ipynb | 40 ++++++++++++++- .../allowed_presumptions.txt | 2 + .../thm_proof.ipynb | 50 ++++++++++++++++++- 6 files changed, 132 insertions(+), 3 deletions(-) diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/allowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/allowed_presumptions.txt index e69de29bb2d1..6aa517e4925f 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/allowed_presumptions.txt +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/allowed_presumptions.txt @@ -0,0 +1 @@ +proveit.logic.equality.sub_right_side_into diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/thm_proof.ipynb index 7a29f394b90d..6feea55260ca 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/thm_proof.ipynb @@ -15,6 +15,8 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.linear_algebra.inner_products import hilbert_space_def\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +29,42 @@ "%proving hilbert_space_is_inner_prod_space" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = hilbert_space_is_inner_prod_space.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hilbert_space_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hilbert_space_def.sub_right_side_into(hilbert_space_is_inner_prod_space.condition)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +75,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/allowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/allowed_presumptions.txt index e69de29bb2d1..de71ff8d981e 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/allowed_presumptions.txt +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/allowed_presumptions.txt @@ -0,0 +1,2 @@ +proveit.linear_algebra.inner_products.hilbert_space_is_inner_prod_space +proveit.linear_algebra.inner_products.inner_prod_space_is_vec_space diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/thm_proof.ipynb index 1a272809a8e6..3eb080b677bb 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/thm_proof.ipynb @@ -15,6 +15,8 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.linear_algebra.inner_products import hilbert_space_is_inner_prod_space\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +29,42 @@ "%proving hilbert_space_is_vec_space" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = hilbert_space_is_vec_space.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hilbert_space_is_inner_prod_space" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hilbert_space_is_inner_prod_space_inst = hilbert_space_is_inner_prod_space.instantiate()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +75,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/allowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/allowed_presumptions.txt index e69de29bb2d1..536fbeefa071 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/allowed_presumptions.txt +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/allowed_presumptions.txt @@ -0,0 +1,2 @@ +proveit.logic.equality.rhs_via_equality +proveit.logic.booleans.conjunction.left_from_and diff --git a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/thm_proof.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/thm_proof.ipynb index e64ae3455fbd..bd3a78aeafcd 100644 --- a/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/thm_proof.ipynb +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_space_is_vec_space/thm_proof.ipynb @@ -15,6 +15,9 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.linear_algebra.inner_products import inner_prod_space_def\n", + "\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +30,51 @@ "%proving inner_prod_space_is_vec_space" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = inner_prod_space_is_vec_space.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def_inst = inner_prod_space_def.instantiate()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_space_def_inst.derive_right_via_equality()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +85,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } From cec4806d793a2162e08d21722311add509637f79 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Mon, 12 Aug 2024 10:19:25 +0530 Subject: [PATCH 27/29] Update thm_proof.ipynb --- .../proofs/qmult_of_bra_as_map/thm_proof.ipynb | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb index c4a4684dd47e..27ef0d085eba 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_bra_as_map/thm_proof.ipynb @@ -44,7 +44,7 @@ "metadata": {}, "outputs": [], "source": [ - "defaults.assumptions=qmult_of_bra_as_map.all_conditions()" + "#defaults.assumptions=qmult_of_bra_as_map.all_conditions()" ] }, { @@ -53,7 +53,7 @@ "metadata": {}, "outputs": [], "source": [ - "defaults.assumptions+=[InSet(n, NaturalPos),InSet(ket_varphi, CartExp(Complex, n))]" + "#defaults.assumptions+=[InSet(n, NaturalPos),InSet(ket_varphi, CartExp(Complex, n))]" ] }, { @@ -80,7 +80,7 @@ "metadata": {}, "outputs": [], "source": [ - "bra_def_instance=bra_def.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" + "#bra_def_instance=bra_def.instantiate({Hspace:CartExp(Complex,n),varphi:varphi})" ] }, { @@ -89,7 +89,7 @@ "metadata": {}, "outputs": [], "source": [ - "qmult_of_bra_instance=qmult_of_bra.instantiate({Hspace:CartExp(Complex,n),varphi:varphi},auto_simplify=False)" + "#qmult_of_bra_instance=qmult_of_bra.instantiate({Hspace:CartExp(Complex,n),varphi:varphi},auto_simplify=False)" ] }, { @@ -98,7 +98,7 @@ "metadata": {}, "outputs": [], "source": [ - "qmult_of_bra_instance.apply_transitivities([bra_def_instance])" + "#qmult_of_bra_instance.apply_transitivities([bra_def_instance])" ] }, { From 8852551151f75c1d98fd38b0e097b4c1d2dc4fb5 Mon Sep 17 00:00:00 2001 From: Warren Craft <41027033+wdcraft01@users.noreply.github.com> Date: Thu, 22 Aug 2024 07:19:53 -0600 Subject: [PATCH 28/29] physics/quantum/algebra: update no_cloning theorem 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. --- .../no_cloning_alt/allowed_presumptions.txt | 0 .../disallowed_presumptions.txt | 0 .../proofs/no_cloning_alt/thm_proof.ipynb | 123 ++++++++++++++++++ .../algebra/_theory_nbs_/theorems.ipynb | 41 +++++- 4 files changed, 157 insertions(+), 7 deletions(-) create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/allowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/disallowed_presumptions.txt create mode 100644 packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/thm_proof.ipynb diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/allowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/allowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/disallowed_presumptions.txt new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/thm_proof.ipynb new file mode 100644 index 000000000000..6820c7efba01 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/thm_proof.ipynb @@ -0,0 +1,123 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.physics.quantum.algebra.no_cloning_alt theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "from proveit import defaults\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving no_cloning_alt" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions = no_cloning_alt.all_conditions()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "hypo1 = no_cloning_alt.instance_expr.instance_expr.antecedent" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions += [hypo1]\n", + "defaults.assumptions" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions += no_cloning_alt.instance_expr.instance_expr.consequent.all_conditions()\n", + "defaults.assumptions" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "conseq1 = no_cloning_alt.instance_expr.instance_expr.consequent.instance_expr" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions += [conseq1.antecedent]\n", + "defaults.assumptions" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "conseq2 = conseq1.consequent" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Since $U$ is unitary, $U$ should preserve inner products and we should have $\\Big(U(a \\otimes b), U(c \\otimes b)\\Big) = \\Big(a \\otimes b, c \\otimes b\\Big)$.
\n", + "The LHS of that equation simplifies as follows: $\\Big(U(a \\otimes b), U(c \\otimes b)\\Big) = \\Big(a \\otimes a, c \\otimes c\\Big) = (\\bra{a}\\ket{c})^{2}$.
\n", + "The RHS of that equation simplifies as follows $\\Big(a \\otimes b, c \\otimes b\\Big) = \\Big(a \\otimes b, c \\otimes b\\Big) = \\bra{a}\\ket{c}$." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb index f797f4a41ddb..07e6280ae733 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/theorems.ipynb @@ -20,12 +20,12 @@ "\n", "from proveit import (Function, Lambda, Conditional, Composition,\n", " ExprTuple, ExprRange, IndexedVar)\n", - "from proveit import (a, b, c, f, i, j, k, l, m, n, x, A, B, D,K,M, P, Q, U, V, W, X, Y,\n", + "from proveit import (a, b, c, f, i, j, k, l, m, n, x, A, B, D, K, M, P, Q, U, V, W, X, Y,\n", " alpha)\n", "from proveit.core_expr_types import (A_i,V_i,W_i,\n", - " a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, b_1_to_j,v_1_to_n, \n", - " x_i, x_1_to_n, v_i, v_j, w_i, w_j, v_1_to_n, v_1_to_m, w_1_to_n, \n", - " A_1_to_l,A_1_to_n, A_1_to_m, B_1_to_i, B_1_to_j, B_1_to_m, C_1_to_n,V_1_to_n, W_1_to_n, lambda_i)\n", + " a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, b_1_to_j,v_1_to_n, x_i, x_1_to_n,\n", + " v_i, v_j, w_i, w_j, v_1_to_n, v_1_to_m, w_1_to_n, A_1_to_l,A_1_to_n,\n", + " A_1_to_m, B_1_to_i, B_1_to_j, B_1_to_m, C_1_to_n,V_1_to_n, W_1_to_n, lambda_i)\n", "from proveit.logic import (And, Implies, Iff, Or, Forall, Exists, Equals, NotEquals,\n", " Set, InSet, SubsetEq, InClass, CartExp, Functions,NotInSet,NotExists)\n", "from proveit.numbers import (zero, one, two,four, Natural, NaturalPos, \n", @@ -68,9 +68,36 @@ "metadata": {}, "outputs": [], "source": [ - "no_cloning=NotExists(U,Forall((a,b),Equals(Qmult(U,TensorProd(a,b)),TensorProd(a,a)),\n", - " domain=QubitSpace,conditions=(Equals(Norm(a),one),Equals(Norm(b),one))),\n", - " domain=Unitary(four))" + "no_cloning = (\n", + " NotExists((U, b),\n", + " Forall((a,b),\n", + " Equals(Qmult(U,TensorProd(a,b)),TensorProd(a,a)),\n", + " domain=QubitSpace,\n", + " conditions = [Equals(Norm(a),one)]),\n", + " domains = [Unitary(four), QubitSpace],\n", + " conditions = [Equals(Norm(b),one)])\n", + ")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "no_cloning_alt = (\n", + " Forall(U,\n", + " Forall((a,b),\n", + " Implies(Equals(Qmult(U, TensorProd(a, b)), TensorProd(a, a)),\n", + " Forall(c,\n", + " Implies(Equals(Qmult(U, TensorProd(c, b)), TensorProd(c, c)),\n", + " Equals(InnerProd(a, c), zero)),\n", + " domain = QubitSpace,\n", + " conditions=[NotEquals(c, a), Equals(Norm(c),one)])).with_wrap_after_operator(),\n", + " domain = QubitSpace,\n", + " conditions=[Equals(Norm(a),one),Equals(Norm(b),one)]),\n", + " domain=Unitary(four))\n", + ")" ] }, { From e9f1a00b0ed840ace23838ff64bc89d6da8f8d28 Mon Sep 17 00:00:00 2001 From: Sudhindu Bikash Mandal <33581066+sudhindu@users.noreply.github.com> Date: Fri, 20 Dec 2024 10:10:26 +0530 Subject: [PATCH 29/29] commit --- .../algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb index 17dbe40a0b54..ffbb9cd1251b 100644 --- a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning/thm_proof.ipynb @@ -37,7 +37,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }