logo

Theorems (or conjectures) for the theory of proveit.physics.quantum.algebra

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.

from proveit import (Function, Lambda, Conditional, Composition,
                     ExprTuple, ExprRange, IndexedVar)
from proveit import (a, b, c, f, i, j, k, l, m, n, x, A, B, M, Q, X, Y, U,
                     alpha)
from proveit.core_expr_types import (
    b_1_to_j, A_1_to_l, A_1_to_m, 
    B_1_to_i, B_1_to_j, B_1_to_m, C_1_to_n)
from proveit.linear_algebra import (
    VecSpaces, LinMap, MatrixSpace, MatrixMult, Unitary, ScalarMult,
    VecAdd, VecSum, InnerProd, InnerProdSpaces, Norm, TensorProd)
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
from proveit.logic import (Implies, Or, Forall, Exists, Equals, NotEquals,
                           Set, InSet, InClass, CartExp)
from proveit.numbers import (zero, one, two, Natural, NaturalPos, 
                             RealNonNeg, Complex, Interval)
from proveit.numbers import Add, subtract, Mult, Exp
from proveit.physics.quantum import (
    Qmult, Bra, Ket, NumBra, NumKet, ket0, ket1, m_ket_domain,
    psi, varphi, ket_psi, ket_varphi, bra_varphi, 
    var_ket_psi, var_ket_v, QubitSpace, QubitRegisterSpace)
from proveit.physics.quantum.algebra import (
    HilbertSpaces, Hspace, QmultCodomain, n_bit_interval)
In [2]:
%begin theorems

Defining theorems for theory 'proveit.physics.quantum.algebra'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

Basis ket membership and reductions

In [3]:
ket_zero_in_qubit_space = InSet(ket0, QubitSpace)
Out[3]:
ket_zero_in_qubit_space (conjecture without proof):
In [4]:
ket_one_in_qubit_space = InSet(ket1, QubitSpace)
Out[4]:
ket_one_in_qubit_space (conjecture without proof):
In [5]:
ket_zero_norm = Equals(Norm(ket0), one)
Out[5]:
ket_zero_norm (conjecture without proof):
In [6]:
ket_one_norm = Equals(Norm(ket1), one)
Out[6]:
ket_one_norm (conjecture without proof):
In [7]:
ket_zero_and_one_are_orthogonal = Equals(InnerProd(ket0, ket1), zero)
Out[7]:
ket_zero_and_one_are_orthogonal (conjecture without proof):
In [8]:
single_qubit_num_ket = Forall(
    b, Equals(NumKet(b, one), Ket(b)),
    domain=Natural)
Out[8]:
single_qubit_num_ket (conjecture without proof):
In [9]:
num_ket0 = Equals(NumKet(zero, one), ket0)
Out[9]:
num_ket0 (conjecture without proof):
In [10]:
num_ket1 = Equals(NumKet(one, one), ket1)
Out[10]:
num_ket1 (conjecture without proof):
In [11]:
num_ket_in_register_space = Forall(
    n,
    Forall(k,
           InSet(NumKet(k, n), CartExp(Complex, Exp(two, n))),
           domain=n_bit_interval),
    domain=NaturalPos)
Out[11]:
num_ket_in_register_space (conjecture without proof):
In [12]:
num_ket_norm = Forall(n, Forall(k, Equals(Norm(NumKet(k, n)), one),
                                domain=n_bit_interval),
                      domain=NaturalPos)
Out[12]:
num_ket_norm (conjecture without proof):
In [13]:
num_bra_is_lin_map = Forall(
    n,
    Forall(k,
           InSet(NumBra(k, n), 
                 LinMap(CartExp(Complex, Exp(two, n)),
                        Complex)),
           domain=n_bit_interval),
    domain=NaturalPos)
Out[13]:
num_bra_is_lin_map (conjecture without proof):

NumKet theorems

In [14]:
prepend_num_ket_with_zero_ket = Forall(
        n,
        Forall(k,
               Equals(NumKet(k, Add(n, one)),
                      TensorProd(ket0, NumKet(k, n))),
               domain=n_bit_interval),
        domain=NaturalPos)
Out[14]:
prepend_num_ket_with_zero_ket (conjecture without proof):
In [15]:
prepend_num_ket_with_one_ket = Forall(
        n, 
        Forall(k, Equals(NumKet(Add(Exp(two, n), k), Add(n, one)),
                         TensorProd(ket1, NumKet(k, n))),
               domain=n_bit_interval),
        domain=NaturalPos)
Out[15]:
prepend_num_ket_with_one_ket (conjecture without proof):

