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, TensorProd, VecAdd, VecSum
from proveit.numbers import Add, Exp, Interval, Mult, e, frac, i, one, pi, subtract, two, zero
from proveit.physics.quantum import NumKet, ket0, ket1
from proveit.physics.quantum.QPE import _phase, two_pow_t

# build up the expression from sub-expressions
sub_expr1 = frac(t, two)
sub_expr2 = frac(one, Exp(two, sub_expr1))
sub_expr3 = frac(one, Exp(two, subtract(frac(Add(t, one), two), sub_expr1)))
sub_expr4 = VecAdd(ket0, ScalarMult(Exp(e, Mult(two, pi, i, _phase, two_pow_t)), ket1))
sub_expr5 = VecSum(index_or_indices = [k], summand = ScalarMult(Exp(e, Mult(two, pi, i, _phase, k)), NumKet(k, t)), domain = Interval(zero, subtract(two_pow_t, one)))
expr = ExprTuple(ScalarMult(sub_expr3, TensorProd(sub_expr4, ScalarMult(sub_expr2, sub_expr5))), ScalarMult(sub_expr3, ScalarMult(sub_expr2, TensorProd(sub_expr4, sub_expr5))))

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(\frac{1}{2^{\frac{t + 1}{2} - \frac{t}{2}}} \cdot \left(\left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot 2^{t}} \cdot \lvert 1 \rangle\right)\right) {\otimes} \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)\right), \frac{1}{2^{\frac{t + 1}{2} - \frac{t}{2}}} \cdot \left(\frac{1}{2^{\frac{t}{2}}} \cdot \left(\left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot 2^{t}} \cdot \lvert 1 \rangle\right)\right) {\otimes} \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)\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: 52 operands: 3
2	Operation	operator: 52 operands: 4
3	ExprTuple	6, 5
4	ExprTuple	6, 7
5	Operation	operator: 16 operands: 8
6	Operation	operator: 48 operands: 9
7	Operation	operator: 52 operands: 10
8	ExprTuple	20, 11
9	ExprTuple	86, 12
10	ExprTuple	18, 13
11	Operation	operator: 52 operands: 14
12	Operation	operator: 80 operands: 15
13	Operation	operator: 16 operands: 17
14	ExprTuple	18, 21
15	ExprTuple	84, 19
16	Literal
17	ExprTuple	20, 21
18	Operation	operator: 48 operands: 22
19	Operation	operator: 72 operands: 23
20	Operation	operator: 24 operands: 25
21	Operation	operator: 26 operand: 33
22	ExprTuple	86, 28
23	ExprTuple	29, 30
24	Literal
25	ExprTuple	31, 32
26	Literal
27	ExprTuple	33
28	Operation	operator: 80 operands: 34
29	Operation	operator: 48 operands: 35
30	Operation	operator: 82 operand: 42
31	Operation	operator: 51 operand: 68
32	Operation	operator: 52 operands: 38
33	Lambda	parameter: 77 body: 40
34	ExprTuple	84, 42
35	ExprTuple	41, 84
36	ExprTuple	42
37	ExprTuple	68
38	ExprTuple	43, 44
39	ExprTuple	77
40	Conditional	value: 45 condition: 46
41	Operation	operator: 72 operands: 47
42	Operation	operator: 48 operands: 49
43	Operation	operator: 80 operands: 50
44	Operation	operator: 51 operand: 86
45	Operation	operator: 52 operands: 53
46	Operation	operator: 54 operands: 55
47	ExprTuple	85, 86
48	Literal
49	ExprTuple	85, 84
50	ExprTuple	66, 56
51	Literal
52	Literal
53	ExprTuple	57, 58
54	Literal
55	ExprTuple	77, 59
56	Operation	operator: 70 operands: 60
57	Operation	operator: 80 operands: 61
58	Operation	operator: 62 operands: 63
59	Operation	operator: 64 operands: 65
60	ExprTuple	84, 74, 75, 76, 78
61	ExprTuple	66, 67
62	Literal
63	ExprTuple	77, 85
64	Literal
65	ExprTuple	68, 69
66	Literal
67	Operation	operator: 70 operands: 71
68	Literal
69	Operation	operator: 72 operands: 73
70	Literal
71	ExprTuple	84, 74, 75, 76, 77
72	Literal
73	ExprTuple	78, 79
74	Literal
75	Literal
76	Literal
77	Variable
78	Operation	operator: 80 operands: 81
79	Operation	operator: 82 operand: 86
80	Literal
81	ExprTuple	84, 85
82	Literal
83	ExprTuple	86
84	Literal
85	Variable
86	Literal