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 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 = [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()

# 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_{\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}

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