NumKets of the same dimension are equal if and only if their contents are equal.

In [16]:
num_ket_eq = Forall(
    n, Forall((j, k), Equals(NumKet(j, n), NumKet(k, n)),
              domain=n_bit_interval, condition=Equals(j, k)),
    domain=NaturalPos)
Out[16]:
num_ket_eq (conjecture without proof):
In [17]:
num_ket_neq = Forall(
    n, Forall((j, k), NotEquals(NumKet(j, n), NumKet(k, n)),
              domain=n_bit_interval, condition=NotEquals(j, k)),
    domain=NaturalPos)
Out[17]:
num_ket_neq (conjecture without proof):

Theorems about Hilbert spaces

Complex vectors form Hilbert spaces

In [18]:
complex_vec_set_is_hilbert_space = Forall(
    n, InClass(CartExp(Complex, n), HilbertSpaces),
    domain=NaturalPos)
Out[18]:
complex_vec_set_is_hilbert_space (conjecture without proof):

As a special case, the complex number set is also a Hilbert space:

In [19]:
complex_set_is_hilbert_space = InClass(Complex, HilbertSpaces)
Out[19]:
complex_set_is_hilbert_space (conjecture without proof):

Hilbert spaces are inner product spaces and vector spaces

In [20]:
hilbert_space_is_inner_prod_space = Forall(
    Hspace, InClass(Hspace, InnerProdSpaces(Complex)),
    domain=HilbertSpaces)
Out[20]:
hilbert_space_is_inner_prod_space (conjecture without proof):
In [21]:
hilbert_space_is_vec_space = Forall(
    Hspace, InClass(Hspace, VecSpaces(Complex)),
    domain=HilbertSpaces)
Out[21]:
hilbert_space_is_vec_space (conjecture without proof):

Qmult Associativity

In [22]:
qmult_association = Forall(
    (l,m,n), Forall(
        (A_1_to_l,B_1_to_m,C_1_to_n),
        Equals(Qmult(A_1_to_l, B_1_to_m, C_1_to_n),
               Qmult(A_1_to_l, Qmult(B_1_to_m), 
                     C_1_to_n)).with_wrapping_at(2),
        condition=InClass(Qmult(A_1_to_l, B_1_to_m,
                                C_1_to_n),
                          QmultCodomain)),
    domains=(Natural, NaturalPos, Natural))
Out[22]:
qmult_association (conjecture without proof):
In [23]:
qmult_disassociation = Forall(
    (l,m,n), Forall(
        (A_1_to_l,B_1_to_m,C_1_to_n),
        Equals(Qmult(A_1_to_l, Qmult(B_1_to_m), C_1_to_n),
               Qmult(A_1_to_l, B_1_to_m, C_1_to_n)
              ).with_wrapping_at(2),
        condition=InClass(Qmult(A_1_to_l, B_1_to_m,
                                      C_1_to_n),
                          QmultCodomain)),
    domains=(Natural, NaturalPos, Natural))
Out[23]:
qmult_disassociation (conjecture without proof):
In [24]:
scalar_mult_absorption = Forall(
    (alpha, l, n), Forall(
        (A_1_to_l,B,C_1_to_n),
        Equals(Qmult(A_1_to_l, ScalarMult(alpha, B), C_1_to_n),
               Qmult(A_1_to_l, alpha, B, C_1_to_n)
              ).with_wrapping_at(2),
        condition=InClass(Qmult(A_1_to_l, B, C_1_to_n),
                          QmultCodomain)),
    domains=(Complex, Natural, Natural))
Out[24]:
scalar_mult_absorption (conjecture without proof):

Complex number commutivity and associativity

In [25]:
qmult_pulling_scalar_out_front = Forall(
    (l,n), Forall(
        b, Forall(
            (A_1_to_l, C_1_to_n),
            Equals(Qmult(A_1_to_l, b, C_1_to_n),
                   Qmult(b, A_1_to_l, C_1_to_n)
              ).with_wrapping_at(2),
            condition=InClass(Qmult(A_1_to_l, C_1_to_n),
                              QmultCodomain)),
        domain=Complex),
    domain=Natural)
Out[25]:
qmult_pulling_scalar_out_front (conjecture without proof):
In [26]:
qmult_pulling_scalars_out_front = Forall(
    (j,l,n), Forall(
        b_1_to_j, Forall(
            (A_1_to_l, C_1_to_n),
            Equals(Qmult(A_1_to_l, b_1_to_j, C_1_to_n),
                   Qmult(b_1_to_j, A_1_to_l, C_1_to_n)
              ).with_wrapping_at(2),
            condition=InClass(Qmult(A_1_to_l, C_1_to_n),
                              QmultCodomain)),
        domain=Complex),
    domain=Natural)
