# 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, D, M, P, Q, U, V, W, X, Y,
alpha)
from proveit.core_expr_types import (
a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, b_1_to_j,
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,
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)
from proveit.logic import (And, Implies, Iff, Or, Forall, Exists, Equals, NotEquals,
Set, InSet, SubsetEq, InClass, CartExp, Functions)
from proveit.numbers import (zero, one, two, Natural, NaturalPos,
RealNonNeg, Complex, Interval, Min, KroneckerDelta)
from proveit.numbers import Add, subtract, Mult, Exp, sqrd, sqrt
from proveit.linear_algebra import (
VecSpaces, HilbertSpaces, Hspace, VecZero, LinMap, Commutator,
MatrixSpace, MatrixMult, Unitary, Diagonal, ScalarMult, TensorProd, Identity,
from proveit.physics.quantum import (
Qmult, Bra, Ket, NumBra, NumKet, ket0, ket1, bra0, bra1, m_ket_domain,
psi, varphi, ket_psi, ket_varphi, bra_varphi,
var_ket_psi, var_ket_varphi, var_ket_v, QubitSpace, QubitRegisterSpace)
from proveit.physics.quantum.algebra import (
QmultCodomain, n_bit_interval, a_1_to_m_kets, b_1_to_n_kets,
v_1_to_m_kets, v_1_to_n_kets, w_1_to_n_kets, x_1_to_n_kets)

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


### Completeness relation and properties of orthogonal projectors¶

In [3]:
completeness_relation = Forall(
Hspace, Forall(n, Forall(x_1_to_n,
Equals(VecSum(i, Qmult(Ket(x_i), Bra(x_i)),
domain=Interval(one, n)),
Identity(Hspace)),
condition=InSet(x_1_to_n_kets, OrthoNormBases(Hspace))).with_wrapping(),
domain=NaturalPos),
domain=HilbertSpaces)

completeness_relation (conjecture without proof):

In [4]:
ortho_projector_from_completion = Forall(
Hspace, Forall(
X, Forall(
n, Forall(x_1_to_n,
Equals(OrthoProj(Hspace, X),
VecSum(i, Qmult(Ket(x_i), Bra(x_i)),
domain=Interval(one, n))),
condition=InSet(x_1_to_n_kets, OrthoNormBases(X))).with_wrapping(),
domain=NaturalPos),
condition=SubsetEq(X, Hspace)),
domain=HilbertSpaces)

ortho_projector_from_completion (conjecture without proof):

In [5]:
 Forall(
Hspace, Forall(
X, Forall(
n, Forall(x_1_to_n,
Equals(OrthoProj(Hspace, X),
VecSum(i, Qmult(Ket(x_i), Bra(x_i)),
domain=Interval(one, n))),
condition=InSet(x_1_to_n_kets, OrthoNormBases(Hspace))).with_wrapping(),
domain=NaturalPos),
condition=SubsetEq(X, Hspace)),
domain=HilbertSpaces)

Out[5]:

### Outer product representations and spectral decomposition¶

In [6]:
# Represent a linear operator in an outer product representation
output_prod_operator_repr = Forall(
(V, W), Forall(
A, Forall(
(m, n), Forall(
v_1_to_m, Forall(
w_1_to_n,
Equals(A, VecSum(i, VecSum(j, Qmult(Bra(w_j), A, Ket(v_i), Ket(w_j), Bra(v_i)),
domain=Interval(one, n)),
domain=Interval(one, m))),
condition=InSet(w_1_to_n_kets, OrthoNormBases(W))).with_wrapping(),
condition=InSet(v_1_to_m_kets, OrthoNormBases(V))).with_wrapping(),
domain=NaturalPos),
domain=LinMap(V, W)),
domain=HilbertSpaces)

output_prod_operator_repr (conjecture without proof):

In [7]:
spectral_decomposition_as_outer_prods = Forall(
n, Forall(
Hspace, Forall(
M,
Exists(
v_1_to_n, Exists(
a_1_to_n,
Equals(M, VecSum(i, ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
domain=Complex).with_wrapping(),
condition=InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping())
.with_wrap_after_operator(),
domain=LinMap(Hspace, Hspace)),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)

spectral_decomposition_as_outer_prods (conjecture without proof):

In [8]:
matrix_spectral_decomposition_as_outer_prods = Forall(
n, Forall(
M,
Exists(
v_1_to_n, Exists(
a_1_to_n,
Equals(M, VecSum(i, ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
domain=Complex).with_wrapping(),
condition=InSet(Set(v_1_to_n_kets),
OrthoNormBases(CartExp(Complex, n)))).with_wrapping())
.with_wrap_after_operator(),
domain=MatrixSpace(Complex, n, n)),
domain=NaturalPos)

matrix_spectral_decomposition_as_outer_prods (conjecture without proof):

#### Simultaneous diagonalization¶

In [9]:
simultaneous_diagonalization_as_outer_prods = Forall(
n, Forall(
Hspace, Forall(
(A, B),
Iff(Equals(Commutator(A, B), VecZero(LinMap(Hspace, Hspace))),
Exists(
v_1_to_n, Exists(
(a_1_to_n, b_1_to_n),
And(Equals(A, VecSum(i, ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
Equals(B, VecSum(i, ScalarMult(b_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n)))).with_wrap_after_operator(),
domain=Complex).with_wrapping(),
condition=InSet(Set(v_1_to_n), OrthoNormBases(Hspace))).with_wrapping())
.with_wrap_after_operator(),
domain=LinMap(Hspace, Hspace),
).with_wrapping(),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)

simultaneous_diagonalization_as_outer_prods (conjecture without proof):

In [10]:
matrix_simultaneous_diagonalization_as_outer_prods = Forall(
n, Forall(
(A, B),
Iff(Equals(Commutator(A, B), VecZero(MatrixSpace(Complex, n, n))),
Exists(
v_1_to_n, Exists(
(a_1_to_n, b_1_to_n),
And(Equals(A, VecSum(i, ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
Equals(B, VecSum(i, ScalarMult(b_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n)))).with_wrap_after_operator(),
domain=Complex).with_wrapping(),
condition=InSet(Set(v_1_to_n),
OrthoNormBases(CartExp(Complex, n)))).with_wrapping())
.with_wrap_after_operator(),
domain=MatrixSpace(Complex, n, n),
domain=NaturalPos)


#### Applying a function on a normal operator (derives from a more general linear algebra result)¶

In [11]:
operator_function = Forall(
n, Forall(
Hspace, Forall(
v_1_to_n, Forall(
a_1_to_n, Forall(
f, Equals(
Function(f, VecSum(i, ScalarMult(a_i, Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
VecSum(i, ScalarMult(Function(f, a_i),
Qmult(Ket(v_i), Bra(v_i))),
domain=Interval(one, n))),
domain=Functions(Complex, Complex)),
domain=Complex),
condition=InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping(),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)

operator_function (conjecture without proof):

#### Unitary matrices in outer product form¶

In [12]:
unitary_matrices_transform_ortho_norm_bases = Forall(
n, Forall(
U,
Exists(
(v_1_to_n, w_1_to_n),
Equals(U, VecSum(i, Qmult(Ket(v_i), Bra(w_i)), domain=Interval(one, n))),
conditions=[InSet(Set(v_1_to_n_kets),
OrthoNormBases(CartExp(Complex, n))),
InSet(Set(w_1_to_n_kets),
OrthoNormBases(CartExp(Complex, n)))]).with_wrapping(),
domain=Unitary(n)),
domain=NaturalPos)

unitary_matrices_transform_ortho_norm_bases (conjecture without proof):

In [13]:
ortho_norm_bases_form_unitary_matrix = Forall(
n, Forall(
(v_1_to_n, w_1_to_n),
InSet(VecSum(i, Qmult(Ket(v_i), Bra(w_i)), domain=Interval(one, n)), Unitary(n)),
conditions=[InSet(Set(v_1_to_n_kets), OrthoNormBases(CartExp(Complex, n))),
InSet(Set(w_1_to_n_kets), OrthoNormBases(CartExp(Complex, n)))]).with_wrapping(),
domain=NaturalPos)

ortho_norm_bases_form_unitary_matrix (conjecture without proof):

In [14]:
unitarity_by_ortho_norm_bases_elements = Forall(
n, Forall(
U, Forall(
v_1_to_n,
Implies(
Forall((i, j), Equals(Qmult(Bra(v_i), Adj(U), U, Ket(v_j)), KroneckerDelta(i, j)),
domain=Interval(one, n)),
InSet(U, Unitary(n))),
condition=InSet(Set(v_1_to_n_kets), OrthoNormBases(CartExp(Complex, n)))).with_wrapping(),
domain=MatrixSpace(Complex, n, n)),
domain=NaturalPos)

unitarity_by_ortho_norm_bases_elements (conjecture without proof):

#### Polar and singular-value decompositions¶

In [15]:
matrix_left_polar_decomposition = Forall(
n, Forall(
A,
Exists(
U,
domain=Unitary(n)),
domain=MatrixSpace(Complex, n, n)
),
domain=NaturalPos)

matrix_left_polar_decomposition (conjecture without proof):

In [16]:
matrix_right_polar_decomposition = Forall(
n, Forall(
A,
Exists(
U,
domain=Unitary(n)),
domain=MatrixSpace(Complex, n, n)
),
domain=NaturalPos)

matrix_right_polar_decomposition (conjecture without proof):

In [17]:
matrix_singular_value_decomposition = Forall(
n, Forall(
A,
Exists(
D, Exists(
(U, V),
Equals(A, Qmult(U, D, V)),
domain=Unitary(n)),
domain=Diagonal(n)),
domain=MatrixSpace(Complex, n, n)
),
domain=NaturalPos)

matrix_singular_value_decomposition (conjecture without proof):

In [18]:
schmidt_decomposition = Forall(
(m, n), Forall(
var_ket_psi,
Exists(
a_1_to_m, Exists(
b_1_to_n, Exists(
ExprRange(i, lambda_i, one, Min(m, n)),
Equals(var_ket_psi,
VecSum(i, ScalarMult(lambda_i, Qmult(Ket(a_i), Ket(b_i))),
domain=Interval(one, Min(m, n)))),
domain=RealNonNeg).with_wrapping(),
condition=InSet(Set(b_1_to_n_kets),
OrthoNormBases(CartExp(Complex, n)))).with_wrapping(),
condition=InSet(Set(a_1_to_m_kets),
OrthoNormBases(CartExp(Complex, m)))).with_wrapping(),
domain=TensorProd(CartExp(Complex, m), CartExp(Complex, n))).with_wrapping(),
domain=NaturalPos)

schmidt_decomposition (conjecture without proof):

### Basis ket membership and reductions¶

In [19]:
ket_zero_in_qubit_space = InSet(ket0, QubitSpace)

ket_zero_in_qubit_space (conjecture without proof):

In [20]:
ket_one_in_qubit_space = InSet(ket1, QubitSpace)

ket_one_in_qubit_space (conjecture without proof):

In [21]:
ket_zero_norm = Equals(Norm(ket0), one)

ket_zero_norm (conjecture without proof):

In [22]:
ket_one_norm = Equals(Norm(ket1), one)

ket_one_norm (conjecture without proof):

In [23]:
ket_zero_and_one_are_orthogonal = Equals(Qmult(bra0, ket1), zero)

ket_zero_and_one_are_orthogonal (conjecture without proof):

In [24]:
# We should have this automatically derived from the above,
# but let's just use this for now.
ket_zero_and_one_have_zero_inner_prod = Equals(InnerProd(ket0, ket1), zero)

ket_zero_and_one_have_zero_inner_prod (conjecture without proof):

In [25]:
single_qubit_num_ket = Forall(
b, Equals(NumKet(b, one), Ket(b)),
domain=Natural)

single_qubit_num_ket (conjecture without proof):

In [26]:
num_ket0 = Equals(NumKet(zero, one), ket0)

num_ket0 (conjecture without proof):

In [27]:
num_ket1 = Equals(NumKet(one, one), ket1)

num_ket1 (conjecture without proof):

In [28]:
num_ket_in_register_space = Forall(
n,
Forall(k,
InSet(NumKet(k, n), CartExp(Complex, Exp(two, n))),
domain=n_bit_interval),
domain=NaturalPos)

num_ket_in_register_space (conjecture without proof):

In [29]:
num_ket_norm = Forall(n, Forall(k, Equals(Norm(NumKet(k, n)), one),
domain=n_bit_interval),
domain=NaturalPos)

num_ket_norm (conjecture without proof):

In [30]:
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)

num_bra_is_lin_map (conjecture without proof):

### NumKet theorems¶

In [31]:
prepend_num_ket_with_zero_ket = Forall(
n,
Forall(k,
TensorProd(ket0, NumKet(k, n))),
domain=n_bit_interval),
domain=NaturalPos)

prepend_num_ket_with_zero_ket (conjecture without proof):

In [32]:
prepend_num_ket_with_one_ket = Forall(
n,
TensorProd(ket1, NumKet(k, n))),
domain=n_bit_interval),
domain=NaturalPos)

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 [33]:
# We don't need the domain because substitution is possible
# in any operation.
num_ket_eq = Forall(
n, Forall((j, k), Equals(NumKet(j, n), NumKet(k, n)),
condition=Equals(j, k)))

num_ket_eq (established theorem):

In [34]:
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)

num_ket_neq (conjecture without proof):

### Qmult Associativity¶

In [35]:
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))

qmult_association (conjecture without proof):

In [36]:
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))

qmult_disassociation (conjecture without proof):

In [37]:
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))

scalar_mult_absorption (conjecture without proof):

### Complex number commutivity and associativity¶

In [38]:
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)

qmult_pulling_scalar_out_front (conjecture without proof):

In [39]:
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)

qmult_pulling_scalars_out_front (conjecture without proof):

In [40]:
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))

qmult_scalar_association (conjecture without proof):

In [41]:
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)

