Expression of type And

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 k, t
from proveit.linear_algebra import ScalarMult, VecSum
from proveit.logic import And, 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 = And(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)\right) \land \left[\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
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

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