Out[26]:
qmult_pulling_scalars_out_front (conjecture without proof):
In [27]:
qmult_scalar_association = Forall(
    (j,l), Forall(
        b_1_to_j, Forall(
            A_1_to_l,
            Equals(Qmult(b_1_to_j, A_1_to_l),
                   Qmult(Mult(b_1_to_j), A_1_to_l)
              ).with_wrapping_at(2),
            condition=InClass(Qmult(A_1_to_l),
                              QmultCodomain)),
        domain=Complex),
    domains=(NaturalPos, Natural))
Out[27]:
qmult_scalar_association (conjecture without proof):
In [28]:
scalar_mult_factorization = Forall(
    j, Forall(
        a, Forall(
            B_1_to_j,
            Equals(Qmult(a, B_1_to_j),
                   ScalarMult(a, Qmult(B_1_to_j))
              ).with_wrapping_at(2),
            condition=InClass(Qmult(B_1_to_j),
                              QmultCodomain)),
        domain=Complex),
    domain=NaturalPos)
Out[28]:
scalar_mult_factorization (conjecture without proof):

Qmult Distributivity

In [29]:
qmult_distribution_over_add = Forall(
    (i, m, n), Forall(
        (A_1_to_m, B_1_to_i, C_1_to_n), 
        Implies(
            InClass(Qmult(A_1_to_m, VecAdd(B_1_to_i), C_1_to_n),
                          QmultCodomain),
            Equals(Qmult(A_1_to_m, VecAdd(B_1_to_i), C_1_to_n),
                   VecAdd(ExprRange(
                       k, Qmult(A_1_to_m, IndexedVar(B, k), 
                                C_1_to_n),
                       one, i))).with_wrap_after_operator())
        .with_wrap_after_operator()),
    domains=(NaturalPos, Natural, Natural))
Out[29]:
qmult_distribution_over_add (conjecture without proof):
In [30]:
qmult_distribution_over_summation = Forall(
    (j, m, n), Forall(
        (A_1_to_m, C_1_to_n, f, Q),
        Implies(InClass(Qmult(A_1_to_m, vec_summation_b1toj_fQ,
                              C_1_to_n),
                        QmultCodomain),
                Equals(Qmult(A_1_to_m, vec_summation_b1toj_fQ,
                             C_1_to_n),
                       VecSum(b_1_to_j,
                              Qmult(A_1_to_m, Function(f, b_1_to_j),
                                    C_1_to_n),
                              condition=Function(Q, b_1_to_j)))
                .with_wrap_before_operator())
        .with_wrap_after_operator()),
    domains=(NaturalPos, Natural, Natural))
Out[30]:
qmult_distribution_over_summation (conjecture without proof):

Unary Qmult

In [31]:
qmult_of_complex = Forall(c, Equals(Qmult(c), c),
                          domain=Complex)
