Expression of type Conditional ¶

from the theory of proveit.physics.quantum.QPE ¶

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprRange, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import Unitary
from proveit.logic import InSet
from proveit.numbers import Add, Exp, Interval, one, two
from proveit.physics.quantum.QPE import QPE1, QPE1_U_t_circuit
from proveit.physics.quantum.circuits import Gate, MultiQubitElem, Qcircuit, QcircuitEquiv

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, s)
sub_expr3 = MultiQubitElem(element = Gate(operation = QPE1(U, t), part = sub_expr1), targets = Interval(one, sub_expr2))
expr = Conditional(QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, sub_expr3, one, t), ExprRange(sub_expr1, sub_expr3, Add(t, one), sub_expr2)])), QPE1_U_t_circuit), InSet(U, Unitary(Exp(two, s))))

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left\{\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \multigate{1}{\textrm{QPE}_1\left(U, t\right)} & { /^{t} } \qw \\
& \ghost{\textrm{QPE}_1\left(U, t\right)} & { /^{s} } \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qw \\
& \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qw \\
& \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & { /^{s} } \qw
} \end{array}\right) \textrm{ if } U \in \textrm{U}\left(2^{s}\right)\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Conditional	value: 1 condition: 2
1	Operation	operator: 3 operands: 4
2	Operation	operator: 5 operands: 6
3	Literal
4	ExprTuple	7, 8
5	Literal
6	ExprTuple	79, 9
7	Operation	operator: 11 operand: 15
8	Operation	operator: 11 operands: 12
9	Operation	operator: 13 operand: 17
10	ExprTuple	15
11	Literal
12	ExprTuple	16
13	Literal
14	ExprTuple	17
15	ExprTuple	18, 19
16	ExprRange	lambda_map: 20 start_index: 21 end_index: 22
17	Operation	operator: 83 operands: 23
18	ExprRange	lambda_map: 24 start_index: 90 end_index: 89
19	ExprRange	lambda_map: 24 start_index: 82 end_index: 67
20	Lambda	parameter: 93 body: 25
21	Operation	operator: 85 operands: 26
22	Literal
23	ExprTuple	87, 81
24	Lambda	parameter: 72 body: 27
25	ExprTuple	28, 29
26	ExprTuple	30, 90
27	Operation	operator: 59 operands: 31
28	ExprRange	lambda_map: 32 start_index: 90 end_index: 89
29	ExprRange	lambda_map: 33 start_index: 90 end_index: 81
30	Operation	operator: 91 operand: 89
31	NamedExprs	element: 35 targets: 36
32	Lambda	parameter: 72 body: 37
33	Lambda	parameter: 72 body: 39
34	ExprTuple	89
35	Operation	operator: 62 operands: 40
36	Operation	operator: 57 operands: 41
37	Operation	operator: 42 operands: 43
38	ExprTuple	72
39	Operation	operator: 59 operands: 44
40	NamedExprs	operation: 45 part: 72
41	ExprTuple	90, 67
42	Literal
43	ExprTuple	46, 47
44	NamedExprs	element: 48 targets: 49
45	Operation	operator: 50 operands: 51
46	Conditional	value: 52 condition: 53
47	Conditional	value: 54 condition: 55
48	Operation	operator: 62 operands: 56
49	Operation	operator: 57 operands: 58
50	Literal
51	ExprTuple	79, 89
52	Operation	operator: 59 operands: 60
53	Operation	operator: 61 operands: 65
54	Operation	operator: 62 operands: 63
55	Operation	operator: 64 operands: 65
56	NamedExprs	operation: 66 part: 72
57	Literal
58	ExprTuple	82, 67
59	Literal
60	NamedExprs	element: 68 targets: 69
61	Literal
62	Literal
63	NamedExprs	operation: 70
64	Literal
65	ExprTuple	71, 72
66	Operation	operator: 73 operands: 74
67	Operation	operator: 85 operands: 75
68	Literal
69	Operation	operator: 76 operand: 82
70	Literal
71	Operation	operator: 85 operands: 78
72	Variable
73	Literal
74	ExprTuple	79, 80
75	ExprTuple	89, 81
76	Literal
77	ExprTuple	82
78	ExprTuple	93, 89
79	Variable
80	Operation	operator: 83 operands: 84
81	Variable
82	Operation	operator: 85 operands: 86
83	Literal
84	ExprTuple	87, 88
85	Literal
86	ExprTuple	89, 90
87	Literal
88	Operation	operator: 91 operand: 93
89	Variable
90	Literal
91	Literal
92	ExprTuple	93
93	Variable

Expression of type Conditional¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Conditional ¶

from the theory of proveit.physics.quantum.QPE ¶