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, MatrixSpace, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, CartExp, 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 = MatrixSpace(field = Complex, rows = n, columns = n)
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(CartExp(Complex, n)))).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 \mathbb{C}^{n \times n}~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathbb{C}^{n \times n}\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(\mathbb{C}^{n}\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: 72 operands: 16
11	Operation	operator: 40 operand: 24
12	Operation	operator: 102 operands: 18
13	Operation	operator: 102 operands: 19
14	Operation	operator: 72 operands: 20
15	Operation	operator: 72 operands: 21
16	ExprTuple	22, 23
17	ExprTuple	24
18	ExprTuple	76, 35
19	ExprTuple	78, 35
20	ExprTuple	25, 76
21	ExprTuple	26, 78
22	Operation	operator: 27 operands: 28
23	Operation	operator: 29 operand: 35
24	Lambda	parameters: 49 body: 31
25	Operation	operator: 33 operand: 76
26	Operation	operator: 33 operand: 78
27	Literal
28	ExprTuple	76, 78
29	Literal
30	ExprTuple	35
31	Conditional	value: 36 condition: 37
32	ExprTuple	76
33	Literal
34	ExprTuple	78
35	Operation	operator: 38 operands: 39
36	Operation	operator: 40 operand: 43
37	Operation	operator: 102 operands: 42
38	Literal
39	NamedExprs	field: 91 rows: 117 columns: 117
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: 116 end_index: 117
53	ExprRange	lambda_map: 59 start_index: 116 end_index: 117
54	Operation	operator: 61 operands: 60
55	Operation	operator: 61 operands: 62
56	ExprRange	lambda_map: 63 start_index: 116 end_index: 117
57	Operation	operator: 64 operands: 65
58	Lambda	parameter: 98 body: 89
59	Lambda	parameter: 98 body: 90
60	ExprTuple	66, 67
61	Literal
62	ExprTuple	68, 69
63	Lambda	parameter: 98 body: 70
64	Literal
65	ExprTuple	91, 117
66	Operation	operator: 72 operands: 71
67	Operation	operator: 72 operands: 73
68	ExprRange	lambda_map: 74 start_index: 116 end_index: 117
69	ExprRange	lambda_map: 75 start_index: 116 end_index: 117
70	IndexedVar	variable: 122 index: 98
71	ExprTuple	76, 77
72	Literal
73	ExprTuple	78, 79
74	Lambda	parameter: 98 body: 80
75	Lambda	parameter: 98 body: 81
76	Variable
77	Operation	operator: 83 operand: 87
78	Variable
79	Operation	operator: 83 operand: 88
80	Operation	operator: 102 operands: 85
81	Operation	operator: 102 operands: 86
82	ExprTuple	87
83	Literal
84	ExprTuple	88
85	ExprTuple	89, 91
86	ExprTuple	90, 91
87	Lambda	parameter: 124 body: 92
88	Lambda	parameter: 124 body: 93
89	IndexedVar	variable: 108 index: 98
90	IndexedVar	variable: 109 index: 98
91	Literal
92	Conditional	value: 95 condition: 97
93	Conditional	value: 96 condition: 97
94	ExprTuple	98
95	Operation	operator: 100 operands: 99
96	Operation	operator: 100 operands: 101
97	Operation	operator: 102 operands: 103
98	Variable
99	ExprTuple	104, 106
100	Literal
101	ExprTuple	105, 106
102	Literal
103	ExprTuple	124, 107
104	IndexedVar	variable: 108 index: 124
105	IndexedVar	variable: 109 index: 124
106	Operation	operator: 110 operands: 111
107	Operation	operator: 112 operands: 113
108	Variable
109	Variable
110	Literal
111	ExprTuple	114, 115
112	Literal
113	ExprTuple	116, 117
114	Operation	operator: 118 operand: 121
115	Operation	operator: 119 operand: 121
116	Literal
117	Variable
118	Literal
119	Literal
120	ExprTuple	121
121	IndexedVar	variable: 122 index: 124
122	Variable
123	ExprTuple	124
124	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 ¶