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, 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 = [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), InSet(U, Unitary(Exp(two, m))))

# 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_{\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] \textrm{ if } U \in \textrm{U}\left(2^{m}\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: 12 operand: 5
2	Operation	operator: 21 operands: 4
3	ExprTuple	5
4	ExprTuple	99, 6
5	Lambda	parameter: 103 body: 7
6	Operation	operator: 8 operand: 39
7	Conditional	value: 10 condition: 11
8	Literal
9	ExprTuple	39
10	Operation	operator: 12 operand: 16
11	Operation	operator: 14 operands: 15
12	Literal
13	ExprTuple	16
14	Literal
15	ExprTuple	17, 18
16	Lambda	parameter: 131 body: 20
17	Operation	operator: 21 operands: 22
18	Operation	operator: 29 operands: 23
19	ExprTuple	131
20	Conditional	value: 24 condition: 25
21	Literal
22	ExprTuple	103, 26
23	ExprTuple	27, 125
24	Operation	operator: 29 operands: 28
25	Operation	operator: 29 operands: 30
26	Operation	operator: 31 operands: 32
27	Operation	operator: 33 operand: 103
28	ExprTuple	35, 125
29	Literal
30	ExprTuple	36, 37
31	Literal
32	ExprTuple	38, 39
33	Literal
34	ExprTuple	103
35	Operation	operator: 40 operand: 46
36	Operation	operator: 42 operands: 43
37	Operation	operator: 108 operands: 44
38	Literal
39	Operation	operator: 119 operands: 45
40	Literal
41	ExprTuple	46
42	Literal
43	ExprTuple	99, 103
44	ExprTuple	114, 103
45	ExprTuple	128, 116
46	Operation	operator: 47 operands: 48
47	Literal
48	ExprTuple	49, 50, 51
49	ExprTuple	52, 53
50	ExprTuple	54, 55
51	ExprTuple	56, 57
52	Operation	operator: 89 operands: 58
53	ExprRange	lambda_map: 59 start_index: 125 end_index: 64
54	Operation	operator: 80 operands: 60
55	ExprRange	lambda_map: 61 start_index: 125 end_index: 64
56	Operation	operator: 95 operands: 62
57	ExprRange	lambda_map: 63 start_index: 125 end_index: 64
58	NamedExprs	state: 65
59	Lambda	parameter: 104 body: 66
60	NamedExprs	element: 67 targets: 68
61	Lambda	parameter: 104 body: 69
62	NamedExprs	state: 70
63	Lambda	parameter: 104 body: 72
64	Operation	operator: 110 operands: 73
65	Operation	operator: 121 operand: 82
66	Operation	operator: 80 operands: 75
67	Literal
68	Operation	operator: 76 operand: 128
69	Operation	operator: 80 operands: 78
70	Operation	operator: 108 operands: 79
71	ExprTuple	104
72	Operation	operator: 80 operands: 81
73	ExprTuple	116, 125
74	ExprTuple	82
75	NamedExprs	element: 83 targets: 88
76	Literal
77	ExprTuple	128
78	NamedExprs	element: 84 targets: 88
79	ExprTuple	85, 86
80	Literal
81	NamedExprs	element: 87 targets: 88
82	Literal
83	Operation	operator: 89 operands: 96
84	Operation	operator: 90 operands: 91
85	Operation	operator: 117 operands: 92
86	Operation	operator: 93 operands: 94
87	Operation	operator: 95 operands: 96
88	Operation	operator: 97 operands: 98
89	Literal
90	Literal
91	NamedExprs	operation: 99 part: 104
92	ExprTuple	125, 100
93	Literal
94	ExprTuple	101, 102
95	Literal
96	NamedExprs	state: 103 part: 104
97	Literal
98	ExprTuple	128, 105
99	Variable
100	Operation	operator: 119 operands: 106
101	Operation	operator: 121 operand: 113
102	Operation	operator: 108 operands: 109
103	Variable
104	Variable
105	Operation	operator: 110 operands: 111
106	ExprTuple	128, 112
107	ExprTuple	113
108	Literal
109	ExprTuple	114, 115
110	Literal
111	ExprTuple	116, 128
112	Operation	operator: 117 operands: 118
113	Literal
114	Operation	operator: 119 operands: 120
115	Operation	operator: 121 operand: 125
116	Variable
117	Literal
118	ExprTuple	125, 128
119	Literal
120	ExprTuple	123, 124
121	Literal
122	ExprTuple	125
123	Literal
124	Operation	operator: 126 operands: 127
125	Literal
126	Literal
127	ExprTuple	128, 129, 130, 131
128	Literal
129	Literal
130	Literal
131	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 ¶