Common expressions for the theory of proveit.physics.quantum¶
In [1]:
import proveit
# Automation is not needed when building common expressions:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import IndexedVar, Lambda, Function
from proveit import a, b, c, d, k, l, m, n, u, x, y, A, B, C, D, P, Q, U, V
from proveit import Variable, Literal, ExprRange, ExprArray, ExprTuple
# from proveit.multi_expression import Block
from proveit.core_expr_types import A_1_to_m, b_1_to_j, n_k
from proveit.logic import Equals, Set, InSet, CartExp
from proveit.numbers import sqrt, Add, subtract, frac, Exp
from proveit.numbers import zero, one, two, three, Interval
from proveit.numbers import Complex
from proveit.linear_algebra import VecSum, LinMap, SU, TensorExp, Norm
from proveit.physics.quantum import Ket, Bra
In [2]:
%begin common
In [3]:
# For positive X eigenstate
PLUS = Literal(string_format='+', latex_format='+')
PLUS: 
In [4]:
# For negative X eigenstate
MINUS = Literal(string_format='-', latex_format='-')
MINUS: 
In [5]:
ket0, ket1, ket_plus, ket_minus = Ket(zero), Ket(one), Ket(PLUS), Ket(MINUS)
ket0: 
ket1: 
ket_plus: 
ket_minus: 
In [6]:
bra0, bra1, bra_plus, bra_minus = Bra(zero), Bra(one), Bra(PLUS), Bra(MINUS)
bra0: 
bra1: 
bra_plus: 
bra_minus: 
In [7]:
psi = Variable('psi', r'\psi')
psi: 
In [8]:
varphi = Variable('varphi', r'\varphi')
varphi: 
In [9]:
ket_psi = Ket(psi)
ket_psi: 
In [10]:
bra_psi = Bra(psi)
bra_psi: 
In [11]:
ket_varphi = Ket(varphi)
ket_varphi: 
In [12]:
bra_varphi = Bra(varphi)
bra_varphi: 
These Variable version of $\lvert \psi \rangle$ and $\lvert v \rangle$ are useful in theorems applicable to any ket where there is no reference to the complementary $\langle \psi \rvert$ or $\langle v \rvert$:
In [13]:
var_ket_psi = Variable('|psi>', r'\lvert \psi \rangle')
var_ket_psi:
In [14]:
var_ket_varphi = Variable('|varphi>', r'\lvert \varphi \rangle')
var_ket_varphi:
In [15]:
var_ket_v = Variable('|v>', r'\lvert v \rangle')
var_ket_v: 
In [16]:
var_ket_u = Variable('|u>', r'\lvert u \rangle')
var_ket_u: 
In [17]:
var_ket_utilde = Variable('|~u~>', r'\tilde{u}')
var_ket_utilde: 
In [18]:
l_ket_domain = CartExp(Complex, Exp(two, l))
l_ket_domain: 
In [19]:
m_ket_domain = CartExp(Complex, Exp(two, m))
m_ket_domain: 
In [20]:
nk_ket_domain = CartExp(Complex, Exp(two, n_k))
nk_ket_domain: 
In [21]:
normalized_var_ket_psi = Equals(Norm(var_ket_psi), one)
normalized_var_ket_psi: 
In [22]:
normalized_var_ket_u = Equals(Norm(var_ket_u), one)
normalized_var_ket_u: 
In [23]:
m_bit_interval = Interval(zero, subtract(Exp(two, m), one))
m_bit_interval: 
In [24]:
# Identity operation
I = Literal('I')
I: 
In [25]:
# Pauli's X, Y, Z
X, Y, Z = Literal('X'), Literal('Y'), Literal('Z')
X: 
Y: 
Z: 
In [26]:
# Hadamard
H = Literal('H')
H: 
In [27]:
# Measurement Gate
MEAS = Literal('MEAS')
MEAS: 
In [28]:
# Swap Gate - for use in a MultiQubitGate that connects to the second swap gate.
SWAP = Literal('SWAP')
SWAP: 
In [29]:
# SPACE: is used as a blank space holder in situations like classically controlled circuits
SPACE = Literal('SPACE')
SPACE: 
In [30]:
# WIRE: is used to explicitly denote a classical wire. The classical version of 'I'
WIRE = Literal('WIRE')
WIRE: 
In [ ]:
In [31]:
# CONTROL: indicates a controlled MultiQubitGate
CONTROL = Literal('CONTROL')
CONTROL: 
In [32]:
# CLASSICAL_CONTROL: indicates a classically controlled MultiQubitGate
CLASSICAL_CONTROL = Literal('CLASSICAL\_CONTROL')
CLASSICAL_CONTROL: 
In [33]:
# LEGACY
# CTRL_UP, CTRL_DN, CTRL_UPDN = (
# Literal('CTRL\_UP'),
# Literal('CTRL\_DN'),
# Literal('CTRL\_UPDN'))
In [34]:
# LEGACY
# # WIRE_UP: wire goes up to link with another wire
# # WIRE_DN: wire goes down to link with another wire
# # WIRE_LINK: link destination for WIRE_UP or WIRE_DN
# WIRE_UP, WIRE_DN, WIRE_LINK = (Literal('WIRE\_UP'),
# Literal('WIRE\_DN'),
# Literal('WIRE\_LINK'))
In [35]:
QubitSpace = CartExp(Complex, two)
QubitSpace: 
In [36]:
# These eventually moved to separate definitions inside the quantum/quantum_ops.py file
# QubitRegisterSpace = lambda n : TensorExp(Exp(Complex, two), n)
# RegisterSU = lambda n : SU(Exp(two, n))
In [37]:
inv_root2 = frac(one, sqrt(two))
inv_root2: 
In [38]:
B1, B2, B3 = Variable('B1'), Variable('B2'), Variable('B3')
B1: 
B2: 
B3: 
In [39]:
C1, C2, C3 = Variable('C1'), Variable('C2'), Variable('C3')
C1: 
C2: 
C3: 
In [40]:
# Duplicate of I??
#I, IB, IC = Variable('I'), Variable('IB'), Variable('IC')
In [41]:
# pregated_controlled_ngate = Circuit(ExprArray(ExprTuple(Input(a), Gate(u), MultiQubitGate(CONTROL, Set(one, two)), Output(b)),
# ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(y))))
In [42]:
# pregated_controlled_ngate_with_merge = Circuit(ExprArray(ExprTuple(Input(c), MultiWire(k), MultiWire(k).with_implicit_style(), MultiQubitGate(MultiWire(k).with_implicit_style(), Set(one, two)), SPACE, SPACE),
# ExprTuple(Input(a), Gate(u), MultiQubitGate(CONTROL, Set(two, three)), MultiQubitGate(I, Set(one, two)), MultiWire(Add(k, one)), Output(d)),
# ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(two, three)), Output(y), SPACE, SPACE)))
In [43]:
%end common