Out[31]:
qmult_of_complex (conjecture without proof):
In [32]:
qmult_of_bra = Forall(
    Hspace, Forall(varphi, Equals(Qmult(Bra(varphi)), Bra(varphi)),
                   condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[32]:
qmult_of_bra (conjecture without proof):

Qmult as a linear map

In [33]:
qmult_of_bra_as_map = Forall(
    Hspace, Forall(
        varphi, Equals(
            Qmult(Bra(varphi)), 
            Lambda(var_ket_psi,
                   Conditional(InnerProd(ket_varphi, var_ket_psi),
                               InSet(var_ket_psi, Hspace)))),
        condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[33]:
qmult_of_bra_as_map (conjecture without proof):

QmultCodomain closure-like theorems

In [34]:
complex_in_QmultCodomain = Forall(c, InClass(c, QmultCodomain), domain=Complex)
Out[34]:
complex_in_QmultCodomain (conjecture without proof):
In [35]:
ket_in_QmultCodomain = Forall(
    Hspace, Forall(var_ket_psi, InClass(var_ket_psi, QmultCodomain), domain=Hspace),
    domain=HilbertSpaces)
Out[35]:
ket_in_QmultCodomain (conjecture without proof):
In [36]:
bra_is_linmap = Forall(
    Hspace, Forall(varphi, InSet(Bra(varphi),
                                 LinMap(Hspace, Complex)),
                   condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[36]:
bra_is_linmap (conjecture without proof):
In [37]:
bra_in_QmultCodomain = Forall(
    Hspace, Forall(varphi, InClass(Bra(varphi), QmultCodomain), 
                   condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[37]:
bra_in_QmultCodomain (conjecture without proof):
In [38]:
op_in_QmultCodomain = Forall(
    (Hspace, X), Forall(A, InClass(A, QmultCodomain), 
                       domain=LinMap(Hspace, X)),
    domain=HilbertSpaces)
Out[38]:
op_in_QmultCodomain (conjecture without proof):
In [39]:
qmult_complex_in_QmultCodomain = Forall(
    c, InClass(Qmult(c), QmultCodomain),
    domain=Complex)
Out[39]:
qmult_complex_in_QmultCodomain (conjecture without proof):
In [40]:
qmult_ket_is_ket = Forall(
    Hspace, Forall(var_ket_psi, InSet(Qmult(var_ket_psi),
                                      Hspace),
                   domain=Hspace),
    domain=HilbertSpaces)
Out[40]:
qmult_ket_is_ket (conjecture without proof):
In [41]:
qmult_ket_in_QmultCodomain = Forall(
    Hspace, Forall(var_ket_psi, InClass(Qmult(var_ket_psi), 
                                        QmultCodomain),
                   domain=Hspace),
    domain=HilbertSpaces)
Out[41]:
qmult_ket_in_QmultCodomain (conjecture without proof):
In [42]:
qmult_matrix_is_linmap = Forall(
    (m, n), Forall(M, InSet(Qmult(M), LinMap(CartExp(Complex, n),
                                             CartExp(Complex, m))),
                   domain=MatrixSpace(Complex, m, n)),
    domain=NaturalPos)
Out[42]:
qmult_matrix_is_linmap (conjecture without proof):
In [43]:
qmult_matrix_in_QmultCodomain = Forall(
    (m, n), Forall(M, InClass(Qmult(M), QmultCodomain),
                   domain=MatrixSpace(Complex, m, n)),
    domain=NaturalPos)
Out[43]:
qmult_matrix_in_QmultCodomain (conjecture without proof):
In [44]:
qmult_bra_is_linmap = Forall(
    Hspace, Forall(varphi, InSet(Qmult(Bra(varphi)),
                                 LinMap(Hspace, Complex)),
                   condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[44]:
qmult_bra_is_linmap (conjecture without proof):
In [45]:
qmult_bra_in_QmultCodomain = Forall(
    Hspace, Forall(varphi, InClass(Qmult(Bra(varphi)),
                                   QmultCodomain),
                   condition=InSet(Ket(varphi), Hspace)),
    domain=HilbertSpaces)
Out[45]:
qmult_bra_in_QmultCodomain (conjecture without proof):
In [46]:
qmult_op_is_linmap = Forall(
    (Hspace, X), Forall(A, InSet(Qmult(A), LinMap(Hspace, X)),
                        domain=LinMap(Hspace, X)),
    domain=HilbertSpaces)
Out[46]:
qmult_op_is_linmap (conjecture without proof):
In [47]:
qmult_op_in_QmultCodomain = Forall(
    (Hspace, X), Forall(A, InClass(Qmult(A), QmultCodomain),
                        domain=LinMap(Hspace, X)),
    domain=HilbertSpaces)
Out[47]:
qmult_op_in_QmultCodomain (conjecture without proof):
In [48]:
qmult_nested_closure = Forall(
    A, InClass(Qmult(A), QmultCodomain),
    domain=QmultCodomain)
Out[48]:
qmult_nested_closure (conjecture without proof):
In [49]:
qmult_op_ket_is_ket = Forall(
    (Hspace, X), Forall(
        A, Forall(var_ket_psi, InSet(Qmult(A, var_ket_psi), X),
                  domain=Hspace),
        condition=InSet(Qmult(A),
                        LinMap(Hspace, X))),
    domain=HilbertSpaces)
Out[49]:
qmult_op_ket_is_ket (conjecture without proof):
In [50]:
qmult_op_ket_in_QmultCodomain = Forall(
    (Hspace, X), Forall(
        A, Forall(var_ket_psi, InClass(Qmult(A, var_ket_psi),
                                       QmultCodomain),
                  domain=Hspace),
        condition=InSet(Qmult(A),
                        LinMap(Hspace, X))),
    domain=HilbertSpaces)
Out[50]:
qmult_op_ket_in_QmultCodomain (conjecture without proof):
In [51]:
qmult_op_op_is_op = Forall(
    (Hspace, X, Y), Forall(
        (A, B), InSet(Qmult(A, B), LinMap(Hspace, Y)),
        conditions=[InSet(Qmult(A), LinMap(X, Y)),
                    InSet(Qmult(B), LinMap(Hspace, X))]),
    domain=HilbertSpaces)
Out[51]:
qmult_op_op_is_op (conjecture without proof):
In [52]:
qmult_op_op_in_QmultCodomain = Forall(
    (Hspace, X, Y), Forall(
        (A, B), InClass(Qmult(A, B), QmultCodomain),
        conditions=[InSet(Qmult(A), LinMap(X, Y)),
                    InSet(Qmult(B), LinMap(Hspace, X))]),
    domain=HilbertSpaces)
Out[52]:
qmult_op_op_in_QmultCodomain (conjecture without proof):
In [53]:
qmult_ket_bra_is_op = Forall(
    (Hspace, X), Forall(
        var_ket_psi, Forall(
            varphi, InSet(Qmult(var_ket_psi, Bra(varphi)),
                          LinMap(X, Hspace)),
            condition=InSet(Ket(varphi), X)),
        domain=Hspace))
Out[53]:
qmult_ket_bra_is_op (conjecture without proof):
In [54]:
qmult_ket_bra_in_QmultCodomain = Forall(
    (Hspace, X), Forall(
        var_ket_psi, Forall(
            varphi, InClass(Qmult(var_ket_psi, Bra(varphi)),
                            QmultCodomain),
            condition=InSet(Ket(varphi), X)),
        domain=Hspace))
Out[54]:
qmult_ket_bra_in_QmultCodomain (conjecture without proof):
In [55]:
qmult_complex_complex_closure = Forall(
    (a, b), InSet(Qmult(a, b), Complex),
    domain=Complex)
Out[55]:
qmult_complex_complex_closure (conjecture without proof):
In [56]:
qmult_complex_ket_closure = Forall(
    c, Forall(Hspace, Forall(var_ket_psi, InSet(Qmult(c, var_ket_psi), Hspace),
                             domain=Hspace),
              domain=HilbertSpaces),
    domain=Complex)
Out[56]:
qmult_complex_ket_closure (conjecture without proof):
In [57]:
qmult_ket_complex_closure = Forall(
    c, Forall(Hspace, Forall(var_ket_psi, InSet(Qmult(var_ket_psi, c), Hspace),
                             domain=Hspace),
              domain=HilbertSpaces),
    domain=Complex)
Out[57]:
qmult_ket_complex_closure (conjecture without proof):
In [58]:
qmult_complex_op_closure = Forall(
    c, Forall(
        (Hspace, X), Forall(
            A, InSet(Qmult(c, A), LinMap(Hspace, X)),
            condition=InSet(Qmult(A), LinMap(Hspace, X))),
        domain=HilbertSpaces),
    domain=Complex)
Out[58]:
qmult_complex_op_closure (conjecture without proof):
In [59]:
qmult_op_complex_closure = Forall(
    c, Forall(
        (Hspace, X), Forall(
            A, InSet(Qmult(A, c), LinMap(Hspace, X)),
            condition=InSet(Qmult(A), LinMap(Hspace, X))),
        domain=HilbertSpaces),
    domain=Complex)
Out[59]:
qmult_op_complex_closure (conjecture without proof):
In [60]:
qmult_complex_left_closure = Forall(
    c, Forall(A, InClass(Qmult(c, A), QmultCodomain),
              condition=InClass(Qmult(A), QmultCodomain)),
    domain=Complex)
Out[60]:
qmult_complex_left_closure (conjecture without proof):
In [61]:
qmult_complex_right_closure = Forall(
    c, Forall(A, InClass(Qmult(A, c), QmultCodomain),
              condition=InClass(Qmult(A), QmultCodomain)),
    domain=Complex)
Out[61]:
qmult_complex_right_closure (conjecture without proof):

Unitary transformations

In [62]:
state_space_preservation = Forall(
    n, Forall(
        U, Forall(var_ket_psi,
                  InSet(Qmult(U, var_ket_psi), CartExp(Complex, n)),
                  domain=CartExp(Complex, n)),
        domain=Unitary(n)),
    domain=NaturalPos)
Out[62]:
state_space_preservation (conjecture without proof):
In [63]:
normalization_preservation = Forall(
    n,  Forall(
        U, Forall(
            alpha, Forall(
                var_ket_psi, Equals(Norm(Qmult(U, var_ket_psi)), alpha),
                domain=CartExp(Complex, n),
                condition=Equals(Norm(var_ket_psi), alpha)),
            domain=RealNonNeg),
        domain=Unitary(n)),
    domain=NaturalPos)
Out[63]:
normalization_preservation (conjecture without proof):
In [64]:
%end theorems

These theorems may now be imported from the theory package: proveit.physics.quantum.algebra