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, 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 = [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()

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

\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}

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