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.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,
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,
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):

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(
QmultCodomain),
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]:

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