Expression of type ExprTuple

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 ExprTuple, k, t
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import Equals, Forall
from proveit.numbers import Add, Exp, Interval, Mult, NaturalPos, e, frac, i, one, pi, sqrt, subtract, two, zero
from proveit.physics.quantum import Ket, NumKet
from proveit.physics.quantum.QPE import SubIndexed, _phase, _psi, _psi_t_ket, two_pow_t

# build up the expression from sub-expressions
sub_expr1 = [k]
sub_expr2 = Add(t, one)
sub_expr3 = Exp(e, Mult(two, pi, i, _phase, k))
expr = ExprTuple(Equals(SubIndexed(_psi, [one]), ScalarMult(frac(one, sqrt(two)), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr3, Ket(k)), domain = Interval(zero, one)))), Forall(instance_param_or_params = [t], instance_expr = Equals(SubIndexed(_psi, [sub_expr2]), ScalarMult(frac(one, Exp(two, frac(sub_expr2, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr3, NumKet(k, sub_expr2)), domain = Interval(zero, subtract(Mult(two, two_pow_t), one))))), domain = NaturalPos, condition = Equals(_psi_t_ket, ScalarMult(frac(one, Exp(two, frac(t, two))), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(sub_expr3, NumKet(k, t)), domain = Interval(zero, subtract(two_pow_t, one)))))))

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

\left(\lvert \psi_{1} \rangle = \left(\frac{1}{\sqrt{2}} \cdot \left(\sum_{k=0}^{1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle\right)\right)\right), \forall_{t \in \mathbb{N}^+~|~\lvert \psi_{t} \rangle = \left(\frac{1}{2^{\frac{t}{2}}} \cdot \left(\sum_{k=0}^{2^{t} - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right)\right)\right)}~\left(\lvert \psi_{t + 1} \rangle = \left(\frac{1}{2^{\frac{t + 1}{2}}} \cdot \left(\sum_{k=0}^{\left(2 \cdot 2^{t}\right) - 1} \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t + 1}\right)\right)\right)\right)\right)

stored_expr.style_options()

name	description	default	current value	related methods
wrap_positions	position(s) at which wrapping is to occur; 'n' is after the nth comma.	()	()	('with_wrapping_at',)
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	left	left	('with_justification',)

# display the expression information
stored_expr.expr_info()

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