Expression of type Forall ¶

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 ExprRange, IndexedVar, U, Variable, t
from proveit.linear_algebra import MatrixMult, ScalarMult
from proveit.logic import Equals, Forall
from proveit.numbers import Exp, Mult, e, i, one, pi, two
from proveit.physics.quantum import m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(varphi, sub_expr1)
expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(IndexedVar(U, sub_expr1), var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr2)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping()

# 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())

\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{t}~|~\left(\left(U_{1} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert u \rangle\right)\right), \left(\left(U_{2} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert u \rangle\right)\right), \ldots, \left(\left(U_{t} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert u \rangle\right)\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \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_{t}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U_{1}} & \gate{U_{2}} & \gate{\cdots} & \gate{U_{t}} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\end{array}\right]\end{array}

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	True	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

	core type	sub-expressions
0	Operation	operator: 6 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 95 body: 3
3	Conditional	value: 4 condition: 5
4	Operation	operator: 6 operand: 9
5	Operation	operator: 24 operands: 8
6	Literal
7	ExprTuple	9
8	ExprTuple	10, 11
9	Lambda	parameters: 12 body: 13
10	Operation	operator: 14 operands: 15
11	Operation	operator: 108 operands: 16
12	ExprTuple	17
13	Conditional	value: 18 condition: 19
14	Literal
15	ExprTuple	95, 20
16	ExprTuple	21, 148
17	ExprRange	lambda_map: 22 start_index: 148 end_index: 147
18	Operation	operator: 108 operands: 23
19	Operation	operator: 24 operands: 25
20	Operation	operator: 26 operands: 27
21	Operation	operator: 28 operand: 95
22	Lambda	parameter: 157 body: 154
23	ExprTuple	30, 148
24	Literal
25	ExprTuple	31
26	Literal
27	ExprTuple	32, 33
28	Literal
29	ExprTuple	95
30	Operation	operator: 34 operand: 38
31	ExprRange	lambda_map: 36 start_index: 148 end_index: 147
32	Literal
33	Operation	operator: 139 operands: 37
34	Literal
35	ExprTuple	38
36	Lambda	parameter: 157 body: 39
37	ExprTuple	151, 131
38	Operation	operator: 40 operands: 41
39	Operation	operator: 108 operands: 42
40	Literal
41	ExprTuple	43, 44, 45
42	ExprTuple	46, 47
43	ExprTuple	48, 49
44	ExprRange	lambda_map: 50 start_index: 148 end_index: 147
45	ExprTuple	51, 52
46	Operation	operator: 53 operands: 54
47	Operation	operator: 126 operands: 55
48	ExprRange	lambda_map: 56 start_index: 148 end_index: 147
49	ExprRange	lambda_map: 57 start_index: 148 end_index: 131
50	Lambda	parameter: 130 body: 58
51	ExprRange	lambda_map: 59 start_index: 148 end_index: 147
52	ExprRange	lambda_map: 60 start_index: 148 end_index: 131
53	Literal
54	ExprTuple	61, 95
55	ExprTuple	134, 95
56	Lambda	parameter: 157 body: 62
57	Lambda	parameter: 157 body: 63
58	ExprTuple	64, 65
59	Lambda	parameter: 157 body: 66
60	Lambda	parameter: 157 body: 67
61	IndexedVar	variable: 121 index: 157
62	Operation	operator: 81 operands: 68
63	Operation	operator: 106 operands: 69
64	ExprRange	lambda_map: 70 start_index: 148 end_index: 147
65	ExprRange	lambda_map: 71 start_index: 148 end_index: 131
66	Operation	operator: 86 operands: 72
67	Operation	operator: 106 operands: 73
68	NamedExprs	state: 74
69	NamedExprs	element: 75 targets: 92
70	Lambda	parameter: 157 body: 76
71	Lambda	parameter: 157 body: 77
72	NamedExprs	state: 78
73	NamedExprs	element: 79 targets: 92
74	Operation	operator: 141 operand: 88
75	Operation	operator: 81 operands: 87
76	Operation	operator: 82 operands: 83
77	Operation	operator: 106 operands: 84
78	Operation	operator: 126 operands: 85
79	Operation	operator: 86 operands: 87
80	ExprTuple	88
81	Literal
82	Literal
83	ExprTuple	89, 90
84	NamedExprs	element: 91 targets: 92
85	ExprTuple	93, 94
86	Literal
87	NamedExprs	state: 95 part: 157
88	Literal
89	Conditional	value: 96 condition: 97
90	Conditional	value: 98 condition: 99
91	Operation	operator: 109 operands: 100
92	Operation	operator: 101 operands: 102
93	Operation	operator: 137 operands: 103
94	Operation	operator: 104 operands: 105
95	Variable
96	Operation	operator: 106 operands: 107
97	Operation	operator: 108 operands: 112
98	Operation	operator: 109 operands: 110
99	Operation	operator: 111 operands: 112
100	NamedExprs	operation: 113 part: 157
101	Literal
102	ExprTuple	136, 114
103	ExprTuple	148, 115
104	Literal
105	ExprTuple	116, 117
106	Literal
107	NamedExprs	element: 118 targets: 119
108	Literal
109	Literal
110	NamedExprs	operation: 120
111	Literal
112	ExprTuple	130, 157
113	IndexedVar	variable: 121 index: 130
114	Operation	operator: 143 operands: 123
115	Operation	operator: 139 operands: 124
116	Operation	operator: 141 operand: 133
117	Operation	operator: 126 operands: 127
118	Literal
119	Operation	operator: 128 operand: 136
120	Literal
121	Variable
122	ExprTuple	130
123	ExprTuple	147, 131
124	ExprTuple	151, 132
125	ExprTuple	133
126	Literal
127	ExprTuple	134, 135
128	Literal
129	ExprTuple	136
130	Variable
131	Variable
132	Operation	operator: 137 operands: 138
133	Literal
134	Operation	operator: 139 operands: 140
135	Operation	operator: 141 operand: 148
136	Operation	operator: 143 operands: 144
137	Literal
138	ExprTuple	148, 151
139	Literal
140	ExprTuple	145, 146
141	Literal
142	ExprTuple	148
143	Literal
144	ExprTuple	147, 148
145	Literal
146	Operation	operator: 149 operands: 150
147	Variable
148	Literal
149	Literal
150	ExprTuple	151, 152, 153, 154
151	Literal
152	Literal
153	Literal
154	IndexedVar	variable: 155 index: 157
155	Variable
156	ExprTuple	157
157	Variable

Expression of type Forall¶

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

Expression of type Forall ¶

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