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
from proveit.linear_algebra import ScalarMult
from proveit.logic import And, 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 = [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))), And(InSet(var_ket_u, m_ket_domain), normalized_var_ket_u))

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