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/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/allowed_presumptions.txt b/packages/proveit/_core_/expression/composite/_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/_core_/expression/composite/_sub_theories_.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/disallowed_presumptions.txt b/packages/proveit/_core_/expression/conditional/_sub_theories_.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/disallowed_presumptions.txt rename to packages/proveit/_core_/expression/conditional/_sub_theories_.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/allowed_presumptions.txt b/packages/proveit/_core_/expression/label/_sub_theories_.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/_core_/expression/label/_sub_theories_.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/special_unitaries_are_matrices/disallowed_presumptions.txt b/packages/proveit/_core_/expression/lambda_expr/_sub_theories_.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/_core_/expression/lambda_expr/_sub_theories_.txt diff --git a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/allowed_presumptions.txt b/packages/proveit/_core_/expression/operation/_sub_theories_.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/allowed_presumptions.txt rename to packages/proveit/_core_/expression/operation/_sub_theories_.txt 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..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))))" ] }, { @@ -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_/demonstrations.ipynb b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb index 306537fbc558..c9b3bffebbf7 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,12 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit import defaults\n", + "from proveit.numbers import Complex, NaturalPos, Real\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, InClass, InSet\n", "%begin demonstrations" ] }, @@ -23,7 +29,200 @@ "execution_count": null, "metadata": {}, "outputs": [], - "source": [] + "source": [ + "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)]" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Testing the instantiation of some theorems underlying important `InnerProd` methods." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_field_membership.instantiate({H:V,x:v,y:w})" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "inner_prod_complex_membership.instantiate({H:H,x:x,y:y})" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Testing some `InnerProd` and `InnerProdSpaces` methods and related `VecSpaces` methods." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### Some new default assumptions:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "Cn_vec_space_claim = CartExp(Complex, n).deduce_as_vec_space()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from proveit.linear_algebra.vector_spaces import including_vec_space\n", + "Cn_including_vec_space = including_vec_space(CartExp(Complex, n), field=Complex)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "try:\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, + "metadata": {}, + "outputs": [], + "source": [ + "InnerProd(v, w)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "##### And we can deduce the inner product's membership in a specified field:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InnerProd(v, w).deduce_membership(Complex)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "InnerProd(x, y).deduce_membership(Real)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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}$:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "try:\n", + " InnerProd(v, x).deduce_membership(Real)\n", + "except Exception as the_exception:\n", + " print(f'Exception: {the_exception}')" + ] }, { "cell_type": "code", @@ -37,7 +236,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_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_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/matrices/_theory_nbs_/proofs/unitaries_are_matrices/disallowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/disallowed_presumptions.txt similarity index 100% rename from packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/unitaries_are_matrices/disallowed_presumptions.txt rename to 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/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..bf4208fed0a8 --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_complex_membership/thm_proof.ipynb @@ -0,0 +1,89 @@ +{ + "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", + "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" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving inner_prod_complex_membership" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "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 (ipykernel)", + "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/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/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/disallowed_presumptions.txt b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/disallowed_presumptions.txt similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/disallowed_presumptions.txt rename to 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/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..f59becde04f6 --- /dev/null +++ b/packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/inner_prod_field_membership/thm_proof.ipynb @@ -0,0 +1,95 @@ +{ + "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", + "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" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%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, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} 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" } 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..b8a6465a30df 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), domain=H),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), domain=H),condition=InClass(H,HilbertSpaces))" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -624,11 +646,18 @@ "source": [ "%end theorems" ] + }, + { + "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/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() 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 20861e5bfe14..33bcf43c1040 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,4 +64,56 @@ 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, 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 + from proveit.numbers import Complex + _x, _y = self.operands + 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( + 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 field set K. + ''' + from proveit.linear_algebra import InnerProdSpaces + _x, _y = self.operands + inner_prod_spaces = ( + InnerProdSpaces. + yield_readily_provable_inner_prod_spaces((_x, _y), field=K)) + fields = set() + for inner_prod_space in inner_prod_spaces: + # 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(_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 1fd23a21c65f..aa28663a4257 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,8 @@ 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 @@ -107,7 +109,40 @@ 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): + ''' + For the given list vec_or_vecs of vectors, yield the set of + 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, 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))): + yield space + else: + # we have a list of vectors + 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)): + 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) + for space in space_intersection: + yield space class InnerProdSpacesMembership(ClassMembership): def __init__(self, element, domain): @@ -179,16 +214,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/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 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..ca364a0476a0 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/linear_algebra/matrices/_theory_nbs_/demonstrations.ipynb @@ -15,15 +15,76 @@ "outputs": [], "source": [ "import proveit\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, + "metadata": {}, + "outputs": [], + "source": [ + "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": [] + "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", @@ -37,7 +98,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_/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/identity.py b/packages/proveit/linear_algebra/matrices/identity.py new file mode 100644 index 000000000000..57b26bf52531 --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/identity.py @@ -0,0 +1,34 @@ +from proveit import Function, Literal + +class Identity(Function): + ''' + 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__) + + def _config_latex_tool(self, lt): + if 'bbm' not in lt.packages: + lt.packages.append('bbm') + + def __init__(self, size, *, styles=None): + ''' + 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) + + 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) + '}') 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/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/allowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_sub_theories_.txt similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_in_QmultCodomain/allowed_presumptions.txt rename to packages/proveit/linear_algebra/matrices/transposition/_sub_theories_.txt diff --git a/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/allowed_presumptions.txt b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/__init__.py similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/allowed_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..5ed8297fa6eb --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/demonstrations.ipynb @@ -0,0 +1,101 @@ +{ + "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\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": [ + "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:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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:" + ] + }, + { + "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": [ + "%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/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb new file mode 100644 index 000000000000..4a774ec7ee3e --- /dev/null +++ b/packages/proveit/linear_algebra/matrices/transposition/_theory_nbs_/proofs/unitary_dag_unitary/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.linear_algebra.matrices.transposition.unitary_dag_unitary 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_dag_unitary" + ] + }, + { + "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/completeness_relation/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/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/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/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/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/physics/quantum/algebra/_theory_nbs_/proofs/bra_is_linmap/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 95% rename from packages/proveit/linear_algebra/matrices/unitary_group.py rename to packages/proveit/linear_algebra/matrices/transposition/unitary_group.py index d3ca6b256cd2..cc5631242fb2 100644 --- a/packages/proveit/linear_algebra/matrices/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 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/_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_/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..0a91f8dd9fcc 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,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", + " 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,230 @@ " 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": [ + "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": [ + "CartExp(Complex, n)" + ] + }, + { + "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": [ + "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}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra.instantiate({Hspace:H,varphi:varphi}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_as_map.instantiate({Hspace:H,varphi:varphi}, assumptions = defaults.assumptions + [InSet(ket_varphi, H)])" + ] + }, + { + "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, + "metadata": {}, + "outputs": [], + "source": [ + "qmult_of_bra_as_map.instantiate({Hspace:CartExp(Complex, n),varphi:varphi})" + ] + }, { "cell_type": "code", "execution_count": null, @@ -269,7 +533,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 +590,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 +621,15 @@ "qmult1" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "defaults.assumptions" + ] + }, { "cell_type": "code", "execution_count": null, @@ -683,6 +996,13 @@ "qmult4.simplification()" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -691,11 +1011,18 @@ "source": [ "%end demonstrations" ] + }, + { + "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/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/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/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/completeness_relation/disallowed_presumptions.txt b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/disallowed_presumptions.txt similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/completeness_relation/disallowed_presumptions.txt rename to packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/disallowed_presumptions.txt 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..4b3e06c82fb2 --- /dev/null +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/ket_self_projection/thm_proof.ipynb @@ -0,0 +1,181 @@ +{ + "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\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" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving ket_self_projection" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "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.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)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "norm_def_inst.square_both_sides()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%qed" + ] + } + ], + "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_/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/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..ffbb9cd1251b --- /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 (ipykernel)", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} 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/no_cloning_alt/allowed_presumptions.txt similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/allowed_presumptions.txt rename to packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/allowed_presumptions.txt 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/no_cloning_alt/disallowed_presumptions.txt similarity index 100% rename from packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/complex_in_QmultCodomain/disallowed_presumptions.txt rename to packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/no_cloning_alt/disallowed_presumptions.txt 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_/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_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_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..324df620d479 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,8 @@ "outputs": [], "source": [ "import proveit\n", + "from proveit.physics.quantum.algebra import bra_def\n", + "\n", "theory = proveit.Theory() # the theorem's theory" ] }, @@ -27,6 +29,84 @@ "%proving qmult_of_bra_as_map" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ +<<<<<<< HEAD + "#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": [ +======= +>>>>>>> hos_branch_remote/313-hoss_quantum_algebra_development + "bra_def" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ +<<<<<<< HEAD + "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": [ +======= +>>>>>>> hos_branch_remote/313-hoss_quantum_algebra_development + "%qed" + ] + }, { "cell_type": "code", "execution_count": null, @@ -37,7 +117,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/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/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/thm_proof.ipynb b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/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/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/thm_proof.ipynb index 34baa25c4233..32b46da61ee7 100644 --- a/packages/proveit/linear_algebra/matrices/_theory_nbs_/proofs/eigen_pow/thm_proof.ipynb +++ b/packages/proveit/physics/quantum/algebra/_theory_nbs_/proofs/qmult_of_linear_maps/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.physics.quantum.algebra.qmult_of_linear_maps theorem\n", "========" ] }, @@ -24,7 +24,7 @@ "metadata": {}, "outputs": [], "source": [ - "%proving eigen_pow" + "%proving qmult_of_linear_maps" ] }, { 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..07e6280ae733 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", - " 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", + "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, 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)\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,44 @@ "### Completeness relation and properties of orthogonal projectors" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "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", + ")" + ] + }, { "cell_type": "code", "execution_count": null, @@ -893,6 +932,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 +1204,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 +1400,13 @@ " domain=NaturalPos)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + }, { "cell_type": "code", "execution_count": null, @@ -1334,7 +1426,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" } diff --git a/packages/proveit/physics/quantum/algebra/qmult.py b/packages/proveit/physics/quantum/algebra/qmult.py index 3e7097b8a017..14562034105e 100644 --- a/packages/proveit/physics/quantum/algebra/qmult.py +++ b/packages/proveit/physics/quantum/algebra/qmult.py @@ -155,17 +155,78 @@ 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 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}) + #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 @@ -190,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,