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, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, 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 = LinMap(Hspace, Hspace)
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(Hspace))).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(\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} \textrm{ if } A \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right) ,  B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right) ,  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: 67 operands: 13
8	Operation	operator: 37 operand: 21
9	Operation	operator: 97 operands: 15
10	Operation	operator: 97 operands: 16
11	Operation	operator: 67 operands: 17
12	Operation	operator: 67 operands: 18
13	ExprTuple	19, 20
14	ExprTuple	21
15	ExprTuple	71, 32
16	ExprTuple	73, 32
17	ExprTuple	22, 71
18	ExprTuple	23, 73
19	Operation	operator: 24 operands: 25
20	Operation	operator: 26 operand: 32
21	Lambda	parameters: 46 body: 28
22	Operation	operator: 30 operand: 71
23	Operation	operator: 30 operand: 73
24	Literal
25	ExprTuple	71, 73
26	Literal
27	ExprTuple	32
28	Conditional	value: 33 condition: 34
29	ExprTuple	71
30	Literal
31	ExprTuple	73
32	Operation	operator: 35 operands: 36
33	Operation	operator: 37 operand: 40
34	Operation	operator: 97 operands: 39
35	Literal
36	ExprTuple	54, 54
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: 111 end_index: 112
50	ExprRange	lambda_map: 56 start_index: 111 end_index: 112
51	Operation	operator: 58 operands: 57
52	Operation	operator: 58 operands: 59
53	ExprRange	lambda_map: 60 start_index: 111 end_index: 112
54	Variable
55	Lambda	parameter: 93 body: 84
56	Lambda	parameter: 93 body: 85
57	ExprTuple	61, 62
58	Literal
59	ExprTuple	63, 64
60	Lambda	parameter: 93 body: 65
61	Operation	operator: 67 operands: 66
62	Operation	operator: 67 operands: 68
63	ExprRange	lambda_map: 69 start_index: 111 end_index: 112
64	ExprRange	lambda_map: 70 start_index: 111 end_index: 112
65	IndexedVar	variable: 117 index: 93
66	ExprTuple	71, 72
67	Literal
68	ExprTuple	73, 74
69	Lambda	parameter: 93 body: 75
70	Lambda	parameter: 93 body: 76
71	Variable
72	Operation	operator: 78 operand: 82
73	Variable
74	Operation	operator: 78 operand: 83
75	Operation	operator: 97 operands: 80
76	Operation	operator: 97 operands: 81
77	ExprTuple	82
78	Literal
79	ExprTuple	83
80	ExprTuple	84, 86
81	ExprTuple	85, 86
82	Lambda	parameter: 119 body: 87
83	Lambda	parameter: 119 body: 88
84	IndexedVar	variable: 103 index: 93
85	IndexedVar	variable: 104 index: 93
86	Literal
87	Conditional	value: 90 condition: 92
88	Conditional	value: 91 condition: 92
89	ExprTuple	93
90	Operation	operator: 95 operands: 94
91	Operation	operator: 95 operands: 96
92	Operation	operator: 97 operands: 98
93	Variable
94	ExprTuple	99, 101
95	Literal
96	ExprTuple	100, 101
97	Literal
98	ExprTuple	119, 102
99	IndexedVar	variable: 103 index: 119
100	IndexedVar	variable: 104 index: 119
101	Operation	operator: 105 operands: 106
102	Operation	operator: 107 operands: 108
103	Variable
104	Variable
105	Literal
106	ExprTuple	109, 110
107	Literal
108	ExprTuple	111, 112
109	Operation	operator: 113 operand: 116
110	Operation	operator: 114 operand: 116
111	Literal
112	Variable
113	Literal
114	Literal
115	ExprTuple	116
116	IndexedVar	variable: 117 index: 119
117	Variable
118	ExprTuple	119
119	Variable