Expression of type Forall ¶

from the theory of proveit.physics.quantum.algebra ¶

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 A, B, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Commutator, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Forall, Iff, InSet, Set
from proveit.numbers import Complex, Interval, NaturalPos, one
from proveit.physics.quantum import Bra, Ket, Qmult

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = LinMap(Hspace, Hspace)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = Forall(instance_param_or_params = [n], instance_expr = Forall(instance_param_or_params = [Hspace], instance_expr = Forall(instance_param_or_params = [A, B], instance_expr = Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).with_wrapping(), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).with_wrapping(), domain = NaturalPos)

# 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_{n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\begin{array}{l}\forall_{A, B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{n}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\right)\end{array}\right]\end{array}\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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',)

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

Expression of type Forall¶

from the theory of proveit.physics.quantum.algebra¶

Expression of type Forall ¶

from the theory of proveit.physics.quantum.algebra ¶