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

# 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_{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}

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