Expression of type Lambda

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, Conditional, Lambda, 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, NaturalPos, 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 = Lambda(n, Conditional(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(), InSet(n, NaturalPos)))

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

n \mapsto \left\{\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} \textrm{ if } n \in \mathbb{N}^+\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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