scalar_mult_factorization (conjecture without proof):

### Qmult Distributivity¶

In [42]:
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))


In [43]:
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))

qmult_distribution_over_summation (conjecture without proof):

### Unary Qmult¶

In [44]:
qmult_of_complex = Forall(c, Equals(Qmult(c), c),
domain=Complex)

qmult_of_complex (conjecture without proof):

In [45]:
qmult_of_bra = Forall(
Hspace, Forall(varphi, Equals(Qmult(Bra(varphi)), Bra(varphi)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)

qmult_of_bra (conjecture without proof):

### Qmult as a linear map¶

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

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

qmult_of_bra_as_map (conjecture without proof):

### QmultCodomain closure-like theorems¶

In [47]:
complex_in_QmultCodomain = Forall(c, InClass(c, QmultCodomain), domain=Complex)

complex_in_QmultCodomain (conjecture without proof):

In [48]:
ket_in_QmultCodomain = Forall(
Hspace, Forall(var_ket_psi, InClass(var_ket_psi, QmultCodomain), domain=Hspace),
domain=HilbertSpaces)

ket_in_QmultCodomain (conjecture without proof):

In [49]:
bra_is_linmap = Forall(
Hspace, Forall(varphi, InSet(Bra(varphi),
LinMap(Hspace, Complex)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)

bra_is_linmap (conjecture without proof):

In [50]:
bra_in_QmultCodomain = Forall(
Hspace, Forall(varphi, InClass(Bra(varphi), QmultCodomain),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)

bra_in_QmultCodomain (conjecture without proof):

In [51]:
op_in_QmultCodomain = Forall(
(Hspace, X), Forall(A, InClass(A, QmultCodomain),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)

op_in_QmultCodomain (conjecture without proof):

In [52]:
qmult_complex_in_QmultCodomain = Forall(
c, InClass(Qmult(c), QmultCodomain),
domain=Complex)

qmult_complex_in_QmultCodomain (conjecture without proof):

In [53]:
qmult_ket_is_ket = Forall(
Hspace, Forall(var_ket_psi, InSet(Qmult(var_ket_psi),
Hspace),
domain=Hspace),
domain=HilbertSpaces)

qmult_ket_is_ket (conjecture without proof):

In [54]:
qmult_ket_in_QmultCodomain = Forall(
Hspace, Forall(var_ket_psi, InClass(Qmult(var_ket_psi),
QmultCodomain),
domain=Hspace),
domain=HilbertSpaces)

qmult_ket_in_QmultCodomain (conjecture without proof):

In [55]:
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)

qmult_matrix_is_linmap (conjecture without proof):

In [56]:
qmult_matrix_in_QmultCodomain = Forall(
(m, n), Forall(M, InClass(Qmult(M), QmultCodomain),
domain=MatrixSpace(Complex, m, n)),
domain=NaturalPos)

qmult_matrix_in_QmultCodomain (conjecture without proof):

In [57]:
qmult_bra_is_linmap = Forall(
Hspace, Forall(varphi, InSet(Qmult(Bra(varphi)),
LinMap(Hspace, Complex)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)

qmult_bra_is_linmap (conjecture without proof):

In [58]:
qmult_bra_in_QmultCodomain = Forall(
Hspace, Forall(varphi, InClass(Qmult(Bra(varphi)),
QmultCodomain),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)

qmult_bra_in_QmultCodomain (conjecture without proof):

In [59]:
qmult_op_is_linmap = Forall(
(Hspace, X), Forall(A, InSet(Qmult(A), LinMap(Hspace, X)),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)

qmult_op_is_linmap (conjecture without proof):

In [60]:
qmult_op_in_QmultCodomain = Forall(
(Hspace, X), Forall(A, InClass(Qmult(A), QmultCodomain),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)

qmult_op_in_QmultCodomain (conjecture without proof):

In [61]:
qmult_nested_closure = Forall(
A, InClass(Qmult(A), QmultCodomain),
domain=QmultCodomain)

qmult_nested_closure (conjecture without proof):

In [62]:
qmult_ket_ket_is_ket = Forall(
(A, B), Forall(
(var_ket_psi, var_ket_varphi),
InSet(Qmult(var_ket_psi, var_ket_varphi),
TensorProd(A, B)),
domains=(A, B)),
domain=HilbertSpaces)

qmult_ket_ket_is_ket (conjecture without proof):

In [63]:
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)

qmult_op_ket_is_ket (conjecture without proof):

In [64]:
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)

qmult_op_ket_in_QmultCodomain (conjecture without proof):

In [65]:
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)

qmult_op_op_is_op (conjecture without proof):

In [66]:
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)

qmult_op_op_in_QmultCodomain (conjecture without proof):

In [67]:
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))

qmult_ket_bra_is_op (conjecture without proof):

In [68]:
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))

qmult_ket_bra_in_QmultCodomain (conjecture without proof):

In [69]:
qmult_complex_complex_closure = Forall(
(a, b), InSet(Qmult(a, b), Complex),
domain=Complex)

qmult_complex_complex_closure (conjecture without proof):

In [70]:
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)

qmult_complex_ket_closure (conjecture without proof):

In [71]:
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)

qmult_ket_complex_closure (conjecture without proof):

In [72]:
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)

qmult_complex_op_closure (conjecture without proof):

In [73]:
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)

qmult_op_complex_closure (conjecture without proof):

In [74]:
qmult_complex_left_closure = Forall(
c, Forall(A, InClass(Qmult(c, A), QmultCodomain),
condition=InClass(Qmult(A), QmultCodomain)),
domain=Complex)

qmult_complex_left_closure (conjecture without proof):

In [75]:
qmult_complex_right_closure = Forall(
c, Forall(A, InClass(Qmult(A, c), QmultCodomain),
condition=InClass(Qmult(A), QmultCodomain)),
domain=Complex)

qmult_complex_right_closure (conjecture without proof):

### Unitary transformations¶

In [76]:
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)

state_space_preservation (conjecture without proof):

In [77]:
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)

normalization_preservation (conjecture without proof):

In [78]:
%end theorems

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