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,
VecAdd, VecSum, InnerProd, InnerProdSpaces, Norm, OrthoProj, Adj, OrthoNormBases, Dim)
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
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
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)
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)
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)
In [7]:
spectral_decomposition_as_outer_prods = Forall(
n, Forall(
Hspace, Forall(
M,
Iff(Equals(Qmult(Adj(M), M),
Qmult(M, Adj(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)
In [8]:
matrix_spectral_decomposition_as_outer_prods = Forall(
n, Forall(
M,
Iff(Equals(Qmult(Adj(M), M),
Qmult(M, Adj(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)
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),
conditions=[Equals(Adj(A), A), Equals(Adj(B), B)]
).with_wrapping(),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)
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),
conditions=[Equals(Adj(A), A), Equals(Adj(B), B)]).with_wrapping(),
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)
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)
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)
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)
Polar and singular-value decompositions¶
In [15]:
matrix_left_polar_decomposition = Forall(
n, Forall(
A,
Exists(
U,
Equals(A, Qmult(U, sqrt(Qmult(Adj(A), A)))),
domain=Unitary(n)),
domain=MatrixSpace(Complex, n, n)
),
domain=NaturalPos)
In [16]:
matrix_right_polar_decomposition = Forall(
n, Forall(
A,
Exists(
U,
Equals(A, Qmult(sqrt(Qmult(A, Adj(A))), U)),
domain=Unitary(n)),
domain=MatrixSpace(Complex, n, n)
),
domain=NaturalPos)
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)
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)
Basis ket membership and reductions¶
In [19]:
ket_zero_in_qubit_space = InSet(ket0, QubitSpace)
In [20]:
ket_one_in_qubit_space = InSet(ket1, QubitSpace)
In [21]:
ket_zero_norm = Equals(Norm(ket0), one)
In [22]:
ket_one_norm = Equals(Norm(ket1), one)
In [23]:
ket_zero_and_one_are_orthogonal = Equals(Qmult(bra0, ket1), zero)
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)
In [25]:
single_qubit_num_ket = Forall(
b, Equals(NumKet(b, one), Ket(b)),
domain=Natural)
In [26]:
num_ket0 = Equals(NumKet(zero, one), ket0)
In [27]:
num_ket1 = Equals(NumKet(one, one), ket1)
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)
In [29]:
num_ket_norm = Forall(n, Forall(k, Equals(Norm(NumKet(k, n)), one),
domain=n_bit_interval),
domain=NaturalPos)
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)
NumKet theorems¶
In [31]:
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)
In [32]:
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)
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)))
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)
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))
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))
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))
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)
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)
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))
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)
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(
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))
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))
Unary Qmult¶
In [44]:
qmult_of_complex = Forall(c, Equals(Qmult(c), c),
domain=Complex)
In [45]:
qmult_of_bra = Forall(
Hspace, Forall(varphi, Equals(Qmult(Bra(varphi)), Bra(varphi)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)
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)
QmultCodomain closure-like theorems¶
In [47]:
complex_in_QmultCodomain = Forall(c, InClass(c, QmultCodomain), domain=Complex)
In [48]:
ket_in_QmultCodomain = Forall(
Hspace, Forall(var_ket_psi, InClass(var_ket_psi, QmultCodomain), domain=Hspace),
domain=HilbertSpaces)
In [49]:
bra_is_linmap = Forall(
Hspace, Forall(varphi, InSet(Bra(varphi),
LinMap(Hspace, Complex)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)
In [50]:
bra_in_QmultCodomain = Forall(
Hspace, Forall(varphi, InClass(Bra(varphi), QmultCodomain),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)
In [51]:
op_in_QmultCodomain = Forall(
(Hspace, X), Forall(A, InClass(A, QmultCodomain),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)
In [52]:
qmult_complex_in_QmultCodomain = Forall(
c, InClass(Qmult(c), QmultCodomain),
domain=Complex)
In [53]:
qmult_ket_is_ket = Forall(
Hspace, Forall(var_ket_psi, InSet(Qmult(var_ket_psi),
Hspace),
domain=Hspace),
domain=HilbertSpaces)
In [54]:
qmult_ket_in_QmultCodomain = Forall(
Hspace, Forall(var_ket_psi, InClass(Qmult(var_ket_psi),
QmultCodomain),
domain=Hspace),
domain=HilbertSpaces)
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)
In [56]:
qmult_matrix_in_QmultCodomain = Forall(
(m, n), Forall(M, InClass(Qmult(M), QmultCodomain),
domain=MatrixSpace(Complex, m, n)),
domain=NaturalPos)
In [57]:
qmult_bra_is_linmap = Forall(
Hspace, Forall(varphi, InSet(Qmult(Bra(varphi)),
LinMap(Hspace, Complex)),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)
In [58]:
qmult_bra_in_QmultCodomain = Forall(
Hspace, Forall(varphi, InClass(Qmult(Bra(varphi)),
QmultCodomain),
condition=InSet(Ket(varphi), Hspace)),
domain=HilbertSpaces)
In [59]:
qmult_op_is_linmap = Forall(
(Hspace, X), Forall(A, InSet(Qmult(A), LinMap(Hspace, X)),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)
In [60]:
qmult_op_in_QmultCodomain = Forall(
(Hspace, X), Forall(A, InClass(Qmult(A), QmultCodomain),
domain=LinMap(Hspace, X)),
domain=HilbertSpaces)
In [61]:
qmult_nested_closure = Forall(
A, InClass(Qmult(A), QmultCodomain),
domain=QmultCodomain)
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)
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)
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)
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)
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)
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))
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))
In [69]:
qmult_complex_complex_closure = Forall(
(a, b), InSet(Qmult(a, b), Complex),
domain=Complex)
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)
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)
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)
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)
In [74]:
qmult_complex_left_closure = Forall(
c, Forall(A, InClass(Qmult(c, A), QmultCodomain),
condition=InClass(Qmult(A), QmultCodomain)),
domain=Complex)
In [75]:
qmult_complex_right_closure = Forall(
c, Forall(A, InClass(Qmult(A, c), QmultCodomain),
condition=InClass(Qmult(A), QmultCodomain)),
domain=Complex)
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)
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)
In [78]:
%end theorems