Expression of type Lambda

from the theory of proveit.physics.quantum.QPE

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, ExprRange, Lambda, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import Unitary
from proveit.logic import InSet
from proveit.numbers import Add, Exp, Interval, one, two
from proveit.physics.quantum.QPE import QPE1, QPE1_U_t_circuit
from proveit.physics.quantum.circuits import Gate, MultiQubitElem, Qcircuit, QcircuitEquiv

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, s)
sub_expr3 = MultiQubitElem(element = Gate(operation = QPE1(U, t), part = sub_expr1), targets = Interval(one, sub_expr2))
expr = Lambda(U, Conditional(QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, sub_expr3, one, t), ExprRange(sub_expr1, sub_expr3, Add(t, one), sub_expr2)])), QPE1_U_t_circuit), InSet(U, Unitary(Exp(two, s)))))

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

U \mapsto \left\{\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \multigate{1}{\textrm{QPE}_1\left(U, t\right)} & { /^{t} } \qw \\
& \ghost{\textrm{QPE}_1\left(U, t\right)} & { /^{s} } \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qw \\
& \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qw \\
& \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & { /^{s} } \qw
} \end{array}\right) \textrm{ if } U \in \textrm{U}\left(2^{s}\right)\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Lambda	parameter: 81 body: 2
1	ExprTuple	81
2	Conditional	value: 3 condition: 4
3	Operation	operator: 5 operands: 6
4	Operation	operator: 7 operands: 8
5	Literal
6	ExprTuple	9, 10
7	Literal
8	ExprTuple	81, 11
9	Operation	operator: 13 operand: 17
10	Operation	operator: 13 operands: 14
11	Operation	operator: 15 operand: 19
12	ExprTuple	17
13	Literal
14	ExprTuple	18
15	Literal
16	ExprTuple	19
17	ExprTuple	20, 21
18	ExprRange	lambda_map: 22 start_index: 23 end_index: 24
19	Operation	operator: 85 operands: 25
20	ExprRange	lambda_map: 26 start_index: 92 end_index: 91
21	ExprRange	lambda_map: 26 start_index: 84 end_index: 69
22	Lambda	parameter: 95 body: 27
23	Operation	operator: 87 operands: 28
24	Literal
25	ExprTuple	89, 83
26	Lambda	parameter: 74 body: 29
27	ExprTuple	30, 31
28	ExprTuple	32, 92
29	Operation	operator: 61 operands: 33
30	ExprRange	lambda_map: 34 start_index: 92 end_index: 91
31	ExprRange	lambda_map: 35 start_index: 92 end_index: 83
32	Operation	operator: 93 operand: 91
33	NamedExprs	element: 37 targets: 38
34	Lambda	parameter: 74 body: 39
35	Lambda	parameter: 74 body: 41
36	ExprTuple	91
37	Operation	operator: 64 operands: 42
38	Operation	operator: 59 operands: 43
39	Operation	operator: 44 operands: 45
40	ExprTuple	74
41	Operation	operator: 61 operands: 46
42	NamedExprs	operation: 47 part: 74
43	ExprTuple	92, 69
44	Literal
45	ExprTuple	48, 49
46	NamedExprs	element: 50 targets: 51
47	Operation	operator: 52 operands: 53
48	Conditional	value: 54 condition: 55
49	Conditional	value: 56 condition: 57
50	Operation	operator: 64 operands: 58
51	Operation	operator: 59 operands: 60
52	Literal
53	ExprTuple	81, 91
54	Operation	operator: 61 operands: 62
55	Operation	operator: 63 operands: 67
56	Operation	operator: 64 operands: 65
57	Operation	operator: 66 operands: 67
58	NamedExprs	operation: 68 part: 74
59	Literal
60	ExprTuple	84, 69
61	Literal
62	NamedExprs	element: 70 targets: 71
63	Literal
64	Literal
65	NamedExprs	operation: 72
66	Literal
67	ExprTuple	73, 74
68	Operation	operator: 75 operands: 76
69	Operation	operator: 87 operands: 77
70	Literal
71	Operation	operator: 78 operand: 84
72	Literal
73	Operation	operator: 87 operands: 80
74	Variable
75	Literal
76	ExprTuple	81, 82
77	ExprTuple	91, 83
78	Literal
79	ExprTuple	84
80	ExprTuple	95, 91
81	Variable
82	Operation	operator: 85 operands: 86
83	Variable
84	Operation	operator: 87 operands: 88
85	Literal
86	ExprTuple	89, 90
87	Literal
88	ExprTuple	91, 92
89	Literal
90	Operation	operator: 93 operand: 95
91	Variable
92	Literal
93	Literal
94	ExprTuple	95
95	Variable