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, 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 = Lambda([A, B], Conditional(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), And(InSet(A, sub_expr2), InSet(B, sub_expr2), Equals(Adj(A), A), Equals(Adj(B), B))))

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

\left(A, B\right) \mapsto \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} \textrm{ if } A \in \mathbb{C}^{n \times n} ,  B \in \mathbb{C}^{n \times n} ,  A^{\dagger} = A ,  B^{\dagger} = B\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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