Expression of type Conditional ¶

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

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, U, m
from proveit.linear_algebra import ScalarMult, Unitary
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Exp, Mult, NaturalPos, e, i, one, pi, two
from proveit.physics.quantum import Qmult, m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
expr = Conditional(Forall(instance_param_or_params = [U], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [varphi], instance_expr = Equals(Prob(phase_kickback_circuit), one), condition = Equals(Qmult(U, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, varphi)), var_ket_u))), domain = m_ket_domain, condition = normalized_var_ket_u), domain = Unitary(Exp(two, m))), InSet(m, NaturalPos))

# 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\{\forall_{U \in \textrm{U}\left(2^{m}\right)}~\left[\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\left[\forall_{\varphi~|~\left(U \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert u \rangle\right)}~\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\right]\right] \textrm{ if } m \in \mathbb{N}^+\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: 20 operand: 5
2	Operation	operator: 29 operands: 4
3	ExprTuple	5
4	ExprTuple	124, 6
5	Lambda	parameter: 107 body: 8
6	Literal
7	ExprTuple	107
8	Conditional	value: 9 condition: 10
9	Operation	operator: 20 operand: 13
10	Operation	operator: 29 operands: 12
11	ExprTuple	13
12	ExprTuple	107, 14
13	Lambda	parameter: 111 body: 15
14	Operation	operator: 16 operand: 47
15	Conditional	value: 18 condition: 19
16	Literal
17	ExprTuple	47
18	Operation	operator: 20 operand: 24
19	Operation	operator: 22 operands: 23
20	Literal
21	ExprTuple	24
22	Literal
23	ExprTuple	25, 26
24	Lambda	parameter: 139 body: 28
25	Operation	operator: 29 operands: 30
26	Operation	operator: 37 operands: 31
27	ExprTuple	139
28	Conditional	value: 32 condition: 33
29	Literal
30	ExprTuple	111, 34
31	ExprTuple	35, 133
32	Operation	operator: 37 operands: 36
33	Operation	operator: 37 operands: 38
34	Operation	operator: 39 operands: 40
35	Operation	operator: 41 operand: 111
36	ExprTuple	43, 133
37	Literal
38	ExprTuple	44, 45
39	Literal
40	ExprTuple	46, 47
41	Literal
42	ExprTuple	111
43	Operation	operator: 48 operand: 54
44	Operation	operator: 50 operands: 51
45	Operation	operator: 116 operands: 52
46	Literal
47	Operation	operator: 127 operands: 53
48	Literal
49	ExprTuple	54
50	Literal
51	ExprTuple	107, 111
52	ExprTuple	122, 111
53	ExprTuple	136, 124
54	Operation	operator: 55 operands: 56
55	Literal
56	ExprTuple	57, 58, 59
57	ExprTuple	60, 61
58	ExprTuple	62, 63
59	ExprTuple	64, 65
60	Operation	operator: 97 operands: 66
61	ExprRange	lambda_map: 67 start_index: 133 end_index: 72
62	Operation	operator: 88 operands: 68
63	ExprRange	lambda_map: 69 start_index: 133 end_index: 72
64	Operation	operator: 103 operands: 70
65	ExprRange	lambda_map: 71 start_index: 133 end_index: 72
66	NamedExprs	state: 73
67	Lambda	parameter: 112 body: 74
68	NamedExprs	element: 75 targets: 76
69	Lambda	parameter: 112 body: 77
70	NamedExprs	state: 78
71	Lambda	parameter: 112 body: 80
72	Operation	operator: 118 operands: 81
73	Operation	operator: 129 operand: 90
74	Operation	operator: 88 operands: 83
75	Literal
76	Operation	operator: 84 operand: 136
77	Operation	operator: 88 operands: 86
78	Operation	operator: 116 operands: 87
79	ExprTuple	112
80	Operation	operator: 88 operands: 89
81	ExprTuple	124, 133
82	ExprTuple	90
83	NamedExprs	element: 91 targets: 96
84	Literal
85	ExprTuple	136
86	NamedExprs	element: 92 targets: 96
87	ExprTuple	93, 94
88	Literal
89	NamedExprs	element: 95 targets: 96
90	Literal
91	Operation	operator: 97 operands: 104
92	Operation	operator: 98 operands: 99
93	Operation	operator: 125 operands: 100
94	Operation	operator: 101 operands: 102
95	Operation	operator: 103 operands: 104
96	Operation	operator: 105 operands: 106
97	Literal
98	Literal
99	NamedExprs	operation: 107 part: 112
100	ExprTuple	133, 108
101	Literal
102	ExprTuple	109, 110
103	Literal
104	NamedExprs	state: 111 part: 112
105	Literal
106	ExprTuple	136, 113
107	Variable
108	Operation	operator: 127 operands: 114
109	Operation	operator: 129 operand: 121
110	Operation	operator: 116 operands: 117
111	Variable
112	Variable
113	Operation	operator: 118 operands: 119
114	ExprTuple	136, 120
115	ExprTuple	121
116	Literal
117	ExprTuple	122, 123
118	Literal
119	ExprTuple	124, 136
120	Operation	operator: 125 operands: 126
121	Literal
122	Operation	operator: 127 operands: 128
123	Operation	operator: 129 operand: 133
124	Variable
125	Literal
126	ExprTuple	133, 136
127	Literal
128	ExprTuple	131, 132
129	Literal
130	ExprTuple	133
131	Literal
132	Operation	operator: 134 operands: 135
133	Literal
134	Literal
135	ExprTuple	136, 137, 138, 139
136	Literal
137	Literal
138	Literal
139	Variable

Expression of type Conditional¶

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

Expression of type Conditional ¶

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