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 U, m
from proveit.linear_algebra import ScalarMult, Unitary
from proveit.logic import Equals, Forall
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 = 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)))

expr:

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

\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]

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('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',)

# display the expression information
stored_expr.expr_info()

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